th3 f(a union b) = f(a) union f(b) -for_all(A, for_all(B, for_all(C, maps(C, A, B)=>for_all(D, for_all(E, image(C, D union E)equal_set image(C, D)union image(C, E)))))). ******************************************************************************** theorem to be proved -for_all(A, for_all(B, for_all(C, maps(C, A, B)=>for_all(D, for_all(E, image(C, D union E)equal_set image(C, D)union image(C, E)))))). 0 new conclusion -for_all(A, for_all(B, for_all(C, maps(C, A, B)=>for_all(D, for_all(E, image(C, D union E)equal_set image(C, D)union image(C, E)))))). 0 add link maps 0 add link equal_set 0 add link image 0 add link union 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 maps maps1 equal_set equal_set1 image image1 union union1 union2 inc and defconcl1 defconcl1a defconcl1b defconcl1bb exists or defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 new conclusion -for_all(A, for_all(B, for_all(C, maps(C, A, B)=>for_all(D, for_all(E, only(D union E:F, only(image(C, F):G, only(image(C, D):H, only(image(C, E):I, only(H union I:J, G equal_set J)))))))))). --------------------------------------------------------- rule elifon 0 add object x 0 new conclusion -for_all(A, for_all(B, maps(B, x, A)=>for_all(C, for_all(D, only(C union D:E, only(image(B, E):F, only(image(B, C):G, only(image(B, D):H, only(G union H:I, F equal_set I))))))))). --------------------------------------------------------- rule for_all1 0 add object x1 0 new conclusion -for_all(A, maps(A, x, x1)=>for_all(B, for_all(C, only(B union C:D, only(image(A, D):E, only(image(A, B):F, only(image(A, C):G, only(F union G:H, E equal_set H)))))))). --------------------------------------------------------- rule for_all1 0 add object x2 0 new conclusion - (maps(x2, x, x1)=>for_all(A, for_all(B, only(A union B:C, only(image(x2, C):D, only(image(x2, A):E, only(image(x2, B):F, only(E union F:G, D equal_set G)))))))). --------------------------------------------------------- rule for_all1 0 add hypothesis maps(x2, x, x1) 0 new conclusion -for_all(A, for_all(B, only(A union B:C, only(image(x2, C):D, only(image(x2, A):E, only(image(x2, B):F, only(E union F:G, D equal_set G))))))). --------------------------------------------------------- rule => 0 add object x3 0 new conclusion -for_all(A, only(x3 union A:B, only(image(x2, B):C, only(image(x2, x3):D, only(image(x2, A):E, only(D union E:F, C equal_set F)))))). --------------------------------------------------------- rule for_all1 0 add object x4 0 new conclusion -only(x3 union x4:A, only(image(x2, A):B, only(image(x2, x3):C, only(image(x2, x4):D, only(C union D:E, B equal_set E))))). --------------------------------------------------------- rule for_all1 0 add object union_x3_x4 0 add hypothesis x3 union x4:union_x3_x4 0 new conclusion -only(image(x2, union_x3_x4):A, only(image(x2, x3):B, only(image(x2, x4):C, only(B union C:D, A equal_set D)))). --------------------------------------------------------- rule only 0 add object image_x2_union_x3_x4 0 add hypothesis image(x2, union_x3_x4):image_x2_union_x3_x4 0 new conclusion -only(image(x2, x3):A, only(image(x2, x4):B, only(A union B:C, image_x2_union_x3_x4 equal_set C))). --------------------------------------------------------- rule only 0 add object image_x2_x3 0 add hypothesis image(x2, x3):image_x2_x3 0 new conclusion -only(image(x2, x4):A, only(image_x2_x3 union A:B, image_x2_union_x3_x4 equal_set B)). --------------------------------------------------------- rule only 0 add object image_x2_x4 0 add hypothesis image(x2, x4):image_x2_x4 0 new conclusion -only(image_x2_x3 union image_x2_x4:A, image_x2_union_x3_x4 equal_set A). --------------------------------------------------------- rule only 0 add object union_image_x2_x3_image_x2_x4 0 add hypothesis image_x2_x3 union image_x2_x4:union_image_x2_x3_image_x2_x4 0 new conclusion image_x2_union_x3_x4 equal_set union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule only 0 definition of the conclusion 0 new conclusion image_x2_union_x3_x4 inc union_image_x2_x3_image_x2_x4 and union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 --------------------------------------------------------- rule defconcl1 ************************************************ sub-theorem 1 ***** 1 new conclusion image_x2_union_x3_x4 inc union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation of sub-theorem 1 1 definition of the conclusion 1 new conclusion -for_all(A, A elt image_x2_union_x3_x4=>A elt union_image_x2_x3_image_x2_x4). --------------------------------------------------------- rule defconcl1 1 add object x5 1 new conclusion x5 elt image_x2_union_x3_x4=>x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule for_all1 1 add hypothesis x5 elt image_x2_union_x3_x4 1 new conclusion x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule => 1 add hypothesis -exists(A elt union_x3_x4, ..[x2, A]:x5). --------------------------------------------------------- rule image 1 add object x6 1 add hypothesis x6 elt union_x3_x4 1 add hypothesis x2(x6):x5 1 add hypothesis-traitee -exists(A elt union_x3_x4, ..[x2, A]:x5). --------------------------------------------------------- rule exists 1 add hypothesis x6 elt x3 or x6 elt x4 --------------------------------------------------------- rule union 1 traitement de l hypothesis disjonctive x6 elt x3 or x6 elt x4 1 new conclusion (x6 elt x3=>x5 elt union_image_x2_x3_image_x2_x4)and (x6 elt x4=>x5 elt union_image_x2_x3_image_x2_x4) 1 add hypothesis-traitee x6 elt x3 or x6 elt x4 --------------------------------------------------------- rule or ************************************************ sub-theorem 11 ***** 11 new conclusion x6 elt x3=>x5 elt union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation of sub-theorem 11 11 add hypothesis x6 elt x3 11 new conclusion x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule => 11 add hypothesis x5 elt image_x2_x3 --------------------------------------------------------- rule image1 11 add hypothesis -exists(A elt x3, ..[x2, A]:x5). --------------------------------------------------------- rule image 11 add hypothesis x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule union1 11 new conclusion true --------------------------------------------------------- rule stop1 theorem 11 proved 1 new conclusion x6 elt x4=>x5 elt union_image_x2_x3_image_x2_x4 ************************************************ sub-theorem 12 ***** 12 new conclusion x6 elt x4=>x5 elt union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation of sub-theorem 12 12 add hypothesis x6 elt x4 12 new conclusion x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule => 12 add hypothesis x5 elt image_x2_x4 --------------------------------------------------------- rule image1 12 add hypothesis -exists(A elt x4, ..[x2, A]:x5). --------------------------------------------------------- rule image 12 add hypothesis x5 elt union_image_x2_x3_image_x2_x4 --------------------------------------------------------- rule union2 12 new conclusion true --------------------------------------------------------- rule stop1 theorem 12 proved 1 new conclusion true --------------------------------------------------------- rule and theorem 1 proved 0 new conclusion union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 ************************************************ sub-theorem 2 ***** 2 new conclusion union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 ----------------------------------------------- creation of sub-theorem 2 2 definition of the conclusion 2 new conclusion -for_all(A, A elt union_image_x2_x3_image_x2_x4=>A elt image_x2_union_x3_x4). --------------------------------------------------------- rule defconcl1 2 add object x7 2 new conclusion x7 elt union_image_x2_x3_image_x2_x4=>x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule for_all1 2 add hypothesis x7 elt union_image_x2_x3_image_x2_x4 2 new conclusion x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule => 2 add hypothesis x7 elt image_x2_x3 or x7 elt image_x2_x4 --------------------------------------------------------- rule union 2 traitement de l hypothesis disjonctive x7 elt image_x2_x3 or x7 elt image_x2_x4 2 new conclusion (x7 elt image_x2_x3=>x7 elt image_x2_union_x3_x4)and (x7 elt image_x2_x4=>x7 elt image_x2_union_x3_x4) 2 add hypothesis-traitee x7 elt image_x2_x3 or x7 elt image_x2_x4 --------------------------------------------------------- rule or ************************************************ sub-theorem 21 ***** 21 new conclusion x7 elt image_x2_x3=>x7 elt image_x2_union_x3_x4 ----------------------------------------------- creation of sub-theorem 21 21 add hypothesis x7 elt image_x2_x3 21 new conclusion x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule => 21 add hypothesis -exists(A elt x3, ..[x2, A]:x7). --------------------------------------------------------- rule image 21 add object x8 21 add hypothesis x8 elt x3 21 add hypothesis x2(x8):x7 21 add hypothesis-traitee -exists(A elt x3, ..[x2, A]:x7). --------------------------------------------------------- rule exists 21 add hypothesis x8 elt union_x3_x4 --------------------------------------------------------- rule union1 21 add hypothesis x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule image1 21 new conclusion true --------------------------------------------------------- rule stop1 theorem 21 proved 2 new conclusion x7 elt image_x2_x4=>x7 elt image_x2_union_x3_x4 ************************************************ sub-theorem 22 ***** 22 new conclusion x7 elt image_x2_x4=>x7 elt image_x2_union_x3_x4 ----------------------------------------------- creation of sub-theorem 22 22 add hypothesis x7 elt image_x2_x4 22 new conclusion x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule => 22 add hypothesis -exists(A elt x4, ..[x2, A]:x7). --------------------------------------------------------- rule image 22 add object x9 22 add hypothesis x9 elt x4 22 add hypothesis x2(x9):x7 22 add hypothesis-traitee -exists(A elt x4, ..[x2, A]:x7). --------------------------------------------------------- rule exists 22 add hypothesis x9 elt union_x3_x4 --------------------------------------------------------- rule union2 22 add hypothesis x7 elt image_x2_union_x3_x4 --------------------------------------------------------- rule image1 22 new conclusion true --------------------------------------------------------- rule stop1 theorem 22 proved 2 new conclusion true --------------------------------------------------------- rule and theorem 2 proved 0 new conclusion true --------------------------------------------------------- rule and theorem 0 proved in 0.57 seconds ================================================================================