WATCH: 0.00 CPU 0.01 WC

/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p 300 sec                         

SZS status Theorem for FEQ005.p

SZS output start proof for FEQ005.p

* * * * * * * * * * * * * * * * * * * * * * * *
in the following, N is the number of a (sub)theorem
       E is the current step
         or the step when a hypothesis or conclusion has been added or modified
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_ct(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 N-i or N+i is a subtheorem of the (sub)theorem N
   N is proved if all N-i have been proved (&-node)
             or if one N+i have been proved (|-node)
the initial theorem is numbered 0

* * * theorem to be proved
?[D]:![C]: (?[B]:![A]: (A=B<=>big_f(A,C))<=>C=D)

* * * proof :

* * * * * * theoreme 0 * * * * * *
*** newconcl(0,?[D]:![C]: (?[B]:![A]: (A=B<=>big_f(A,C))<=>C=D),1) 
*** explanation : initial theorem
------------------------------------------------------- action ini 
*** addhyp(0,?[C,B]:![D,A]: (A=B&C=D<=>big_f(D,A)),2) 
*** explanation : rule addhyp(_,?[C,B]:![D,A]: (A=B&C=D<=>big_f(D,A)),_) 
built from the axiom pel52_1 
------------------------------------------------------- rule pel52_1_exist 
create object(s) z2 z1  
*** addhyp(0,![B,A]: (A=z2&z1=B<=>big_f(B,A)),3) 
*** because hyp(0,?[C,B]:![D,A]: (A=B&C=D<=>big_f(D,A)),2) 
*** explanation : treatment of the existential hypothesis
------------------------------------------------------- rule hyp_exi 
*** addhyp(0,big_f(z1,z2),4) 
*** because obj_ct(0,z1),obj_ct(0,z2) 
*** explanation : the rule r_hyp__3__ : if (obj_ct(A,z1),obj_ct(A,z2))then addhyp(A,big_f(z1,z2),_) 
is a local rule built from the universal hypothesis ![B,A]: (A=z2&z1=B<=>big_f(B,A)) 
------------------------------------------------------- rule r_hyp__3__ 

* * * * * * creation * * * * * * sub-theoreme 0+2 * * * * * 
all the hypotheses of (sub)theorem 0 are hypotheses of subtheorem 0+2 
*** newconcl(0+2,![C]: (?[B]:![A]: (A=B<=>big_f(A,C))<=>C=z2),19) 
*** because concl(0,?[D]:![C]: (?[B]:![A]: (A=B<=>big_f(A,C))<=>C=D),1) 
*** explanation : z2 is tried for the existential variable 
------------------------------------------------------- action proconclexi 
create object(s) z6  
*** newconcl(0+2,?[B]:![A]: (A=B<=>big_f(A,z6))<=>z6=z2,20) 
*** because concl((0,![C]: (?[B]:![A]: (A=B<=>big_f(A,C))<=>C=z2)),19) 
*** explanation : the universal variable(s) of the conclusion is(are) instantiated
------------------------------------------------------- rule ! 
*** newconcl(0+2, (?[B]:![A]: (A=B<=>big_f(A,z6))=>z6=z2)& (z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6)))) 
*** because concl(0+2,?[B]:![A]: (A=B<=>big_f(A,z6))<=>z6=z2,20) 
*** explanation : A<=>B is replaced by (A=>B)&(B=>A)
------------------------------------------------------- rule <=> 

