>PhoX> Sort term. Sort term defined >PhoX> Cst A : term prop. A : term prop >PhoX> Cst B : term prop. B : term prop >PhoX> theorem numero1 x ( A x B x) ( x A x x B x). Here is the goal: goal 1/1 x (A x B x) x A x x B x %PhoX% intro. 2 goals created. goal 2/2 x A x x B x x (A x B x) goal 1/2 x (A x B x) x A x x B x %PhoX% intro 2. 2 goals created. goal 2/3 H := x (A x B x) x B x goal 1/3 H := x (A x B x) x A x %PhoX% intro. 1 goal created. goal 1/3 H := x0 (A x0 B x0) A x %PhoX% elim H. 0 goal created. goal 2/2 x A x x B x x (A x B x) goal 1/2 H := x (A x B x) x B x %PhoX% intro. 1 goal created. goal 1/2 H := x0 (A x0 B x0) B x %PhoX% elim H. 0 goal created. goal 1/1 x A x x B x x (A x B x) %PhoX% intro 3. 2 goals created. goal 2/2 H := x0 A x0 x0 B x0 B x goal 1/2 H := x0 A x0 x0 B x0 A x %PhoX% elim H. 0 goal created. goal 1/1 H := x0 A x0 x0 B x0 B x %PhoX% elim H. 0 goal created. %PhoX% save numero1. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero1 = x (A x B x) x A x x B x : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst A : term prop. This symbol already exists (ignored). A : term prop >PhoX> Cst B : term prop. This symbol already exists (ignored). B : term prop >PhoX> theorem numero2 x ( A x B x) ( x A x x B x). Here is the goal: goal 1/1 x:A B x x A x x B x %PhoX% intro 2. 2 goals created. goal 2/2 H := x:A B x x B x goal 1/2 H := x:A B x x A x %PhoX% elim H. 1 goal created. goal 1/2 H := x0:A B x0 H0 := A x B x x0 A x0 %PhoX% left H0. 1 goal created. goal 1/2 H := x0:A B x0 H0 := A x H1 := B x x0 A x0 %PhoX% intro. 1 goal created. goal 1/2 H := x0:A B x0 H0 := A x H1 := B x A ?1 %PhoX% axiom H0. 0 goal created. goal 1/1 H := x:A B x x B x %PhoX% elim H. 1 goal created. goal 1/1 H := x0:A B x0 H0 := A x B x x0 B x0 %PhoX% left H0. 1 goal created. goal 1/1 H := x0:A B x0 H0 := A x H1 := B x x0 B x0 %PhoX% intro. 1 goal created. goal 1/1 H := x0:A B x0 H0 := A x H1 := B x B ?2 %PhoX% axiom H1. 0 goal created. %PhoX% save numero2. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero2 = x:A B x x A x x B x : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst A : term prop. This symbol already exists (ignored). A : term prop >PhoX> Cst B1 : prop. B1 : prop >PhoX> theorem numero3 x ( A x B1) ( x A x B1). Here is the goal: goal 1/1 x:A B1 x A x B1 %PhoX% intro. 2 goals created. goal 2/2 x A x B1 x:A B1 goal 1/2 x:A B1 x A x B1 %PhoX% intro 2. 2 goals created. goal 2/3 H := x:A B1 B1 goal 1/3 H := x:A B1 x A x %PhoX% elim H. 1 goal created. goal 1/3 H := x0:A B1 H0 := A x B1 x0 A x0 %PhoX% left H0. 1 goal created. goal 1/3 H := x0:A B1 H0 := A x H1 := B1 x0 A x0 %PhoX% intro. 1 goal created. goal 1/3 H := x0:A B1 H0 := A x H1 := B1 A ?1 %PhoX% axiom H0. 0 goal created. goal 2/2 x A x B1 x:A B1 goal 1/2 H := x:A B1 B1 %PhoX% elim H. 1 goal created. goal 1/2 H := x0:A B1 H0 := A x B1 B1 %PhoX% left H0. 1 goal created. goal 1/2 H := x0:A B1 H0 := A x H1 := B1 B1 %PhoX% axiom H1. 0 goal created. goal 1/1 x A x B1 x:A B1 %PhoX% intro. 1 goal created. goal 1/1 H := x A x B1 x:A B1 %PhoX% left H. 1 goal created. goal 1/1 H := x A x H0 := B1 x:A B1 %PhoX% elim H. 1 goal created. goal 1/1 H := x0 A x0 H0 := B1 H1 := A x x0:A B1 %PhoX% intro 2. 2 goals created. goal 2/2 H := x0 A x0 H0 := B1 H1 := A x B1 goal 1/2 H := x0 A x0 H0 := B1 H1 := A x A ?2 %PhoX% axiom H1. 0 goal created. goal 1/1 H := x0 A x0 H0 := B1 H1 := A x B1 %PhoX% axiom H0. 0 goal created. %PhoX% save numero3. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero3 = x:A B1 x A x B1 : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst A : term prop. This symbol already exists (ignored). A : term prop >PhoX> Cst B : term prop. This symbol already exists (ignored). B : term prop >PhoX> theorem numero4 x ( A x B x) ( x A x x B x). Here is the goal: goal 1/1 x (A x B x) x A x x B x %PhoX% intro. 2 goals created. goal 2/2 x A x x B x x (A x B x) goal 1/2 x (A x B x) x A x x B x %PhoX% intro. 1 goal created. goal 1/2 H := x (A x B x) x A x x B x %PhoX% elim H. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := A x B x x0 A x0 x0 B x0 %PhoX% left H0. 2 goals created. goal 2/3 H := x0 (A x0 B x0) H0 := A x x0 A x0 x0 B x0 goal 1/3 H := x0 (A x0 B x0) H0 := B x x0 A x0 x0 B x0 %PhoX% intro r. 1 goal created. goal 1/3 H := x0 (A x0 B x0) H0 := B x x0 B x0 %PhoX% intro. 1 goal created. goal 1/3 H := x0 (A x0 B x0) H0 := B x B ?1 %PhoX% axiom H0. 0 goal created. goal 2/2 x A x x B x x (A x B x) goal 1/2 H := x0 (A x0 B x0) H0 := A x x0 A x0 x0 B x0 %PhoX% intro l. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := A x x0 A x0 %PhoX% intro. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := A x A ?2 %PhoX% axiom H0. 0 goal created. goal 1/1 x A x x B x x (A x B x) %PhoX% intro. 1 goal created. goal 1/1 H := x A x x B x x (A x B x) %PhoX% left H. 2 goals created. goal 2/2 H := x A x x (A x B x) goal 1/2 H := x B x x (A x B x) %PhoX% elim H. 1 goal created. goal 1/2 H := x0 B x0 H0 := B x x0 (A x0 B x0) %PhoX% intro. 1 goal created. goal 1/2 H := x0 B x0 H0 := B x A ?3 B ?3 %PhoX% intro r. 1 goal created. goal 1/2 H := x0 B x0 H0 := B x B ?3 %PhoX% axiom H0. 0 goal created. goal 1/1 H := x A x x (A x B x) %PhoX% elim H. 1 goal created. goal 1/1 H := x0 A x0 H0 := A x x0 (A x0 B x0) %PhoX% intro. 1 goal created. goal 1/1 H := x0 A x0 H0 := A x A ?4 B ?4 %PhoX% intro l. 1 goal created. goal 1/1 H := x0 A x0 H0 := A x A ?4 %PhoX% axiom H0. 0 goal created. %PhoX% save numero4. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero4 = x (A x B x) x A x x B x : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst A : term prop. This symbol already exists (ignored). A : term prop >PhoX> Cst B : term prop. This symbol already exists (ignored). B : term prop >PhoX> Cst A1 : prop. A1 : prop >PhoX> Cst B1 : prop. This symbol already exists (ignored). B1 : prop >PhoX> theorem numero5 (x A x x B x)x (A x B x). Here is the goal: goal 1/1 x A x x B x x (A x B x) %PhoX% intro 2. 1 goal created. goal 1/1 H := x0 A x0 x0 B x0 A x B x %PhoX% left H. 2 goals created. goal 2/2 H := x0 A x0 A x B x goal 1/2 H := x0 B x0 A x B x %PhoX% intro r. 1 goal created. goal 1/2 H := x0 B x0 B x %PhoX% elim H. 0 goal created. goal 1/1 H := x0 A x0 A x B x %PhoX% intro l. 1 goal created. goal 1/1 H := x0 A x0 A x %PhoX% elim H. 0 goal created. %PhoX% save numero5. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero5 = x A x x B x x (A x B x) : theorem >PhoX> theorem numero7 x(A1 B x)(A1x B x). Here is the goal: goal 1/1 x (A1 B x) (A1 x B x) %PhoX% intros. 2 goals created. goal 2/2 (A1 x B x) x (A1 B x) goal 1/2 x (A1 B x) A1 x B x %PhoX% intro 3. 1 goal created. goal 1/2 H := x0 (A1 B x0) H0 := A1 B x %PhoX% elim H. 1 goal created. goal 1/2 H := x0 (A1 B x0) H0 := A1 A1 %PhoX% axiom H0. 0 goal created. goal 1/1 (A1 x B x) x (A1 B x) %PhoX% intro 3. 1 goal created. goal 1/1 H := A1 x0 B x0 H0 := A1 B x %PhoX% elim H. 1 goal created. goal 1/1 H := A1 x0 B x0 H0 := A1 A1 %PhoX% axiom H0. 0 goal created. %PhoX% save numero7. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero7 = x (A1 B x) (A1 x B x) : theorem >PhoX> theorem numero8 x(A x B1)(x A x B1). Here is the goal: goal 1/1 x:A B1 (x A x B1) %PhoX% intros. 2 goals created. goal 2/2 (x A x B1) x:A B1 goal 1/2 x:A B1 x A x B1 %PhoX% intros. 1 goal created. goal 1/2 H := x:A B1 H0 := x A x B1 %PhoX% left H0. 1 goal created. goal 1/2 H := x0:A B1 H0 := A x B1 %PhoX% elim H. 1 goal created. goal 1/2 H := x0:A B1 H0 := A x A ?1 %PhoX% axiom H0. 0 goal created. goal 1/1 (x A x B1) x:A B1 %PhoX% intros. 1 goal created. goal 1/1 H := x0 A x0 B1 H0 := A x B1 %PhoX% elim H. 1 goal created. goal 1/1 H := x0 A x0 B1 H0 := A x x0 A x0 %PhoX% intro. 1 goal created. goal 1/1 H := x0 A x0 B1 H0 := A x A ?2 %PhoX% axiom H0. 0 goal created. %PhoX% save numero8. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero8 = x:A B1 (x A x B1) : theorem bye