th2 parties(a inter b) = parties(a) inter parties(b) -qqs(A, qqs(B, parties(A inter B)egal_ens parties(A)inter parties(B))). ******************************************************************************** theoreme a demontrer -qqs(A, qqs(B, parties(A inter B)egal_ens parties(A)inter parties(B))). 0 nouvelle conclusion -qqs(A, qqs(B, parties(A inter B)egal_ens parties(A)inter parties(B))). 0 ajouter lien egal_ens 0 ajouter lien parties 0 ajouter lien inter 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 egal_ens egal_ens1 parties parties1 inter inter1 inter2 inc et defconcl1 defconcl1a defconcl1b defconcl1bb ilexiste ou defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 nouvelle conclusion -qqs(A, qqs(B, seul(A inter B:C, seul(parties(C):D, seul(parties(A):E, seul(parties(B):F, seul(E inter F:G, D egal_ens G))))))). --------------------------------------------------------- regle elifon 0 ajouter objet x 0 nouvelle conclusion -qqs(A, seul(x inter A:B, seul(parties(B):C, seul(parties(x):D, seul(parties(A):E, seul(D inter E:F, C egal_ens F)))))). --------------------------------------------------------- regle qqs1 0 ajouter objet x1 0 nouvelle conclusion -seul(x inter x1:A, seul(parties(A):B, seul(parties(x):C, seul(parties(x1):D, seul(C inter D:E, B egal_ens E))))). --------------------------------------------------------- regle qqs1 0 ajouter objet inter_x_x1 0 ajouter hypothese x inter x1:inter_x_x1 0 nouvelle conclusion -seul(parties(inter_x_x1):A, seul(parties(x):B, seul(parties(x1):C, seul(B inter C:D, A egal_ens D)))). --------------------------------------------------------- regle seul 0 ajouter objet parties_inter_x_x1 0 ajouter hypothese parties(inter_x_x1):parties_inter_x_x1 0 nouvelle conclusion -seul(parties(x):A, seul(parties(x1):B, seul(A inter B:C, parties_inter_x_x1 egal_ens C))). --------------------------------------------------------- regle seul 0 ajouter objet parties_x 0 ajouter hypothese parties(x):parties_x 0 nouvelle conclusion -seul(parties(x1):A, seul(parties_x inter A:B, parties_inter_x_x1 egal_ens B)). --------------------------------------------------------- regle seul 0 ajouter objet parties_x1 0 ajouter hypothese parties(x1):parties_x1 0 nouvelle conclusion -seul(parties_x inter parties_x1:A, parties_inter_x_x1 egal_ens A). --------------------------------------------------------- regle seul 0 ajouter objet inter_parties_x_parties_x1 0 ajouter hypothese parties_x inter parties_x1:inter_parties_x_parties_x1 0 nouvelle conclusion parties_inter_x_x1 egal_ens inter_parties_x_parties_x1 --------------------------------------------------------- regle seul 0 definition de la conclusion 0 nouvelle conclusion parties_inter_x_x1 inc inter_parties_x_parties_x1 et inter_parties_x_parties_x1 inc parties_inter_x_x1 --------------------------------------------------------- regle defconcl1 ************************************************ sous-theoreme 1 ***** 1 nouvelle conclusion parties_inter_x_x1 inc inter_parties_x_parties_x1 ----------------------------------------------- creation du sous-theoreme 1 1 definition de la conclusion 1 nouvelle conclusion -qqs(A, A app parties_inter_x_x1=>A app inter_parties_x_parties_x1). --------------------------------------------------------- regle defconcl1 1 ajouter objet x2 1 nouvelle conclusion x2 app parties_inter_x_x1=>x2 app inter_parties_x_parties_x1 --------------------------------------------------------- regle qqs1 1 ajouter hypothese x2 app parties_inter_x_x1 1 nouvelle conclusion x2 app inter_parties_x_parties_x1 --------------------------------------------------------- regle => 1 ajouter hypothese x2 inc inter_x_x1 --------------------------------------------------------- regle parties definition de la conclusion 1 nouvelle conclusion x2 app parties_x et x2 app parties_x1 --------------------------------------------------------- regle defconcl2app ************************************************ sous-theoreme 11 ***** 11 nouvelle conclusion x2 app parties_x ----------------------------------------------- creation du sous-theoreme 11 definition de la conclusion 11 nouvelle conclusion x2 inc x --------------------------------------------------------- regle defconcl2app 11 definition de la conclusion 11 nouvelle conclusion -qqs(A, A app x2=>A app x). --------------------------------------------------------- regle defconcl1 11 ajouter objet x3 11 nouvelle conclusion x3 app x2=>x3 app x --------------------------------------------------------- regle qqs1 11 ajouter hypothese x3 app x2 11 nouvelle conclusion x3 app x --------------------------------------------------------- regle => 11 ajouter hypothese x3 app inter_x_x1 --------------------------------------------------------- regle inc 11 ajouter hypothese x3 app x --------------------------------------------------------- regle inter 11 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 11 demontre 1 nouvelle conclusion x2 app parties_x1 ************************************************ sous-theoreme 12 ***** 12 nouvelle conclusion x2 app parties_x1 ----------------------------------------------- creation du sous-theoreme 12 definition de la conclusion 12 nouvelle conclusion x2 inc x1 --------------------------------------------------------- regle defconcl2app 12 definition de la conclusion 12 nouvelle conclusion -qqs(A, A app x2=>A app x1). --------------------------------------------------------- regle defconcl1 12 ajouter objet x4 12 nouvelle conclusion x4 app x2=>x4 app x1 --------------------------------------------------------- regle qqs1 12 ajouter hypothese x4 app x2 12 nouvelle conclusion x4 app x1 --------------------------------------------------------- regle => 12 ajouter hypothese x4 app inter_x_x1 --------------------------------------------------------- regle inc 12 ajouter hypothese x4 app x --------------------------------------------------------- regle inter 12 ajouter hypothese x4 app x1 --------------------------------------------------------- regle inter1 12 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 12 demontre 1 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 1 demontre 0 nouvelle conclusion inter_parties_x_parties_x1 inc parties_inter_x_x1 ************************************************ sous-theoreme 2 ***** 2 nouvelle conclusion inter_parties_x_parties_x1 inc parties_inter_x_x1 ----------------------------------------------- creation du sous-theoreme 2 2 definition de la conclusion 2 nouvelle conclusion -qqs(A, A app inter_parties_x_parties_x1=>A app parties_inter_x_x1). --------------------------------------------------------- regle defconcl1 2 ajouter objet x5 2 nouvelle conclusion x5 app inter_parties_x_parties_x1=>x5 app parties_inter_x_x1 --------------------------------------------------------- regle qqs1 2 ajouter hypothese x5 app inter_parties_x_parties_x1 2 nouvelle conclusion x5 app parties_inter_x_x1 --------------------------------------------------------- regle => 2 ajouter hypothese x5 app parties_x --------------------------------------------------------- regle inter 2 ajouter hypothese x5 inc x --------------------------------------------------------- regle parties 2 ajouter hypothese x5 app parties_x1 --------------------------------------------------------- regle inter1 2 ajouter hypothese x5 inc x1 --------------------------------------------------------- regle parties definition de la conclusion 2 nouvelle conclusion x5 inc inter_x_x1 --------------------------------------------------------- regle defconcl2app 2 definition de la conclusion 2 nouvelle conclusion -qqs(A, A app x5=>A app inter_x_x1). --------------------------------------------------------- regle defconcl1 2 ajouter objet x6 2 nouvelle conclusion x6 app x5=>x6 app inter_x_x1 --------------------------------------------------------- regle qqs1 2 ajouter hypothese x6 app x5 2 nouvelle conclusion x6 app inter_x_x1 --------------------------------------------------------- regle => 2 ajouter hypothese x6 app x --------------------------------------------------------- regle inc 2 ajouter hypothese x6 app x1 --------------------------------------------------------- regle inc 2 ajouter hypothese x6 app inter_x_x1 --------------------------------------------------------- regle inter2 2 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 2 demontre 0 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 0 demontre en 0.49 seconds ================================================================================