* * * * * * creation * * * * * * sub-theoreme 0+2-1 * * * * * 
all the hypotheses of (sub)theorem 0+2 are hypotheses of subtheorem 0+2-1 
*** newconcl(0+2-1,?[B]:![A]: (A=B<=>big_f(A,z6))=>z6=z2,22) 
*** because concl(0+2, (?[B]:![A]: (A=B<=>big_f(A,z6))=>z6=z2)& (z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6))),21) 
*** explanation : to prove a conjunction, prove all the elements of the conjunction
------------------------------------------------------- action proconj 
*** addhyp(0+2-1,?[B]:![A]: (A=B<=>big_f(A,z6)),23) 
*** newconcl(0+2-1,z6=z2,23) 
*** because concl(0+2-1,?[B]:![A]: (A=B<=>big_f(A,z6))=>z6=z2,22) 
*** explanation : to prove H=>C, assume H and prove C
------------------------------------------------------- rule => 
create object(s) z7  
*** addhyp(0+2-1,![A]: (A=z7<=>big_f(A,z6)),24) 
*** because hyp(0+2-1,?[B]:![A]: (A=B<=>big_f(A,z6)),23) 
*** explanation : treatment of the existential hypothesis
------------------------------------------------------- rule hyp_exi 
*** addhyp(0+2-1,big_f(z7,z6),25) 
*** because obj_ct(0+2-1,z7) 
*** explanation : the rule r_hyp__24__ : if obj_ct(A,z7)then addhyp(A,big_f(z7,z6),_) 
is a local rule built from the universal hypothesis ![A]: (A=z7<=>big_f(A,z6)) 
------------------------------------------------------- rule r_hyp__24__ 
*** addhyp(0+2-1,z1=z7,26) 
*** because hyp(0+2-1,big_f(z7,z6),25),obj_ct(0+2-1,z7),obj_ct(0+2-1,z6) 
*** explanation : the rule r_hyp__3__2 : if (hyp(A,big_f(B,C),_),obj_ct(A,B),obj_ct(A,C))then addhyp(A,z1=B,_) 
is a local rule built from the universal hypothesis ![B,A]: (A=z2&z1=B<=>big_f(B,A)) 
------------------------------------------------------- rule r_hyp__3__2 
*** addhyp(0+2-1,big_f(z1,z6),27) 
*** because hyp(0+2-1,z1=z7,26),hyp(0+2-1,big_f(z7,z6),25) 
*** explanation : z7 is replaced by z1 in the hypotheses 
------------------------------------------------------- treatequal_hyp
*** addhyp(0+2-1,z6=z2,28) 
*** because hyp(0+2-1,big_f(z1,z6),27),obj_ct(0+2-1,z1),obj_ct(0+2-1,z6) 
*** explanation : the rule r_hyp__3__1 : if (hyp(A,big_f(B,C),_),obj_ct(A,B),obj_ct(A,C))then addhyp(A,C=z2,_) 
is a local rule built from the universal hypothesis ![B,A]: (A=z2&z1=B<=>big_f(B,A)) 
------------------------------------------------------- rule r_hyp__3__1 
*** newconcl(0+2-1,z2=z2,30) 
*** because hyp(0+2-1,z2=z6,28),concl(0+2-1,z6=z2,23) 
*** explanation : z6 is replaced by z2 in the conclusion 
------------------------------------------------------- action treatequal_concl 
*** newconcl(0+2-1,true,31) 
*** because concl(0+2-1,z2=z2,30) 
*** explanation : trivial conclusion
------------------------------------------------------- rule concl_stop_trivial 
*** newconcl(0+2,z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6)),32) 
*** because concl(0+2-1,true,31) 
*** explanation : the conclusion ?[B]:![A]: (A=B<=>big_f(A,z6))=>z6=z2 of (sub)theorem 0+2 has been proved ( subtheorem/ 0+2-1 ) 
------------------------------------------------------- action returnpro 

* * * * * * creation * * * * * * sub-theoreme 0+2-2 * * * * * 
all the hypotheses of (sub)theorem 0+2 are hypotheses of subtheorem 0+2-2 
*** newconcl(0+2-2,z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6)),33) 
*** explanation : proof of the last element of the conjunction
------------------------------------------------------- action proconj 
*** addhyp(0+2-2,z6=z2,34) 
*** newconcl(0+2-2,?[B]:![A]: (A=B<=>big_f(A,z6)),34) 
*** because concl(0+2-2,z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6)),33) 
*** explanation : to prove H=>C, assume H and prove C
------------------------------------------------------- rule => 
*** newconcl(0+2-2,?[B]:![A]: (A=B<=>big_f(A,z2)),35) 
*** because hyp(0+2-2,z2=z6,34),concl(0+2-2,?[B]:![A]: (A=B<=>big_f(A,z6)),34) 
*** explanation : z6 is replaced by z2 in the conclusion 
------------------------------------------------------- action treatequal_concl 

* * * * * * creation * * * * * * sub-theoreme 0+2-2+1 * * * * * 
all the hypotheses of (sub)theorem 0+2-2 are hypotheses of subtheorem 0+2-2+1 
*** newconcl(0+2-2+1,![A]: (A=z1<=>big_f(A,z2)),36) 
*** because concl(0+2-2,?[B]:![A]: (A=B<=>big_f(A,z2)),35) 
*** explanation : z1 is tried for the existential variable 
------------------------------------------------------- action proconclexi 
create object(s) z8  
*** newconcl(0+2-2+1,z8=z1<=>big_f(z8,z2),37) 
*** because concl((0,![A]: (A=z1<=>big_f(A,z2))),36) 
*** explanation : the universal variable(s) of the conclusion is(are) instantiated
------------------------------------------------------- rule ! 
*** newconcl(0+2-2+1, (z8=z1=>big_f(z8,z2))& (big_f(z8,z2)=>z8=z1)) 
*** because concl(0+2-2+1,z8=z1<=>big_f(z8,z2),37) 
*** explanation : A<=>B is replaced by (A=>B)&(B=>A)
------------------------------------------------------- rule <=> 

