th3 f(a union b) = f(a) union f(b) -qqs(A, qqs(B, qqs(C, application(C, A, B)=>qqs(D, qqs(E, image(C, D union E)egal_ens image(C, D)union image(C, E)))))). ******************************************************************************** theoreme a demontrer -qqs(A, qqs(B, qqs(C, application(C, A, B)=>qqs(D, qqs(E, image(C, D union E)egal_ens image(C, D)union image(C, E)))))). 0 nouvelle conclusion -qqs(A, qqs(B, qqs(C, application(C, A, B)=>qqs(D, qqs(E, image(C, D union E)egal_ens image(C, D)union image(C, E)))))). 0 ajouter lien application 0 ajouter lien egal_ens 0 ajouter lien image 0 ajouter lien union 0 ajouter lien inc regles actives:elifon stop1 stop2 stop3 stop4 egal egaldef ou1 ou23 ou4 ou5 non hypnon hypnonnon hypnonimp hypimp non_ou_1 non_ou_2 hypequ hypnonequ concl_ou_et => <=> qqs1 qqs2 seul .. ..1 ilec1 ilec2 ilec3 ilec4 ilec5 ilec1a ilec1b et_trivial_1 et_trivial_2 stop_trivial stop_trivial_ou conclet application application1 egal_ens egal_ens1 image image1 union union1 union2 inc et defconcl1 defconcl1a defconcl1b defconcl1bb ilexiste ou defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 nouvelle conclusion -qqs(A, qqs(B, qqs(C, application(C, A, B)=>qqs(D, qqs(E, seul(D union E:F, seul(image(C, F):G, seul(image(C, D):H, seul(image(C, E):I, seul(H union I:J, G egal_ens J)))))))))). --------------------------------------------------------- regle elifon 0 ajouter objet x 0 nouvelle conclusion -qqs(A, qqs(B, application(B, x, A)=>qqs(C, qqs(D, seul(C union D:E, seul(image(B, E):F, seul(image(B, C):G, seul(image(B, D):H, seul(G union H:I, F egal_ens I))))))))). --------------------------------------------------------- regle qqs1 0 ajouter objet x1 0 nouvelle conclusion -qqs(A, application(A, x, x1)=>qqs(B, qqs(C, seul(B union C:D, seul(image(A, D):E, seul(image(A, B):F, seul(image(A, C):G, seul(F union G:H, E egal_ens H)))))))). --------------------------------------------------------- regle qqs1 0 ajouter objet x2 0 nouvelle conclusion - (application(x2, x, x1)=>qqs(A, qqs(B, seul(A union B:C, seul(image(x2, C):D, seul(image(x2, A):E, seul(image(x2, B):F, seul(E union F:G, D egal_ens G)))))))). --------------------------------------------------------- regle qqs1 0 ajouter hypothese application(x2, x, x1) 0 nouvelle conclusion -qqs(A, qqs(B, seul(A union B:C, seul(image(x2, C):D, seul(image(x2, A):E, seul(image(x2, B):F, seul(E union F:G, D egal_ens G))))))). --------------------------------------------------------- regle => 0 ajouter objet x3 0 nouvelle conclusion -qqs(A, seul(x3 union A:B, seul(image(x2, B):C, seul(image(x2, x3):D, seul(image(x2, A):E, seul(D union E:F, C egal_ens F)))))). --------------------------------------------------------- regle qqs1 0 ajouter objet x4 0 nouvelle conclusion -seul(x3 union x4:A, seul(image(x2, A):B, seul(image(x2, x3):C, seul(image(x2, x4):D, seul(C union D:E, B egal_ens E))))). --------------------------------------------------------- regle qqs1 0 ajouter objet union_x3_x4 0 ajouter hypothese x3 union x4:union_x3_x4 0 nouvelle conclusion -seul(image(x2, union_x3_x4):A, seul(image(x2, x3):B, seul(image(x2, x4):C, seul(B union C:D, A egal_ens D)))). --------------------------------------------------------- regle seul 0 ajouter objet image_x2_union_x3_x4 0 ajouter hypothese image(x2, union_x3_x4):image_x2_union_x3_x4 0 nouvelle conclusion -seul(image(x2, x3):A, seul(image(x2, x4):B, seul(A union B:C, image_x2_union_x3_x4 egal_ens C))). --------------------------------------------------------- regle seul 0 ajouter objet image_x2_x3 0 ajouter hypothese image(x2, x3):image_x2_x3 0 nouvelle conclusion -seul(image(x2, x4):A, seul(image_x2_x3 union A:B, image_x2_union_x3_x4 egal_ens B)). --------------------------------------------------------- regle seul 0 ajouter objet image_x2_x4 0 ajouter hypothese image(x2, x4):image_x2_x4 0 nouvelle conclusion -seul(image_x2_x3 union image_x2_x4:A, image_x2_union_x3_x4 egal_ens A). --------------------------------------------------------- regle seul 0 ajouter objet union_image_x2_x3_image_x2_x4 0 ajouter hypothese image_x2_x3 union image_x2_x4:union_image_x2_x3_image_x2_x4 0 nouvelle conclusion image_x2_union_x3_x4 egal_ens union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle seul 0 definition de la conclusion 0 nouvelle conclusion image_x2_union_x3_x4 inc union_image_x2_x3_image_x2_x4 et union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 --------------------------------------------------------- regle defconcl1 ************************************************ sous-theoreme 1 ***** 1 nouvelle conclusion image_x2_union_x3_x4 inc union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation du sous-theoreme 1 1 definition de la conclusion 1 nouvelle conclusion -qqs(A, A app image_x2_union_x3_x4=>A app union_image_x2_x3_image_x2_x4). --------------------------------------------------------- regle defconcl1 1 ajouter objet x5 1 nouvelle conclusion x5 app image_x2_union_x3_x4=>x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle qqs1 1 ajouter hypothese x5 app image_x2_union_x3_x4 1 nouvelle conclusion x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle => 1 ajouter hypothese -ilexiste(A app union_x3_x4, ..[x2, A]:x5). --------------------------------------------------------- regle image 1 ajouter objet x6 1 ajouter hypothese x6 app union_x3_x4 1 ajouter hypothese x2(x6):x5 1 ajouter hypothese-traitee -ilexiste(A app union_x3_x4, ..[x2, A]:x5). --------------------------------------------------------- regle ilexiste 1 ajouter hypothese x6 app x3 ou x6 app x4 --------------------------------------------------------- regle union 1 traitement de l hypothese disjonctive x6 app x3 ou x6 app x4 1 nouvelle conclusion (x6 app x3=>x5 app union_image_x2_x3_image_x2_x4)et (x6 app x4=>x5 app union_image_x2_x3_image_x2_x4) 1 ajouter hypothese-traitee x6 app x3 ou x6 app x4 --------------------------------------------------------- regle ou ************************************************ sous-theoreme 11 ***** 11 nouvelle conclusion x6 app x3=>x5 app union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation du sous-theoreme 11 11 ajouter hypothese x6 app x3 11 nouvelle conclusion x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle => 11 ajouter hypothese x5 app image_x2_x3 --------------------------------------------------------- regle image1 11 ajouter hypothese -ilexiste(A app x3, ..[x2, A]:x5). --------------------------------------------------------- regle image 11 ajouter hypothese x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle union1 11 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 11 demontre 1 nouvelle conclusion x6 app x4=>x5 app union_image_x2_x3_image_x2_x4 ************************************************ sous-theoreme 12 ***** 12 nouvelle conclusion x6 app x4=>x5 app union_image_x2_x3_image_x2_x4 ----------------------------------------------- creation du sous-theoreme 12 12 ajouter hypothese x6 app x4 12 nouvelle conclusion x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle => 12 ajouter hypothese x5 app image_x2_x4 --------------------------------------------------------- regle image1 12 ajouter hypothese -ilexiste(A app x4, ..[x2, A]:x5). --------------------------------------------------------- regle image 12 ajouter hypothese x5 app union_image_x2_x3_image_x2_x4 --------------------------------------------------------- regle union2 12 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 12 demontre 1 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 1 demontre 0 nouvelle conclusion union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 ************************************************ sous-theoreme 2 ***** 2 nouvelle conclusion union_image_x2_x3_image_x2_x4 inc image_x2_union_x3_x4 ----------------------------------------------- creation du sous-theoreme 2 2 definition de la conclusion 2 nouvelle conclusion -qqs(A, A app union_image_x2_x3_image_x2_x4=>A app image_x2_union_x3_x4). --------------------------------------------------------- regle defconcl1 2 ajouter objet x7 2 nouvelle conclusion x7 app union_image_x2_x3_image_x2_x4=>x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle qqs1 2 ajouter hypothese x7 app union_image_x2_x3_image_x2_x4 2 nouvelle conclusion x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle => 2 ajouter hypothese x7 app image_x2_x3 ou x7 app image_x2_x4 --------------------------------------------------------- regle union 2 traitement de l hypothese disjonctive x7 app image_x2_x3 ou x7 app image_x2_x4 2 nouvelle conclusion (x7 app image_x2_x3=>x7 app image_x2_union_x3_x4)et (x7 app image_x2_x4=>x7 app image_x2_union_x3_x4) 2 ajouter hypothese-traitee x7 app image_x2_x3 ou x7 app image_x2_x4 --------------------------------------------------------- regle ou ************************************************ sous-theoreme 21 ***** 21 nouvelle conclusion x7 app image_x2_x3=>x7 app image_x2_union_x3_x4 ----------------------------------------------- creation du sous-theoreme 21 21 ajouter hypothese x7 app image_x2_x3 21 nouvelle conclusion x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle => 21 ajouter hypothese -ilexiste(A app x3, ..[x2, A]:x7). --------------------------------------------------------- regle image 21 ajouter objet x8 21 ajouter hypothese x8 app x3 21 ajouter hypothese x2(x8):x7 21 ajouter hypothese-traitee -ilexiste(A app x3, ..[x2, A]:x7). --------------------------------------------------------- regle ilexiste 21 ajouter hypothese x8 app union_x3_x4 --------------------------------------------------------- regle union1 21 ajouter hypothese x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle image1 21 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 21 demontre 2 nouvelle conclusion x7 app image_x2_x4=>x7 app image_x2_union_x3_x4 ************************************************ sous-theoreme 22 ***** 22 nouvelle conclusion x7 app image_x2_x4=>x7 app image_x2_union_x3_x4 ----------------------------------------------- creation du sous-theoreme 22 22 ajouter hypothese x7 app image_x2_x4 22 nouvelle conclusion x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle => 22 ajouter hypothese -ilexiste(A app x4, ..[x2, A]:x7). --------------------------------------------------------- regle image 22 ajouter objet x9 22 ajouter hypothese x9 app x4 22 ajouter hypothese x2(x9):x7 22 ajouter hypothese-traitee -ilexiste(A app x4, ..[x2, A]:x7). --------------------------------------------------------- regle ilexiste 22 ajouter hypothese x9 app union_x3_x4 --------------------------------------------------------- regle union2 22 ajouter hypothese x7 app image_x2_union_x3_x4 --------------------------------------------------------- regle image1 22 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 22 demontre 2 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 2 demontre 0 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 0 demontre en 0.59 seconds ================================================================================