>PhoX> Sort term. Sort term defined >PhoX> Cst R : term prop. R : term prop >PhoX> theorem numero2 xy(R y R x). Here is the goal: goal 1/1 x y:R R x %PhoX% use x R x x R x. 2 goals created. goal 2/2 x R x x R x goal 1/2 G := x R x x R x x y:R R x %PhoX% left G. 2 goals created. goal 2/3 H := x R x x y:R R x goal 1/3 H := x R x x y:R R x %PhoX% rewrite_hyp H exists.demorgan. 1 goal created. goal 1/3 H := x R x x y:R R x %PhoX% intro 3. 1 goal created. goal 1/3 H := x R x H0 := R y R ?1 %PhoX% elim False. 1 goal created. goal 1/3 H := x R x H0 := R y False %PhoX% apply -1 (y) H. 1 goal created. goal 1/3 H := x R x H0 := R y G := R y False %PhoX% elim G. 1 goal created. goal 1/3 H := x R x H0 := R y G := R y R y %PhoX% axiom H0. 0 goal created. goal 2/2 x R x x R x goal 1/2 H := x R x x y:R R x %PhoX% elim H. 1 goal created. goal 1/2 H := x0 R x0 H0 := R x x0 y:R R x0 %PhoX% intro. 1 goal created. goal 1/2 H := x0 R x0 H0 := R x y:R R ?2 %PhoX% instance ?2 x. Here are the goals: goal 2/2 x R x x R x goal 1/2 H := x0 R x0 H0 := R x y:R R x %PhoX% intro 2. 1 goal created. goal 1/2 H := x0 R x0 H0 := R x H1 := R y R x %PhoX% axiom H0. 0 goal created. goal 1/1 x R x x R x %PhoX% elim excluded_middle. 0 goal created. %PhoX% save numero2. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero2 = x y:R R x : theorem >PhoX> theorem numero3 xy(((R y R x) R x) R y). Here is the goal: goal 1/1 x y (((R y R x) R x) R y) %PhoX% use x R x x R x. 2 goals created. goal 2/2 x R x x R x goal 1/2 G := x R x x R x x y (((R y R x) R x) R y) %PhoX% elim G. 2 goals created. goal 2/3 G := x R x x R x H := x R x x y (((R y R x) R x) R y) goal 1/3 G := x R x x R x H := x R x x y (((R y R x) R x) R y) %PhoX% intro 3. 1 goal created. goal 1/3 G := x R x x R x H := x R x H0 := (R y R ?1) R ?1 R y %PhoX% elim H. 0 goal created. goal 2/2 x R x x R x goal 1/2 G := x R x x R x H := x R x x y (((R y R x) R x) R y) %PhoX% rewrite_hyp H forall.demorgan. 1 goal created. goal 1/2 G := x R x x R x H := x R x x y (((R y R x) R x) R y) %PhoX% elim H. 1 goal created. goal 1/2 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x x0 y (((R y R x0) R x0) R y) %PhoX% intro 3. 1 goal created. goal 1/2 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R ?2) R ?2 R y %PhoX% instance ?2 x. Here are the goals: goal 2/2 x R x x R x goal 1/2 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x R y %PhoX% use R y R y. 2 goals created. goal 2/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x R y R y goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y R y %PhoX% elim G0. 2 goals created. goal 2/4 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y R y goal 1/4 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y R y %PhoX% axiom H2. 0 goal created. goal 3/3 x R x x R x goal 2/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x R y R y goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y R y %PhoX% elim H0. 1 goal created. goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y R x %PhoX% elim H1. 1 goal created. goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y R y R x %PhoX% intro. 1 goal created. goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y H3 := R y R x %PhoX% elim H2. 1 goal created. goal 1/3 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x G0 := R y R y H2 := R y H3 := R y R y %PhoX% axiom H3. 0 goal created. goal 2/2 x R x x R x goal 1/2 G := x0 R x0 x0 R x0 H := x0 R x0 H0 := R x H1 := (R y R x) R x R y R y %PhoX% elim excluded_middle. 0 goal created. goal 1/1 x R x x R x %PhoX% elim excluded_middle. 0 goal created. %PhoX% save numero3. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero3 = x y (((R y R x) R x) R y) : theorem >PhoX> Cst f : term term. f : term term >PhoX> theorem numero5 xy (((R(f x) R(f y)) R x) R y). Here is the goal: goal 1/1 x y (((R (f x) R (f y)) R x) R y) %PhoX% by_absurd. 1 goal created. goal 1/1 H := x y (((R (f x) R (f y)) R x) R y) x y (((R (f x) R (f y)) R x) R y) %PhoX% intro 3. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H0 := (R (f ?1) R (f y)) R ?1 R y %PhoX% rmh H0. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) R y %PhoX% by_absurd. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H0 := R y R y %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H0 := R y x y0 (((R (f x) R (f y0)) R x) R y0) %PhoX% intro 3. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f ?2) R (f y0)) R ?2 R y0 %PhoX% by_absurd. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f ?2) R (f y0)) R ?2 H2 := R y0 R y0 %PhoX% elim H0. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f ?2) R (f y0)) R ?2 H2 := R y0 R y %PhoX% elim H1. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 R (f y) R (f y0) %PhoX% intro. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) R (f y0) %PhoX% by_absurd. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) R (f y0) %PhoX% elim H. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) x y1 (((R (f x) R (f y1)) R x) R y1) %PhoX% intro 3. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) H5 := (R (f ?3) R (f y1)) R ?3 R y1 %PhoX% elim H2. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) H5 := (R (f ?3) R (f y1)) R ?3 R y0 %PhoX% elim H5. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) H5 := (R (f y0) R (f y1)) R y0 R (f y0) R (f y1) %PhoX% intro. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) H5 := (R (f y0) R (f y1)) R y0 H6 := R (f y0) R (f y1) %PhoX% elim H4. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H0 := R y H1 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) H5 := (R (f y0) R (f y1)) R y0 H6 := R (f y0) R (f y0) %PhoX% axiom H6. 0 goal created. %PhoX% save numero5. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero5 = x y (((R (f x) R (f y)) R x) R y) : theorem bye