* * * * * * creation * * * * * * sub-theoreme 0+2-2+1-1 * * * * * 
all the hypotheses of (sub)theorem 0+2-2+1 are hypotheses of subtheorem 0+2-2+1-1 
*** newconcl(0+2-2+1-1,z8=z1=>big_f(z8,z2),39) 
*** because concl(0+2-2+1, (z8=z1=>big_f(z8,z2))& (big_f(z8,z2)=>z8=z1),38) 
*** explanation : to prove a conjunction, prove all the elements of the conjunction
------------------------------------------------------- action proconj 
*** addhyp(0+2-2+1-1,z8=z1,40) 
*** newconcl(0+2-2+1-1,big_f(z8,z2),40) 
*** because concl(0+2-2+1-1,z8=z1=>big_f(z8,z2),39) 
*** explanation : to prove H=>C, assume H and prove C
------------------------------------------------------- rule => 
*** newconcl(0+2-2+1-1,big_f(z1,z2),41) 
*** because hyp(0+2-2+1-1,z1=z8,40),concl(0+2-2+1-1,big_f(z8,z2),40) 
*** explanation : z8 is replaced by z1 in the conclusion 
------------------------------------------------------- action treatequal_concl 
*** newconcl(0+2-2+1-1,true,42) 
*** because hyp(0+2-2+1-1,big_f(z1,z2),4),concl(0+2-2+1-1,big_f(z1,z2),41) 
*** explanation : the conclusion big_f(z1,z2) to be proved is a hypothesis 
------------------------------------------------------- rule stop_hyp_concl 
*** newconcl(0+2-2+1,big_f(z8,z2)=>z8=z1,43) 
*** because concl(0+2-2+1-1,true,42) 
*** explanation : the conclusion z8=z1=>big_f(z8,z2) of (sub)theorem 0+2-2+1 has been proved ( subtheorem/ 0+2-2+1-1 ) 
------------------------------------------------------- action returnpro 

* * * * * * creation * * * * * * sub-theoreme 0+2-2+1-2 * * * * * 
all the hypotheses of (sub)theorem 0+2-2+1 are hypotheses of subtheorem 0+2-2+1-2 
*** newconcl(0+2-2+1-2,big_f(z8,z2)=>z8=z1,44) 
*** explanation : proof of the last element of the conjunction
------------------------------------------------------- action proconj 
*** addhyp(0+2-2+1-2,big_f(z8,z2),45) 
*** newconcl(0+2-2+1-2,z8=z1,45) 
*** because concl(0+2-2+1-2,big_f(z8,z2)=>z8=z1,44) 
*** explanation : to prove H=>C, assume H and prove C
------------------------------------------------------- rule => 
*** addhyp(0+2-2+1-2,z1=z8,46) 
*** because hyp(0+2-2+1-2,big_f(z8,z2),45),obj_ct(0+2-2+1-2,z8),obj_ct(0+2-2+1-2,z2) 
*** explanation : the rule r_hyp__3__2 : if (hyp(A,big_f(B,C),_),obj_ct(A,B),obj_ct(A,C))then addhyp(A,z1=B,_) 
is a local rule built from the universal hypothesis ![B,A]: (A=z2&z1=B<=>big_f(B,A)) 
------------------------------------------------------- rule r_hyp__3__2 
*** newconcl(0+2-2+1-2,z1=z1,47) 
*** because hyp(0+2-2+1-2,z1=z8,46),concl(0+2-2+1-2,z8=z1,45) 
*** explanation : z8 is replaced by z1 in the conclusion 
------------------------------------------------------- action treatequal_concl 
*** newconcl(0+2-2+1-2,true,48) 
*** because concl(0+2-2+1-2,z1=z1,47) 
*** explanation : trivial conclusion
------------------------------------------------------- rule concl_stop_trivial 
*** newconcl(0+2-2+1,true,49) 
*** because concl(0+2-2+1-2,true,48) 
*** explanation : the conclusion big_f(z8,z2)=>z8=z1 of (sub)theorem 0+2-2+1 has been proved ( subtheorem/ 0+2-2+1-2 ) 
------------------------------------------------------- action returnpro 
*** newconcl(0+2-2,true,50) 
*** because concl(0+2-2+1,true,49) 
*** explanation : the conclusion of subtheorem 0+2-2 has been proved (subtheorem 0+2-2+1 ) 
------------------------------------------------------- action returnproexi 
*** newconcl(0+2,true,51) 
*** because concl(0+2-2,true,50) 
*** explanation : the conclusion z6=z2=> ?[B]:![A]: (A=B<=>big_f(A,z6)) of (sub)theorem 0+2 has been proved ( subtheorem/ 0+2-2 ) 
------------------------------------------------------- action returnpro 
*** newconcl(0,true,52) 
*** because concl(0+2,true,51) 
*** explanation : the conclusion of subtheorem 0 has been proved (subtheorem 0+2 ) 
------------------------------------------------------- action returnproexi 
then the initial theorem is proved
* * * * * * * * * * * * * * * * * * * * * * * *

SZS output end proof for FEQ005.p

0.06 sec 
WATCH: 0.09 CPU 0.14 WC

FINAL WATCH: 0.09 CPU 0.14 WC