>PhoX> Cst a : prop. a : prop >PhoX> Cst b : prop. b : prop >PhoX> Cst c : prop. c : prop >PhoX> theorem numero4 ((a b c) c) (((a c c) ((b >PhoX> c c) c)) c). Here is the goal: goal 1/1 ((a b c) c) ((a c c) (b c c) c) c %PhoX% intros. 1 goal created. goal 1/1 H := (a b c) c H0 := (a c c) (b c c) c c %PhoX% elim H. 1 goal created. goal 1/1 H := (a b c) c H0 := (a c c) (b c c) c a b c %PhoX% intros. 1 goal created. goal 1/1 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b c %PhoX% elim H0. 2 goals created. goal 2/2 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b b c c goal 1/2 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b a c c %PhoX% intros. 1 goal created. goal 1/2 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b H4 := c c %PhoX% trivial. 0 goal created. goal 1/1 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b b c c %PhoX% intros. 1 goal created. goal 1/1 H := (a b c) c H0 := (a c c) (b c c) c H1 := a H2 := b H4 := c c %PhoX% trivial. 0 goal created. %PhoX% save numero4. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero4 = ((a b c) c) ((a c c) (b c c) c) c : theorem >PhoX> Cst a : prop. This symbol already exists (ignored). a : prop >PhoX> Cst b : prop. This symbol already exists (ignored). b : prop >PhoX> Cst c : prop. This symbol already exists (ignored). c : prop >PhoX> theorem numero5 (a b c) (a b) (a c). Here is the goal: goal 1/1 (a b c) (a b) (a c) %PhoX% intro. 2 goals created. goal 2/2 (a b) (a c) a b c goal 1/2 (a b c) (a b) (a c) %PhoX% intro 2. 2 goals created. goal 2/3 H := a b c a c goal 1/3 H := a b c a b %PhoX% intro. 1 goal created. goal 1/3 H := a b c H0 := a b %PhoX% elim H. 1 goal created. goal 1/3 H := a b c H0 := a a %PhoX% axiom H0. 0 goal created. goal 2/2 (a b) (a c) a b c goal 1/2 H := a b c a c %PhoX% intro. 1 goal created. goal 1/2 H := a b c H0 := a c %PhoX% elim H. 1 goal created. goal 1/2 H := a b c H0 := a a %PhoX% axiom H0. 0 goal created. goal 1/1 (a b) (a c) a b c %PhoX% intro 3. 2 goals created. goal 2/2 H := (a b) (a c) H0 := a c goal 1/2 H := (a b) (a c) H0 := a b %PhoX% left H. 1 goal created. goal 1/2 H0 := a H := a b H1 := a c b %PhoX% elim H. 1 goal created. goal 1/2 H0 := a H := a b H1 := a c a %PhoX% axiom H0. 0 goal created. goal 1/1 H := (a b) (a c) H0 := a c %PhoX% left H. 1 goal created. goal 1/1 H0 := a H := a b H1 := a c c %PhoX% elim H1. 1 goal created. goal 1/1 H0 := a H := a b H1 := a c a %PhoX% axiom H0. 0 goal created. %PhoX% save numero5. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero5 = (a b c) (a b) (a c) : theorem >PhoX> Cst a : prop. This symbol already exists (ignored). a : prop >PhoX> Cst b : prop. This symbol already exists (ignored). b : prop >PhoX> Cst c : prop. This symbol already exists (ignored). c : prop >PhoX> theorem numero8 (a b c) (a c) (b c). Here is the goal: goal 1/1 (a b c) (a c) (b c) %PhoX% intro. 2 goals created. goal 2/2 (a c) (b c) a b c goal 1/2 (a b c) (a c) (b c) %PhoX% intro. 1 goal created. goal 1/2 H := a b c (a c) (b c) %PhoX% by_absurd. 1 goal created. goal 1/2 H := a b c H0 := ((a c) (b c)) (a c) (b c) %PhoX% rewrite_hyp H0 disjunction.demorgan. 1 goal created. goal 1/2 H := a b c H0 := (a c) (b c) (a c) (b c) %PhoX% left H0. 1 goal created. goal 1/2 H := a b c H0 := (a c) H1 := (b c) (a c) (b c) %PhoX% rewrite_hyp H0 arrow.demorgan. 1 goal created. goal 1/2 H := a b c H1 := (b c) H0 := a c (a c) (b c) %PhoX% left H0. 1 goal created. goal 1/2 H := a b c H1 := (b c) H0 := a H2 := c (a c) (b c) %PhoX% rewrite_hyp H1 arrow.demorgan. 1 goal created. goal 1/2 H := a b c H0 := a H2 := c H1 := b c (a c) (b c) %PhoX% left H1. 1 goal created. goal 1/2 H := a b c H0 := a H2 := c H1 := b (a c) (b c) %PhoX% intro 2. 1 goal created. goal 1/2 H := a b c H0 := a H2 := c H1 := b c %PhoX% elim H. 1 goal created. goal 1/2 H := a b c H0 := a H2 := c H1 := b a b %PhoX% trivial. 0 goal created. goal 1/1 (a c) (b c) a b c %PhoX% intro 2. 1 goal created. goal 1/1 H := (a c) (b c) H0 := a b c %PhoX% left H0. 1 goal created. goal 1/1 H := (a c) (b c) H0 := a H1 := b c %PhoX% left H. 2 goals created. goal 2/2 H0 := a H1 := b H := a c c goal 1/2 H0 := a H1 := b H := b c c %PhoX% trivial. 0 goal created. goal 1/1 H0 := a H1 := b H := a c c %PhoX% trivial. 0 goal created. %PhoX% save numero8. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero8 = (a b c) (a c) (b c) : theorem >PhoX> Cst a : prop. This symbol already exists (ignored). a : prop >PhoX> Cst b : prop. This symbol already exists (ignored). b : prop >PhoX> Cst c : prop. This symbol already exists (ignored). c : prop >PhoX> theorem numero9 (a b) c (a c) (b c). Here is the goal: goal 1/1 a b c (a c) (b c) %PhoX% intro. 2 goals created. goal 2/2 (a c) (b c) a b c goal 1/2 a b c (a c) (b c) %PhoX% intro 2. 2 goals created. goal 2/3 H := a b c b c goal 1/3 H := a b c a c %PhoX% left H. 2 goals created. goal 2/4 H := a b a c goal 1/4 H := c a c %PhoX% trivial. 0 goal created. goal 3/3 (a c) (b c) a b c goal 2/3 H := a b c b c goal 1/3 H := a b a c %PhoX% left H. 1 goal created. goal 1/3 H := a H0 := b a c %PhoX% trivial. 0 goal created. goal 2/2 (a c) (b c) a b c goal 1/2 H := a b c b c %PhoX% left H. 2 goals created. goal 2/3 H := a b b c goal 1/3 H := c b c %PhoX% trivial. 0 goal created. goal 2/2 (a c) (b c) a b c goal 1/2 H := a b b c %PhoX% left H. 1 goal created. goal 1/2 H := a H0 := b b c %PhoX% trivial. 0 goal created. goal 1/1 (a c) (b c) a b c %PhoX% intro. 1 goal created. goal 1/1 H := (a c) (b c) a b c %PhoX% left H. 1 goal created. goal 1/1 H := a c H0 := b c a b c %PhoX% left H. 2 goals created. goal 2/2 H0 := b c H := a a b c goal 1/2 H0 := b c H := c a b c %PhoX% left H0. 2 goals created. goal 2/3 H := c H0 := b a b c goal 1/3 H := c a b c %PhoX% trivial. 0 goal created. goal 2/2 H0 := b c H := a a b c goal 1/2 H := c H0 := b a b c %PhoX% trivial. 0 goal created. goal 1/1 H0 := b c H := a a b c %PhoX% left H0. 2 goals created. goal 2/2 H := a H0 := b a b c goal 1/2 H := a H0 := c a b c %PhoX% trivial. 0 goal created. goal 1/1 H := a H0 := b a b c %PhoX% intro l. 1 goal created. goal 1/1 H := a H0 := b a b %PhoX% trivial. 0 goal created. %PhoX% save numero9. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero9 = a b c (a c) (b c) : theorem >PhoX> Cst a : prop. This symbol already exists (ignored). a : prop >PhoX> Cst b : prop. This symbol already exists (ignored). b : prop >PhoX> Cst c : prop. This symbol already exists (ignored). c : prop >PhoX> theorem numero10 (a b)c(ac)or(bc). Here is the goal: goal 1/1 (a b) c a c b c %PhoX% intros. 2 goals created. goal 2/2 a c b c (a b) c goal 1/2 (a b) c a c b c %PhoX% intro. 1 goal created. goal 1/2 H := (a b) c a c b c %PhoX% left H. 1 goal created. goal 1/2 H := a b H0 := c a c b c %PhoX% left H. 2 goals created. goal 2/3 H0 := c H := a a c b c goal 1/3 H0 := c H := b a c b c %PhoX% intro r. 1 goal created. goal 1/3 H0 := c H := b b c %PhoX% intro. 2 goals created. goal 2/4 H0 := c H := b c goal 1/4 H0 := c H := b b %PhoX% axiom H. 0 goal created. goal 3/3 a c b c (a b) c goal 2/3 H0 := c H := a a c b c goal 1/3 H0 := c H := b c %PhoX% axiom H0. 0 goal created. goal 2/2 a c b c (a b) c goal 1/2 H0 := c H := a a c b c %PhoX% intro l. 1 goal created. goal 1/2 H0 := c H := a a c %PhoX% intro. 2 goals created. goal 2/3 H0 := c H := a c goal 1/3 H0 := c H := a a %PhoX% axiom H. 0 goal created. goal 2/2 a c b c (a b) c goal 1/2 H0 := c H := a c %PhoX% axiom H0. 0 goal created. goal 1/1 a c b c (a b) c %PhoX% intro 2. 2 goals created. goal 2/2 H := a c b c c goal 1/2 H := a c b c a b %PhoX% left H. 2 goals created. goal 2/3 H := a c a b goal 1/3 H := b c a b %PhoX% intro r. 1 goal created. goal 1/3 H := b c b %PhoX% elim H. 0 goal created. goal 2/2 H := a c b c c goal 1/2 H := a c a b %PhoX% intro l. 1 goal created. goal 1/2 H := a c a %PhoX% elim H. 0 goal created. goal 1/1 H := a c b c c %PhoX% left H. 2 goals created. goal 2/2 H := a c c goal 1/2 H := b c c %PhoX% elim H. 0 goal created. goal 1/1 H := a c c %PhoX% elim H. 0 goal created. %PhoX% save numero10. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero10 = (a b) c a c b c : theorem >PhoX> theorem numero12 (a b)((a b)b). Here is the goal: goal 1/1 a b ((a b) b) %PhoX% intro. 2 goals created. goal 2/2 ((a b) b) a b goal 1/2 a b (a b) b %PhoX% intro 2. 1 goal created. goal 1/2 H := a b H0 := a b b %PhoX% elim H. 2 goals created. goal 2/3 H := a b H0 := a b H1 := b b goal 1/3 H := a b H0 := a b H1 := a b %PhoX% elim H0. 1 goal created. goal 1/3 H := a b H0 := a b H1 := a a %PhoX% axiom H1. 0 goal created. goal 2/2 ((a b) b) a b goal 1/2 H := a b H0 := a b H1 := b b %PhoX% axiom H1. 0 goal created. goal 1/1 ((a b) b) a b %PhoX% intro. 1 goal created. goal 1/1 H := (a b) b a b %PhoX% use a a. 2 goals created. goal 2/2 H := (a b) b a a goal 1/2 H := (a b) b G := a a a b %PhoX% elim G. 2 goals created. goal 2/3 H := (a b) b G := a a H0 := a a b goal 1/3 H := (a b) b G := a a H0 := a a b %PhoX% intro l. 1 goal created. goal 1/3 H := (a b) b G := a a H0 := a a %PhoX% axiom H0. 0 goal created. goal 2/2 H := (a b) b a a goal 1/2 H := (a b) b G := a a H0 := a a b %PhoX% intro r. 1 goal created. goal 1/2 H := (a b) b G := a a H0 := a b %PhoX% elim H. 1 goal created. goal 1/2 H := (a b) b G := a a H0 := a a b %PhoX% intro. 1 goal created. goal 1/2 H := (a b) b G := a a H0 := a H1 := a b %PhoX% elim H0. 1 goal created. goal 1/2 H := (a b) b G := a a H0 := a H1 := a a %PhoX% axiom H1. 0 goal created. goal 1/1 H := (a b) b a a %PhoX% elim excluded_middle. 0 goal created. %PhoX% save numero12. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero12 = a b ((a b) b) : theorem >PhoX> theorem numero14 (a b) (a b a b). Here is the goal: goal 1/1 (a b) (a b a b) %PhoX% intros. 2 goals created. goal 2/2 (a b a b) a b goal 1/2 a b a b a b %PhoX% intros. 1 goal created. goal 1/2 H := a b H0 := a b a b %PhoX% left H0. 2 goals created. goal 2/3 H := a b H0 := a a b goal 1/3 H := a b H0 := b a b %PhoX% intro. 2 goals created. goal 2/4 H := a b H0 := b b goal 1/4 H := a b H0 := b a %PhoX% elim H. 1 goal created. goal 1/4 H := a b H0 := b b %PhoX% axiom H0. 0 goal created. goal 3/3 (a b a b) a b goal 2/3 H := a b H0 := a a b goal 1/3 H := a b H0 := b b %PhoX% axiom H0. 0 goal created. goal 2/2 (a b a b) a b goal 1/2 H := a b H0 := a a b %PhoX% intro. 2 goals created. goal 2/3 H := a b H0 := a b goal 1/3 H := a b H0 := a a %PhoX% axiom H0. 0 goal created. goal 2/2 (a b a b) a b goal 1/2 H := a b H0 := a b %PhoX% elim H. 1 goal created. goal 1/2 H := a b H0 := a a %PhoX% axiom H0. 0 goal created. goal 1/1 (a b a b) a b %PhoX% intros. 1 goal created. goal 1/1 H := a b a b a b %PhoX% intros. 2 goals created. goal 2/2 H := a b a b b a goal 1/2 H := a b a b a b %PhoX% intros. 1 goal created. goal 1/2 H := a b a b H0 := a b %PhoX% elim H. 1 goal created. goal 1/2 H := a b a b H0 := a a b %PhoX% intro l. 1 goal created. goal 1/2 H := a b a b H0 := a a %PhoX% axiom H0. 0 goal created. goal 1/1 H := a b a b b a %PhoX% intros. 1 goal created. goal 1/1 H := a b a b H0 := b a %PhoX% elim H. 1 goal created. goal 1/1 H := a b a b H0 := b a b %PhoX% intro r. 1 goal created. goal 1/1 H := a b a b H0 := b b %PhoX% axiom H0. 0 goal created. %PhoX% save numero14. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero14 = (a b) (a b a b) : theorem bye