th2 powerset(a inter b) = powerset(a) inter powerset(b) -for_all(A, for_all(B, powerset(A inter B)equal_set powerset(A)inter powerset(B))). ******************************************************************************** theorem to be proved -for_all(A, for_all(B, powerset(A inter B)equal_set powerset(A)inter powerset(B))). 0 new conclusion -for_all(A, for_all(B, powerset(A inter B)equal_set powerset(A)inter powerset(B))). 0 add link equal_set 0 add link powerset 0 add link inter 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 equal_set equal_set1 powerset powerset1 inter inter1 inter2 inc and defconcl1 defconcl1a defconcl1b defconcl1bb exists or defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 new conclusion -for_all(A, for_all(B, only(A inter B:C, only(powerset(C):D, only(powerset(A):E, only(powerset(B):F, only(E inter F:G, D equal_set G))))))). --------------------------------------------------------- rule elifon 0 add object x 0 new conclusion -for_all(A, only(x inter A:B, only(powerset(B):C, only(powerset(x):D, only(powerset(A):E, only(D inter E:F, C equal_set F)))))). --------------------------------------------------------- rule for_all1 0 add object x1 0 new conclusion -only(x inter x1:A, only(powerset(A):B, only(powerset(x):C, only(powerset(x1):D, only(C inter D:E, B equal_set E))))). --------------------------------------------------------- rule for_all1 0 add object inter_x_x1 0 add hypothesis x inter x1:inter_x_x1 0 new conclusion -only(powerset(inter_x_x1):A, only(powerset(x):B, only(powerset(x1):C, only(B inter C:D, A equal_set D)))). --------------------------------------------------------- rule only 0 add object powerset_inter_x_x1 0 add hypothesis powerset(inter_x_x1):powerset_inter_x_x1 0 new conclusion -only(powerset(x):A, only(powerset(x1):B, only(A inter B:C, powerset_inter_x_x1 equal_set C))). --------------------------------------------------------- rule only 0 add object powerset_x 0 add hypothesis powerset(x):powerset_x 0 new conclusion -only(powerset(x1):A, only(powerset_x inter A:B, powerset_inter_x_x1 equal_set B)). --------------------------------------------------------- rule only 0 add object powerset_x1 0 add hypothesis powerset(x1):powerset_x1 0 new conclusion -only(powerset_x inter powerset_x1:A, powerset_inter_x_x1 equal_set A). --------------------------------------------------------- rule only 0 add object inter_powerset_x_powerset_x1 0 add hypothesis powerset_x inter powerset_x1:inter_powerset_x_powerset_x1 0 new conclusion powerset_inter_x_x1 equal_set inter_powerset_x_powerset_x1 --------------------------------------------------------- rule only 0 definition of the conclusion 0 new conclusion powerset_inter_x_x1 inc inter_powerset_x_powerset_x1 and inter_powerset_x_powerset_x1 inc powerset_inter_x_x1 --------------------------------------------------------- rule defconcl1 ************************************************ sub-theorem 1 ***** 1 new conclusion powerset_inter_x_x1 inc inter_powerset_x_powerset_x1 ----------------------------------------------- creation of sub-theorem 1 1 definition of the conclusion 1 new conclusion -for_all(A, A elt powerset_inter_x_x1=>A elt inter_powerset_x_powerset_x1). --------------------------------------------------------- rule defconcl1 1 add object x2 1 new conclusion x2 elt powerset_inter_x_x1=>x2 elt inter_powerset_x_powerset_x1 --------------------------------------------------------- rule for_all1 1 add hypothesis x2 elt powerset_inter_x_x1 1 new conclusion x2 elt inter_powerset_x_powerset_x1 --------------------------------------------------------- rule => 1 add hypothesis x2 inc inter_x_x1 --------------------------------------------------------- rule powerset definition de la conclusion 1 new conclusion x2 elt powerset_x and x2 elt powerset_x1 --------------------------------------------------------- rule defconcl2app ************************************************ sub-theorem 11 ***** 11 new conclusion x2 elt powerset_x ----------------------------------------------- creation of sub-theorem 11 definition de la conclusion 11 new conclusion x2 inc x --------------------------------------------------------- rule defconcl2app 11 definition of the conclusion 11 new conclusion -for_all(A, A elt x2=>A elt x). --------------------------------------------------------- rule defconcl1 11 add object x3 11 new conclusion x3 elt x2=>x3 elt x --------------------------------------------------------- rule for_all1 11 add hypothesis x3 elt x2 11 new conclusion x3 elt x --------------------------------------------------------- rule => 11 add hypothesis x3 elt inter_x_x1 --------------------------------------------------------- rule inc 11 add hypothesis x3 elt x --------------------------------------------------------- rule inter 11 new conclusion true --------------------------------------------------------- rule stop1 theorem 11 proved 1 new conclusion x2 elt powerset_x1 ************************************************ sub-theorem 12 ***** 12 new conclusion x2 elt powerset_x1 ----------------------------------------------- creation of sub-theorem 12 definition de la conclusion 12 new conclusion x2 inc x1 --------------------------------------------------------- rule defconcl2app 12 definition of the conclusion 12 new conclusion -for_all(A, A elt x2=>A elt x1). --------------------------------------------------------- rule defconcl1 12 add object x4 12 new conclusion x4 elt x2=>x4 elt x1 --------------------------------------------------------- rule for_all1 12 add hypothesis x4 elt x2 12 new conclusion x4 elt x1 --------------------------------------------------------- rule => 12 add hypothesis x4 elt inter_x_x1 --------------------------------------------------------- rule inc 12 add hypothesis x4 elt x --------------------------------------------------------- rule inter 12 add hypothesis x4 elt x1 --------------------------------------------------------- rule inter1 12 new conclusion true --------------------------------------------------------- rule stop1 theorem 12 proved 1 new conclusion true --------------------------------------------------------- rule and theorem 1 proved 0 new conclusion inter_powerset_x_powerset_x1 inc powerset_inter_x_x1 ************************************************ sub-theorem 2 ***** 2 new conclusion inter_powerset_x_powerset_x1 inc powerset_inter_x_x1 ----------------------------------------------- creation of sub-theorem 2 2 definition of the conclusion 2 new conclusion -for_all(A, A elt inter_powerset_x_powerset_x1=>A elt powerset_inter_x_x1). --------------------------------------------------------- rule defconcl1 2 add object x5 2 new conclusion x5 elt inter_powerset_x_powerset_x1=>x5 elt powerset_inter_x_x1 --------------------------------------------------------- rule for_all1 2 add hypothesis x5 elt inter_powerset_x_powerset_x1 2 new conclusion x5 elt powerset_inter_x_x1 --------------------------------------------------------- rule => 2 add hypothesis x5 elt powerset_x --------------------------------------------------------- rule inter 2 add hypothesis x5 inc x --------------------------------------------------------- rule powerset 2 add hypothesis x5 elt powerset_x1 --------------------------------------------------------- rule inter1 2 add hypothesis x5 inc x1 --------------------------------------------------------- rule powerset definition de la conclusion 2 new conclusion x5 inc inter_x_x1 --------------------------------------------------------- rule defconcl2app 2 definition of the conclusion 2 new conclusion -for_all(A, A elt x5=>A elt inter_x_x1). --------------------------------------------------------- rule defconcl1 2 add object x6 2 new conclusion x6 elt x5=>x6 elt inter_x_x1 --------------------------------------------------------- rule for_all1 2 add hypothesis x6 elt x5 2 new conclusion x6 elt inter_x_x1 --------------------------------------------------------- rule => 2 add hypothesis x6 elt x --------------------------------------------------------- rule inc 2 add hypothesis x6 elt x1 --------------------------------------------------------- rule inc 2 add hypothesis x6 elt inter_x_x1 --------------------------------------------------------- rule inter2 2 new conclusion true --------------------------------------------------------- rule stop1 theorem 2 proved 0 new conclusion true --------------------------------------------------------- rule and theorem 0 proved in 0.5 seconds ================================================================================