th4 belonging to the same element of a partition is an equivalence relation -for_all(A, for_all(B, partition(A, B)=>for_all(C, for_all(D elt B, for_all(E elt B, ..[C, D, E]<=>exists(F elt A, D elt F and E elt F)))=>equiv(B, C)))). ******************************************************************************** theorem to be proved -for_all(A, for_all(B, partition(A, B)=>for_all(C, for_all(D elt B, for_all(E elt B, ..[C, D, E]<=>exists(F elt A, D elt F and E elt F)))=>equiv(B, C)))). 0 new conclusion -for_all(A, for_all(B, partition(A, B)=>for_all(C, for_all(D elt B, for_all(E elt B, ..[C, D, E]<=>exists(F elt A, D elt F and E elt F)))=>equiv(B, C)))). 0 add link equiv 0 add link partition 0 add link inc active rules:elifon stop1 stop2 stop3 stop4 equal equaldef or1 or23 or4 or5 not hypnon hypnonnon hypnonimp hypimp not_or_1 not_or_2 hypequ hypnonequ concl_or_and => <=> for_all1 for_all2 only .. ..1 ilec1 ilec2 ilec3 ilec4 ilec5 ilec1a ilec1b and_trivial_1 and_trivial_2 stop_trivial stop_trivial_or conclet equiv equiv1 equiv2 partition partition1 partition2 inc and defconcl1 defconcl1a defconcl1b defconcl1bb exists or defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 add object x 0 new conclusion -for_all(A, partition(x, A)=>for_all(B, for_all(C elt A, for_all(D elt A, ..[B, C, D]<=>exists(E elt x, C elt E and D elt E)))=>equiv(A, B))). --------------------------------------------------------- rule for_all1 0 add object x1 0 new conclusion - (partition(x, x1)=>for_all(A, for_all(B elt x1, for_all(C elt x1, ..[A, B, C]<=>exists(D elt x, B elt D and C elt D)))=>equiv(x1, A))). --------------------------------------------------------- rule for_all1 0 add hypothesis partition(x, x1) 0 new conclusion -for_all(A, for_all(B elt x1, for_all(C elt x1, ..[A, B, C]<=>exists(D elt x, B elt D and C elt D)))=>equiv(x1, A)). --------------------------------------------------------- rule => 0 add object x2 0 new conclusion - (for_all(A elt x1, for_all(B elt x1, ..[x2, A, B]<=>exists(C elt x, A elt C and B elt C)))=>equiv(x1, x2)). --------------------------------------------------------- rule for_all1 0 add the local rule - (rule(A, rulhyp):-hyp(A, B elt x1), hyp(A, C elt x1), D=..[x2, B, C], hyp(A, D), \+hyp(A, exists(E elt x, B elt E and C elt E)), ajhyp(A, exists(E elt x, B elt E and C elt E))). at the end of universal rules 0 add the local rule - (rule(A, rulhyp1):-hyp(A, B elt x1), hyp(A, C elt x1), hyp(A, D elt x), hyp(A, B elt D), hyp(A, C elt D), E=..[x2, B, C], \+hyp(A, E), ajhyp(A, E)). at the end of universal rules 0 new conclusion equiv(x1, x2) --------------------------------------------------------- rule => 0 definition of the conclusion 0 new conclusion -for_all(A elt x1, ..[x2, A, A])and for_all(A elt x1, for_all(B elt x1, ..[x2, A, B]=> ..[x2, B, A]))and for_all(A elt x1, for_all(B elt x1, for_all(C elt x1, ..[x2, A, B]and..[x2, B, C]=> ..[x2, A, C]))). --------------------------------------------------------- rule defconcl1 ************************************************ sub-theorem 1 ***** 1 new conclusion -for_all(A elt x1, ..[x2, A, A]). ----------------------------------------------- creation of sub-theorem 1 1 add object x3 1 add hypothesis x3 elt x1 1 new conclusion ..[x2, x3, x3] --------------------------------------------------------- rule for_all2 1 new conclusion x2(x3, x3) --------------------------------------------------------- rule .. 1 add hypothesis -exists(A elt x, x3 elt A). --------------------------------------------------------- rule partition1 1 add object x4 1 add hypothesis x4 elt x 1 add hypothesis x3 elt x4 1 add hypothesis-traitee -exists(A elt x, x3 elt A). --------------------------------------------------------- rule exists 1 add hypothesis x2(x3, x3) --------------------------------------------------------- rule rulhyp1 1 new conclusion true --------------------------------------------------------- rule stop1 theorem 1 proved 0 new conclusion -for_all(A elt x1, for_all(B elt x1, ..[x2, A, B]=> ..[x2, B, A]))and for_all(A elt x1, for_all(B elt x1, for_all(C elt x1, ..[x2, A, B]and..[x2, B, C]=> ..[x2, A, C]))). ************************************************ sub-theorem 2 ***** 2 new conclusion -for_all(A elt x1, for_all(B elt x1, ..[x2, A, B]=> ..[x2, B, A])). ----------------------------------------------- creation of sub-theorem 2 2 add object x5 2 add hypothesis x5 elt x1 2 new conclusion -for_all(A elt x1, ..[x2, x5, A]=> ..[x2, A, x5]). --------------------------------------------------------- rule for_all2 2 add object x6 2 add hypothesis x6 elt x1 2 new conclusion ..[x2, x5, x6]=> ..[x2, x6, x5] --------------------------------------------------------- rule for_all2 2 add hypothesis x2(x5, x6) 2 new conclusion ..[x2, x6, x5] --------------------------------------------------------- rule => 2 new conclusion x2(x6, x5) --------------------------------------------------------- rule .. 2 add hypothesis -exists(A elt x, x5 elt A and x6 elt A). --------------------------------------------------------- rule rulhyp 2 add hypothesis -exists(A elt x, x5 elt A). --------------------------------------------------------- rule partition1 2 add hypothesis -exists(A elt x, x6 elt A). --------------------------------------------------------- rule partition1 2 add object x7 2 add hypothesis x7 elt x 2 add hypothesis x5 elt x7 2 add hypothesis x6 elt x7 2 add hypothesis-traitee -exists(A elt x, x5 elt A and x6 elt A). --------------------------------------------------------- rule exists 2 add hypothesis x2(x5, x5) --------------------------------------------------------- rule rulhyp1 2 add hypothesis x2(x6, x5) --------------------------------------------------------- rule rulhyp1 2 new conclusion true --------------------------------------------------------- rule stop1 theorem 2 proved 0 new conclusion -for_all(A elt x1, for_all(B elt x1, for_all(C elt x1, ..[x2, A, B]and..[x2, B, C]=> ..[x2, A, C]))). ************************************************ sub-theorem 3 ***** 3 new conclusion -for_all(A elt x1, for_all(B elt x1, for_all(C elt x1, ..[x2, A, B]and..[x2, B, C]=> ..[x2, A, C]))). ----------------------------------------------- creation of sub-theorem 3 3 add object x8 3 add hypothesis x8 elt x1 3 new conclusion -for_all(A elt x1, for_all(B elt x1, ..[x2, x8, A]and..[x2, A, B]=> ..[x2, x8, B])). --------------------------------------------------------- rule for_all2 3 add object x9 3 add hypothesis x9 elt x1 3 new conclusion -for_all(A elt x1, ..[x2, x8, x9]and..[x2, x9, A]=> ..[x2, x8, A]). --------------------------------------------------------- rule for_all2 3 add object x10 3 add hypothesis x10 elt x1 3 new conclusion ..[x2, x8, x9]and..[x2, x9, x10]=> ..[x2, x8, x10] --------------------------------------------------------- rule for_all2 3 add hypothesis x2(x8, x9) 3 add hypothesis x2(x9, x10) 3 new conclusion ..[x2, x8, x10] --------------------------------------------------------- rule => 3 new conclusion x2(x8, x10) --------------------------------------------------------- rule .. 3 add hypothesis -exists(A elt x, x8 elt A and x9 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis -exists(A elt x, x9 elt A and x10 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis -exists(A elt x, x8 elt A). --------------------------------------------------------- rule partition1 3 add hypothesis -exists(A elt x, x9 elt A). --------------------------------------------------------- rule partition1 3 add hypothesis -exists(A elt x, x10 elt A). --------------------------------------------------------- rule partition1 3 add object x11 3 add hypothesis x11 elt x 3 add hypothesis x8 elt x11 3 add hypothesis x9 elt x11 3 add hypothesis-traitee -exists(A elt x, x8 elt A and x9 elt A). --------------------------------------------------------- rule exists 3 add hypothesis x2(x8, x8) --------------------------------------------------------- rule rulhyp1 3 add hypothesis x2(x9, x8) --------------------------------------------------------- rule rulhyp1 3 add hypothesis x2(x9, x9) --------------------------------------------------------- rule rulhyp1 3 add hypothesis -exists(A elt x, x8 elt A and x8 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis -exists(A elt x, x9 elt A and x8 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis -exists(A elt x, x9 elt A and x9 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis x11 inc x1 --------------------------------------------------------- rule partition 3 add object x12 3 add hypothesis x12 elt x 3 add hypothesis x9 elt x12 3 add hypothesis x10 elt x12 3 add hypothesis-traitee -exists(A elt x, x9 elt A and x10 elt A). --------------------------------------------------------- rule exists 3 add hypothesis x2(x10, x9) --------------------------------------------------------- rule rulhyp1 3 add hypothesis x2(x10, x10) --------------------------------------------------------- rule rulhyp1 3 add hypothesis -exists(A elt x, x10 elt A and x9 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis -exists(A elt x, x10 elt A and x10 elt A). --------------------------------------------------------- rule rulhyp 3 add hypothesis x12 inc x1 --------------------------------------------------------- rule partition 3 add hypothesis x11=x12 --------------------------------------------------------- rule partition2 remplacer x12 par x11 propager and remove x12 3 add hypothesis x10 elt x11 remove hypothesis x11=x12 remove object x12 --------------------------------------------------------- rule equal 3 add hypothesis x2(x8, x10) --------------------------------------------------------- rule rulhyp1 3 new conclusion true --------------------------------------------------------- rule stop1 theorem 3 proved 0 new conclusion true --------------------------------------------------------- rule and theorem 0 proved in 1.03 seconds ================================================================================