>PhoX> Cst a : prop. a : prop >PhoX> Cst b : prop. b : prop >PhoX> Cst c : prop. c : prop >PhoX> Cst d : prop. d : prop >PhoX> theorem numero1 (a b) ( a b). Here is the goal: goal 1/1 a b a b %PhoX% intro 2. 2 goals created. goal 2/2 H := a b b a goal 1/2 H := a b a b %PhoX% intro 2. 1 goal created. goal 1/2 H := a b H0 := a H1 := b False %PhoX% left H. 1 goal created. goal 1/2 H0 := a H1 := b H := a b H2 := b a False %PhoX% elim H0. 1 goal created. goal 1/2 H0 := a H1 := b H := a b H2 := b a a %PhoX% elim H2. 1 goal created. goal 1/2 H0 := a H1 := b H := a b H2 := b a b %PhoX% axiom H1. 0 goal created. goal 1/1 H := a b b a %PhoX% intro 2. 1 goal created. goal 1/1 H := a b H0 := b H1 := a False %PhoX% left H. 1 goal created. goal 1/1 H0 := b H1 := a H := a b H2 := b a False %PhoX% elim H0. 1 goal created. goal 1/1 H0 := b H1 := a H := a b H2 := b a b %PhoX% elim H. 1 goal created. goal 1/1 H0 := b H1 := a H := a b H2 := b a a %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero1 = a b a b : theorem >PhoX> theorem numero2 (a b) (c d) (a c b d). Here is the goal: goal 1/1 a b c d a c b d %PhoX% intro 3. 2 goals created. goal 2/2 H := a b H0 := c d b d a c goal 1/2 H := a b H0 := c d a c b d %PhoX% intro 2. 2 goals created. goal 2/3 H := a b H0 := c d H1 := a c d goal 1/3 H := a b H0 := c d H1 := a c b %PhoX% left H. 1 goal created. goal 1/3 H0 := c d H1 := a c H := a b H2 := b a b %PhoX% left H1. 1 goal created. goal 1/3 H0 := c d H := a b H2 := b a H1 := a H3 := c b %PhoX% elim H. 1 goal created. goal 1/3 H0 := c d H := a b H2 := b a H1 := a H3 := c a %PhoX% axiom H1. 0 goal created. goal 2/2 H := a b H0 := c d b d a c goal 1/2 H := a b H0 := c d H1 := a c d %PhoX% left H0. 1 goal created. goal 1/2 H := a b H1 := a c H0 := c d H2 := d c d %PhoX% left H1. 1 goal created. goal 1/2 H := a b H0 := c d H2 := d c H1 := a H3 := c d %PhoX% elim H0. 1 goal created. goal 1/2 H := a b H0 := c d H2 := d c H1 := a H3 := c c %PhoX% axiom H3. 0 goal created. goal 1/1 H := a b H0 := c d b d a c %PhoX% intro 2. 2 goals created. goal 2/2 H := a b H0 := c d H1 := b d c goal 1/2 H := a b H0 := c d H1 := b d a %PhoX% left H. 1 goal created. goal 1/2 H0 := c d H1 := b d H := a b H2 := b a a %PhoX% left H1. 1 goal created. goal 1/2 H0 := c d H := a b H2 := b a H1 := b H3 := d a %PhoX% elim H2. 1 goal created. goal 1/2 H0 := c d H := a b H2 := b a H1 := b H3 := d b %PhoX% axiom H1. 0 goal created. goal 1/1 H := a b H0 := c d H1 := b d c %PhoX% left H0. 1 goal created. goal 1/1 H := a b H1 := b d H0 := c d H2 := d c c %PhoX% left H1. 1 goal created. goal 1/1 H := a b H0 := c d H2 := d c H1 := b H3 := d c %PhoX% elim H2. 1 goal created. goal 1/1 H := a b H0 := c d H2 := d c H1 := b H3 := d d %PhoX% axiom H3. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero2 = a b c d a c b d : theorem >PhoX> theorem numero3 (a b) (c d) (a c b d). Here is the goal: goal 1/1 a b c d a c b d %PhoX% intro 2. 1 goal created. goal 1/1 H := a b H0 := c d a c b d %PhoX% left H. 1 goal created. goal 1/1 H0 := c d H := a b H1 := b a a c b d %PhoX% left H0. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c a c b d %PhoX% intro. 2 goals created. goal 2/2 H := a b H1 := b a H0 := c d H2 := d c b d a c goal 1/2 H := a b H1 := b a H0 := c d H2 := d c a c b d %PhoX% intro. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a c b d %PhoX% left H3. 2 goals created. goal 2/3 H := a b H1 := b a H0 := c d H2 := d c H3 := a b d goal 1/3 H := a b H1 := b a H0 := c d H2 := d c H3 := c b d %PhoX% intro r. 1 goal created. goal 1/3 H := a b H1 := b a H0 := c d H2 := d c H3 := c d %PhoX% trivial. 0 goal created. goal 2/2 H := a b H1 := b a H0 := c d H2 := d c b d a c goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a b d %PhoX% intro l. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a b %PhoX% trivial. 0 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c b d a c %PhoX% intro. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b d a c %PhoX% left H3. 2 goals created. goal 2/2 H := a b H1 := b a H0 := c d H2 := d c H3 := b a c goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := d a c %PhoX% intro r. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := d c %PhoX% trivial. 0 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b a c %PhoX% intro l. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b a %PhoX% trivial. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero3 = a b c d a c b d : theorem >PhoX> theorem numero4 (a b) (c d) ((a c) (b d)). Here is the goal: goal 1/1 a b c d (a c) (b d) %PhoX% intro 2. 1 goal created. goal 1/1 H := a b H0 := c d (a c) (b d) %PhoX% left H. 1 goal created. goal 1/1 H0 := c d H := a b H1 := b a (a c) (b d) %PhoX% left H0. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c (a c) (b d) %PhoX% intro. 2 goals created. goal 2/2 H := a b H1 := b a H0 := c d H2 := d c (b d) a c goal 1/2 H := a b H1 := b a H0 := c d H2 := d c (a c) b d %PhoX% intro 2. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a c H4 := b d %PhoX% elim H0. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a c H4 := b c %PhoX% elim H3. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a c H4 := b a %PhoX% elim H1. 1 goal created. goal 1/2 H := a b H1 := b a H0 := c d H2 := d c H3 := a c H4 := b b %PhoX% axiom H4. 0 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c (b d) a c %PhoX% intro 2. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b d H4 := a c %PhoX% elim H2. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b d H4 := a d %PhoX% elim H3. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b d H4 := a b %PhoX% elim H. 1 goal created. goal 1/1 H := a b H1 := b a H0 := c d H2 := d c H3 := b d H4 := a a %PhoX% axiom H4. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero4 = a b c d (a c) (b d) : theorem >PhoX> Sort term. Sort term defined >PhoX> Cst A : term prop. A : term prop >PhoX> Cst B : term prop. B : term prop >PhoX> theorem numero5 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 4. 2 goals created. goal 2/2 H := x0 (A x0 B x0) H0 := x0 B x0 A x goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 B x %PhoX% elim H. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 A x %PhoX% elim H0. 0 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 A x %PhoX% elim H. 1 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 B x %PhoX% elim H0. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero5 = x (A x B x) x A x x B x : theorem >PhoX> theorem numero6 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. 2 goals created. goal 2/2 H := x (A x B x) x B x x A x goal 1/2 H := 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) H0 := x A x x B x %PhoX% elim H0. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 H1 := A x x0 B x0 %PhoX% elim H. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 H1 := A x H2 := A ?1 B ?1 H3 := B ?1 A ?1 x0 B x0 %PhoX% intro. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 H1 := A x H2 := A ?1 B ?1 H3 := B ?1 A ?1 B ?2 %PhoX% elim H2. 1 goal created. goal 1/2 H := x0 (A x0 B x0) H0 := x0 A x0 H1 := A x H2 := A ?2 B ?2 H3 := B ?2 A ?2 A ?2 %PhoX% axiom H1. 0 goal created. goal 1/1 H := x (A x B x) x B x x A x %PhoX% intro. 1 goal created. goal 1/1 H := x (A x B x) H0 := x B x x A x %PhoX% elim H0. 1 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 H1 := B x x0 A x0 %PhoX% elim H. 1 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 H1 := B x H2 := A ?3 B ?3 H3 := B ?3 A ?3 x0 A x0 %PhoX% intro. 1 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 H1 := B x H2 := A ?3 B ?3 H3 := B ?3 A ?3 A ?4 %PhoX% elim H3. 1 goal created. goal 1/1 H := x0 (A x0 B x0) H0 := x0 B x0 H1 := B x H2 := A ?4 B ?4 H3 := B ?4 A ?4 B ?4 %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero6 = x (A x B x) x A x x B x : theorem bye