%% Copyright (C) 2024 Dennis J. Darland

%% This file is part of darland's philosophy.

%% darland's philosophy is free software: you can redistribute it and/or modify
%% it under the terms of the GNU General Public License as published by
%% the Free Software Foundation, either version 3 of the License, or
%% (at your option) any later version.

%% darland's philosophy is distributed in the hope that it will be useful, 
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%% GNU General Public License for more details.

%% You should have received a copy of the GNU General Public License
%% along with darland's philosophy. If not, see <http://www.gnu.org/licenses/>.
%% Life predicates to simulate Dennis J. Darlands philosophy. 
%% Started Writing 1/4/2017 
%% 
%%
%%
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Study of impredicative comprehension
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

imp_monadic_proposition_ok(Quant, Var_1, Univ_name_2, Var_1, Tp_2, Var_name, Tp_1 , Reduced_univ, Obj, Proposition) :-
    reduced_universal_ok(Quant, Var_1, Univ_name_2, Var_1, Tp_2, Var_name, Tp_1, Reduced_univ),
    Tp_2 > 1,
    object(Obj),
    strcon(Reduced_univ, "(") = Part1,
    strcon(Part1, Obj) = Part2,
    strcon(Part2, ")") = Proposition.

imp_monadic_proposition_ok(Quant, Var_1, Univ_name_2, Var_1, Tp_2, Var_name, Tp_1 , Reduced_univ, Univ, Proposition) :-
    reduced_universal_ok(Quant, Var_1, Univ_name_2, Var_1, Tp_2, Var_name, Tp_1, Reduced_univ),
    monadic_natural_universal_ok(Univ, Var_XX, Tp_3),
    Tp_2 > Tp_1,
    Tp_1 > Tp_3,
    strcon(Reduced_univ, "(") = Part1,
    strcon(Part1, Univ) = Part2,
    strcon(Part2, ")") = Proposition.

imp_monadic_proposition_ok_OLD(Quant, Univ_name_1, Univ_name_2, Univ_name_1, Tp_2, Var_name, Tp_1 , Name, Univ_name_3) :-
    reduced_universal_ok(Quant, Univ_name_1, Univ_name_2, Univ_name_1, Tp_2, Var_name, Tp_1 , Name, Univ_name_3),
    monadic_universal_ok(Univ_name_3, Var_3, Tp_3),
    Tp_1 > Tp_3. 

gen_imp_monadic_proposition_ok(Quant, Var_1, Quant_imp, Univ_name_1, Univ_name_2, Univ_name_1, Tp_2, Var_name, Tp_1 , Name, Var_1) :-
    quant(Quant),
    quant(Quant_imp),
    variable_ok(Var_1, Tp_3),
    reduced_universal_ok(Quant_imp, Univ_name_1, Univ_name_2, Univ_name_1, Tp_2, Var_name, Tp_1 , Name),
    Tp_1 > Tp_3.

monadic_imp_universal_ok(Quant, Univ_name, Name, Var_name, Tp) :-
    quant(Quant),
    Univ_name $\== Name,
    reduced_universal_ok(Quant, Univ_name_1, Univ_name_2, Univ_name_1, Tp_2, Var_name, Tp_1 , Name),
    strcon("(", Quant_imp) = Work0,
    strcon(" ", Univ_name) = Work1,
    strcon(Work1, ")") = Work2,
    strcon(Work2, Name) = Work3,
    strcon(Work3, "(") = Work4,
    strcon(Work4, Var_name) = Work5,
    strcon(Work5, ",") = Work6,
    strcon(Work6, Var_2) = Work7,
    strcon(Work7, ")") = Name_3.

reduced_universal_ok(Quant, Var_1, Univ_name_2, Var_1, Tp_2, Var_name, Tp , Reduced_univ) :-
    quant(Quant),
    monadic_universal_ok(Univ_name_2, Var_1, Tp_2),
    variable_ok(Var_1, Tp_1),
    strcon("(", Quant) = Work0,
    strcon(Work0, " ") = Work00,
    strcon(Work00, Var_1) = Work1,
    strcon(Work1, ")") = Work2,
    strcon(Work2, Univ_name_2) = Work3,
    strcon(Work3, "(") = Work4,
    strcon(Work4, Var_1) = Work5,
    strcon(Work5, ",") = Work6,
    strcon(Work6, Var_name) = Work7,
    strcon(Work7, ")") = Reduced_univ.
%    Tp >= Tp_imp,
%    Tp >= Tp_2.
    

% imp_monadic_proposition_ok("all", "f1^x0", "f2^x1", "f1^x0", 2, "x0", 1, Reduced_univ, napoleon, Proposition)?