% Theorem and definitions
%%%%%%%%%%%%%%%%%%%%%%%%%

theorem(![A]:transitive(subset, power_set(A))).
definition(transitive(R,E) <=>
            ![X,Y,Z]:(member(X,E) & member(Y,E) & member(Z,E) =>
                        (..[R,X,Y] & ..[R,Y,Z] => ..[R,X,Z]))).
definition(  subset(A,B) <=> 
                        ! [X] : ( member(X,A) => member(X,B) ) ) .
definition(  member(X,power_set(A)) <=> subset(X,A) ) .


% *****************
% * proof *
% *****************
% 
% SZS output start proof for problem
% 
% * * * * * * * * * * * * * * * * * * * * * * * *
% 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 :
% 
% * * * * * * theorem 0 * * * * * *
% *** newconcl(0, ![A]:transitive(subset, power_set(A)), 1) 
% 
% *** explanation : initial theorem
% --------------------------------------------------------- action(ini)
% create object(s) z1  
% *** newconcl(0, transitive(subset, power_set(z1)), 2) 
% 
% *** because concl((0, ![A]:transitive(subset, power_set(A))), 1) 
% 
% *** explanation : the variables of the conclusion are instantiated
% --------------------------------------------------------- rule(!)
% *** newconcl(0, only(power_set(z1)::A, transitive(subset, A)), 3) 
% 
% *** because concl(0, transitive(subset, power_set(z1)), 2) 
% 
% *** explanation : elimination of the functional symbols of the conclusion 
% for example, p(f(X)) is replaced by only(f(X)::Y, p(Y) 
% --------------------------------------------------------- rule(elifun)
% *** addhyp(0, power_set(z1)::z2, 4), newconcl(0, transitive(subset, z2), 4) 
% 
% *** because concl(0, only(power_set(z1)::A, transitive(subset, A)), 3) 
% 
% *** explanation : creation of object z2 and of its definition 
% --------------------------------------------------------- rule(concl_only)
% *** newconcl(0, ![A, B, C]: (member(A, z2)&member(B, z2)&member(C, z2)=> ..[subset, A|...]& ..[subset, B|...]=> ..[subset, A, C]), 5) 
% 
% *** because concl(0, transitive(subset, z2), 4) 
% 
% *** explanation : the conclusion  transitive(subset, z2) is replaced by its definition(fof transitive ) 
% --------------------------------------------------------- rule(def_concl_pred)
% create object(s) z5 z4 z3  
% *** newconcl(0, member(z3, z2)&member(z4, z2)&member(z5, z2)=> ..[subset, z3, z4]& ..[subset, z4, z5]=> ..[subset, z3, z5], 6) 
% 
% *** because concl((0, ![A, B, C]: (member(A, z2)&member(B, z2)&member(C, z2)=> ..[subset|...]& ..[subset|...]=> ..[subset, A|...])), 5) 
% 
% *** explanation : the variables of the conclusion are instantiated
% --------------------------------------------------------- rule(!)
% *** addhyp(0, member(z3, z2), 7)  
% *** addhyp(0, member(z4, z2), 7)  
% *** addhyp(0, member(z5, z2), 7) 
% *** newconcl(0, ..[subset, z3, z4]& ..[subset, z4, z5]=> ..[subset, z3, z5], 7) 
% 
% *** because concl(0, member(z3, z2)&member(z4, z2)&member(z5, z2)=> ..[subset, z3, z4]& ..[subset, z4, z5]=> ..[subset, z3, z5], 6) 
% 
% *** explanation : to prove H=>C, assume H and prove C
% --------------------------------------------------------- rule(=>)
% *** addhyp(0, ..[subset, z3, z4], 8)  
% *** addhyp(0, ..[subset, z4, z5], 8) 
% *** newconcl(0, ..[subset, z3, z5], 8) 
% 
% *** because concl(0, ..[subset, z3, z4]& ..[subset, z4, z5]=> ..[subset, z3, z5], 7) 
% 
% *** explanation : to prove H=>C, assume H and prove C
% --------------------------------------------------------- rule(=>)
% *** newconcl(0, subset(z3, z5), 9) 
% 
% *** because concl(0, ..[subset, z3, z5], 8) 
% 
% *** explanation : 
% *** because ..[r,a,b] = r(a,b)
% --------------------------------------------------------- rule(..)
% *** newconcl(0, ![A]: (member(A, z3)=>member(A, z5)), 13) 
% 
% *** because concl(0, subset(z3, z5), 9) 
% 
% *** explanation : the conclusion  subset(z3, z5) is replaced by its definition(fof subset ) 
% --------------------------------------------------------- rule(def_concl_pred)
% create object(s) z6  
% *** newconcl(0, member(z6, z3)=>member(z6, z5), 14) 
% 
% *** because concl((0, ![A]: (member(A, z3)=>member(A, z5))), 13) 
% 
% *** explanation : the variables of the conclusion are instantiated
% --------------------------------------------------------- rule(!)
% *** addhyp(0, member(z6, z3), 15) 
% *** newconcl(0, member(z6, z5), 15) 
% 
% *** because concl(0, member(z6, z3)=>member(z6, z5), 14) 
% 
% *** explanation : to prove H=>C, assume H and prove C
% --------------------------------------------------------- rule(=>)
% *** addhyp(0, member(z6, z4), 16) 
% 
% *** because hyp(0, subset(z3, z4), 8), hyp(0, member(z6, z3), 15), obj_cte(0, z6) 
% 
% *** explanation : rule2 if (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))then addhyp(A, member(C, D), _) 
% built from the definition of subset (fof subset ) 
% --------------------------------------------------------- rule(subset)
% *** addhyp(0, member(z6, z5), 17) 
% 
% *** because hyp(0, subset(z4, z5), 8), hyp(0, member(z6, z4), 16), obj_cte(0, z6) 
% 
% *** explanation : rule2 if (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))then addhyp(A, member(C, D), _) 
% built from the definition of subset (fof subset ) 
% --------------------------------------------------------- rule(subset)
% *** newconcl(0, true, 18) 
% 
% *** because hyp(0, member(z6, z5), 17), concl(0, member(z6, z5), 15) 
% 
% *** explanation : the conclusion member(z6, z5) to be proved is a hypothesis 
% --------------------------------------------------------- rule(stop_hyp_concl)
% then the initial theorem is proved
% * * * * * * * * * * * * * * * * * * * * * * * *
% 
% SZS output end proof for problem
%