th1
transitivite de l inclusion dans  l'ensemble des parties

-qqs(A, transitive(inc, parties(A))).


********************************************************************************
theoreme a demontrer 

-qqs(A, transitive(inc, parties(A))).
 
0 nouvelle conclusion 
-qqs(A, transitive(inc, parties(A))).
 
0 ajouter lien inc 
0 ajouter lien transitive 
0 ajouter lien parties 

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 inc transitive transitive1 parties parties1 et defconcl1 defconcl1a defconcl1b defconcl1bb ilexiste ou defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 

0 nouvelle conclusion 
-qqs(A, seul(parties(A):B, transitive(inc, B))).
 
--------------------------------------------------------- regle elifon 
0 ajouter objet x 
0 nouvelle conclusion 
-seul(parties(x):A, transitive(inc, A)).
 
--------------------------------------------------------- regle qqs1 
0 ajouter objet parties_x 
0 ajouter hypothese parties(x):parties_x 
0 nouvelle conclusion transitive(inc, parties_x) 
--------------------------------------------------------- regle seul 
0 ajouter objet inc 
0 definition de la conclusion 
0 nouvelle conclusion 
-qqs(A app parties_x, qqs(B app parties_x, qqs(C app parties_x, ..[inc, A, B]et..[inc, B, C]=> ..[inc, A, C]))).
 
--------------------------------------------------------- regle defconcl1 
0 ajouter objet x1 
0 ajouter hypothese x1 app parties_x 
0 nouvelle conclusion 
-qqs(A app parties_x, qqs(B app parties_x, ..[inc, x1, A]et..[inc, A, B]=> ..[inc, x1, B])).
 
--------------------------------------------------------- regle qqs2 
0 ajouter objet x2 
0 ajouter hypothese x2 app parties_x 
0 nouvelle conclusion 
-qqs(A app parties_x, ..[inc, x1, x2]et..[inc, x2, A]=> ..[inc, x1, A]).
 
--------------------------------------------------------- regle qqs2 
0 ajouter objet x3 
0 ajouter hypothese x3 app parties_x 
0 nouvelle conclusion ..[inc, x1, x2]et..[inc, x2, x3]=> ..[inc, x1, x3] 
--------------------------------------------------------- regle qqs2 
0 ajouter hypothese x1 inc x2 
0 ajouter hypothese x2 inc x3 
0 nouvelle conclusion ..[inc, x1, x3] 
--------------------------------------------------------- regle => 
0 nouvelle conclusion x1 inc x3 
--------------------------------------------------------- regle .. 
0 ajouter hypothese x1 inc x 
--------------------------------------------------------- regle parties 
0 ajouter hypothese x2 inc x 
--------------------------------------------------------- regle parties 
0 ajouter hypothese x3 inc x 
--------------------------------------------------------- regle parties 
0 definition de la conclusion 
0 nouvelle conclusion 
-qqs(A, A app x1=>A app x3).
 
--------------------------------------------------------- regle defconcl1 
0 ajouter objet x4 
0 nouvelle conclusion x4 app x1=>x4 app x3 
--------------------------------------------------------- regle qqs1 
0 ajouter hypothese x4 app x1 
0 nouvelle conclusion x4 app x3 
--------------------------------------------------------- regle => 
0 ajouter hypothese x4 app x2 
--------------------------------------------------------- regle inc 
0 ajouter hypothese x4 app x3 
--------------------------------------------------------- regle inc 
0 nouvelle conclusion vrai 
--------------------------------------------------------- regle stop1 
theoreme 0 demontre en 0.92 seconds
================================================================================