% Theoreme et definitions
%%%%%%%%%%%%%%%%%%%%%%%%%

theoreme(![A]:transitive(inc, parties(A))).
definition(transitive(R,E) <=>
            ![X,Y,Z]:(app(X,E) & app(Y,E) & app(Z,E) =>
                        (..[R,X,Y] & ..[R,Y,Z] => ..[R,X,Z]))).
definition( inc(A,B) <=> ! [X] : ( app(X,A) => app(X,B) ) ) .
definition(  app(X,parties(A)) <=> inc(X,A) ) .


% *****************
% * demonstration *
% *****************
% 
% SZS output start proof for probleme
% 
% * * * * * * * * * * * * * * * * * * * * * * * *
% in the following, N is the number of a (sub)theorem
%                   E is the current step
% hyp(N,H,E) means that H is an hypothesis of (sub)theorem N
% concl(N,C,E) means that C is the conclusion of (sub)theorem N
% obj_cte(N,C) means that C is a created object or a given constant
% addhyp(N,H,E) means add H as a new hypothesis for N
% newconcl(N,C,E) means that the new conclusion of N is C
%            (C replaces the precedent conclusion)
% a subtheorem N0-i or N0+i is a subtheorem of the (sub)theorem N0
%    N0 is proved if all N0-i have been proved (&-node)
%              or if one N0+i have been proved (|-node)
% the initial theorem is numbered 0
% 
% * * * theorem to be proved
% 
% 
% * * * proof :
% 
% * * * * * * theoreme 0 * * * * * *
% *** nouvconcl(0, ![A]:transitive(inc, parties(A)), 1) 
% 
% *** explication : theoreme initial
% --------------------------------------------------------- action(ini)
% creer objet(s) z1  
% *** nouvconcl(0, transitive(inc, parties(z1)), 2) 
% 
% *** car concl((0, ![A]:transitive(inc, parties(A))), 1) 
% 
% *** explication : on instancie la(les) variable(s) universelle(s) de la conclusion
% --------------------------------------------------------- regle(!)
% *** nouvconcl(0, seul(parties(z1)::A, transitive(inc, A)), 3) 
% 
% *** car concl(0, transitive(inc, parties(z1)), 2) 
% 
% *** explication : elimination des symboles fonctionnels dans la conclusion 
% for example, p(f(X)) is replaced by only(f(X)::Y, p(Y) 
% --------------------------------------------------------- regle(elifon)
% *** ajhyp(0, parties(z1)::z2, 4), nouvconcl(0, transitive(inc, z2), 4) 
% 
% *** car concl(0, seul(parties(z1)::A, transitive(inc, A)), 3) 
% 
% *** explication : creation de l'objet z2 et de sa definition 
% --------------------------------------------------------- regle(concl_seul)
% *** nouvconcl(0, ![A, B, C]: (A app z2&B app z2&C app z2=> ..[inc, A|...]& ..[inc, B|...]=> ..[inc, A, C]), 5) 
% 
% *** car concl(0, transitive(inc, z2), 4) 
% 
% *** explication : on remplace la conclusion  transitive(inc, z2)  par sa definition(fof transitive ) 
% --------------------------------------------------------- regle(def_concl_pred)
% creer objet(s) z5 z4 z3  
% *** nouvconcl(0, z3 app z2&z4 app z2&z5 app z2=> ..[inc, z3, z4]& ..[inc, z4, z5]=> ..[inc, z3, z5], 6) 
% 
% *** car concl((0, ![A, B, C]: (A app z2&B app z2&C app z2=> ..[inc|...]& ..[inc|...]=> ..[inc, A|...])), 5) 
% 
% *** explication : on instancie la(les) variable(s) universelle(s) de la conclusion
% --------------------------------------------------------- regle(!)
% *** ajhyp(0, z3 app z2, 7)  
% *** ajhyp(0, z4 app z2, 7)  
% *** ajhyp(0, z5 app z2, 7) 
% *** nouvconcl(0, ..[inc, z3, z4]& ..[inc, z4, z5]=> ..[inc, z3, z5], 7) 
% 
% *** car concl(0, z3 app z2&z4 app z2&z5 app z2=> ..[inc, z3, z4]& ..[inc, z4, z5]=> ..[inc, z3, z5], 6) 
% 
% *** explication : pour demontrer H=>C, on suppose H et on doit demontrer C
% --------------------------------------------------------- regle(=>)
% *** ajhyp(0, ..[inc, z3, z4], 8)  
% *** ajhyp(0, ..[inc, z4, z5], 8) 
% *** nouvconcl(0, ..[inc, z3, z5], 8) 
% 
% *** car concl(0, ..[inc, z3, z4]& ..[inc, z4, z5]=> ..[inc, z3, z5], 7) 
% 
% *** explication : pour demontrer H=>C, on suppose H et on doit demontrer C
% --------------------------------------------------------- regle(=>)
% *** nouvconcl(0, inc(z3, z5), 9) 
% 
% *** car concl(0, ..[inc, z3, z5], 8) 
% 
% *** explication : 
% *** car ..[r,a,b] = r(a,b)
% --------------------------------------------------------- regle(..)
% *** nouvconcl(0, ![A]: (A app z3=>A app z5), 13) 
% 
% *** car concl(0, inc(z3, z5), 9) 
% 
% *** explication : on remplace la conclusion  inc(z3, z5)  par sa definition(fof inc ) 
% --------------------------------------------------------- regle(def_concl_pred)
% creer objet(s) z6  
% *** nouvconcl(0, z6 app z3=>z6 app z5, 14) 
% 
% *** car concl((0, ![A]: (A app z3=>A app z5)), 13) 
% 
% *** explication : on instancie la(les) variable(s) universelle(s) de la conclusion
% --------------------------------------------------------- regle(!)
% *** ajhyp(0, z6 app z3, 15) 
% *** nouvconcl(0, z6 app z5, 15) 
% 
% *** car concl(0, z6 app z3=>z6 app z5, 14) 
% 
% *** explication : pour demontrer H=>C, on suppose H et on doit demontrer C
% --------------------------------------------------------- regle(=>)
% *** ajhyp(0, z6 app z4, 16) 
% 
% *** car hyp(0, inc(z3, z4), 8), hyp(0, z6 app z3, 15), obj_cte(0, z6) 
% 
% *** explication : regle2 si (hyp(A, inc(B, D), _), hyp(A, C app B, _), obj_cte(A, C))alors ajhyp(A, C app D, _) 
% construite a partir de la definition de inc (fof inc ) 
% --------------------------------------------------------- regle(inc)
% *** ajhyp(0, z6 app z5, 17) 
% 
% *** car hyp(0, inc(z4, z5), 8), hyp(0, z6 app z4, 16), obj_cte(0, z6) 
% 
% *** explication : regle2 si (hyp(A, inc(B, D), _), hyp(A, C app B, _), obj_cte(A, C))alors ajhyp(A, C app D, _) 
% construite a partir de la definition de inc (fof inc ) 
% --------------------------------------------------------- regle(inc)
% *** nouvconcl(0, true, 18) 
% 
% *** car hyp(0, z6 app z5, 17), concl(0, z6 app z5, 15) 
% 
% *** explication : la conclusion z6 app z5 a demontrer est une hypothese 
% --------------------------------------------------------- regle(stop_hyp_concl)
% le theoreme initial 0 est donc demontre
% * * * * * * * * * * * * * * * * * * * * * * * *
% 
% SZS output end proof for probleme
%