>PhoX> Sort term. Sort term defined >PhoX> Cst R : term prop. R : term prop >PhoX> theorem numero1 xy (R x R y). Here is the goal: goal 1/1 x y (R x R y) %PhoX% intro. 1 goal created. goal 1/1 H := x y (R x R y) False %PhoX% elim H. 1 goal created. goal 1/1 H := x y (R x R y) x y (R x R y) %PhoX% intro 4. 1 goal created. goal 1/1 H := x y0 (R x R y0) H0 := R ?1 H1 := R y False %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 (R x R y0) H0 := R ?1 H1 := R y x y0 (R x R y0) %PhoX% intro 4. 1 goal created. goal 1/1 H := x y1 (R x R y1) H0 := R ?1 H1 := R y H2 := R ?2 H3 := R y0 False %PhoX% elim H1. 1 goal created. goal 1/1 H := x y1 (R x R y1) H0 := R ?1 H1 := R y H2 := R ?2 H3 := R y0 R y %PhoX% axiom H2. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero1 = x y (R x R y) : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst R : term prop. This symbol already exists (ignored). R : term prop >PhoX> theorem numero3 x y ((( 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% intro. 1 goal created. goal 1/1 H := x y ((( R y R x) R x) R y) False %PhoX% elim H. 1 goal created. goal 1/1 H := x y ((( R y R x) R x) R y) x y ((( R y R x) R x) R y) %PhoX% intro 4. 1 goal created. goal 1/1 H := x y0 ((( R y0 R x) R x) R y0) H0 := ( R y R ?1) R ?1 H1 := R y False %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 ((( R y0 R x) R x) R y0) H0 := ( R y R ?1) R ?1 H1 := R y x y0 ((( R y0 R x) R x) R y0) %PhoX% intro 4. 1 goal created. goal 1/1 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R ?2) R ?2 H3 := R y0 False %PhoX% instance ?2 y. Here is the goal: goal 1/1 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 False %PhoX% elim H2. 2 goals created. goal 2/2 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 R y goal 1/2 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 R y0 R y %PhoX% intro 2. 1 goal created. goal 1/2 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 H4 := R y0 False %PhoX% elim H4. 1 goal created. goal 1/2 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 H4 := R y0 R y0 %PhoX% axiom H3. 0 goal created. goal 1/1 H := x y1 ((( R y1 R x) R x) R y1) H0 := ( R y R ?1) R ?1 H1 := R y H2 := ( R y0 R y) R y H3 := R y0 R y %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero3 = x y ((( R y R x) R x) R y) : theorem >PhoX> Sort term. This symbol already exists (ignored). Sort term defined >PhoX> Cst R : term prop. This symbol already exists (ignored). R : term prop >PhoX> Cst S : term prop. S : term prop >PhoX> (* exercice difficile*) >PhoX> theorem numero4 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% intro. 1 goal created. goal 1/1 H := x y (((R y R x) R x) R y) False %PhoX% elim H. 1 goal created. goal 1/1 H := x y (((R y R x) R x) R y) x y (((R y R x) R x) R y) %PhoX% intro 2. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) (((R y R ?1) R ?1) R y) %PhoX% intro. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) False %PhoX% elim H0. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) ((R y R ?1) R ?1) R y %PhoX% intro. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 R y %PhoX% (* la commande suivante correspond à la règle d'absurdité intuitionniste*) %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 x y0 (((R y0 R x) R x) R y0) %PhoX% intro. 1 goal created. goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 y0 (((R y0 R ?2) R ?2) R y0) %PhoX% instance ?2 y. Here is the goal: goal 1/1 H := x y0 (((R y0 R x) R x) R y0) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 y0 (((R y0 R y) R y) R y0) %PhoX% intro 2. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) False %PhoX% elim H2. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) ((R y0 R y) R y) R y0 %PhoX% intro. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y R y0 %PhoX% elim H0. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y ((R y R ?1) R ?1) R y %PhoX% intro. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y R y %PhoX% elim H3. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y R y0 R y %PhoX% intro. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y H5 := R y0 R y %PhoX% elim H2. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y H5 := R y0 ((R y0 R y) R y) R y0 %PhoX% intro. 1 goal created. goal 1/1 H := x y1 (((R y1 R x) R x) R y1) H0 := (((R y R ?1) R ?1) R y) H1 := (R y R ?1) R ?1 H2 := (((R y0 R y) R y) R y0) H3 := (R y0 R y) R y H5 := R y0 R y0 %PhoX% axiom H5. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero4 = x y (((R y R x) R x) R y) : theorem >PhoX> (* comme le précédent mais un peu plus dur !*) >PhoX> theorem numero6 xy ((S y R x) (S x R y)). Here is the goal: goal 1/1 x y ((S y R x) S x R y) %PhoX% intro. 1 goal created. goal 1/1 H := x y ((S y R x) S x R y) False %PhoX% elim H. 1 goal created. goal 1/1 H := x y ((S y R x) S x R y) x y ((S y R x) S x R y) %PhoX% intro 2. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) ((S y R ?1) S ?1 R y) %PhoX% intro. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) False %PhoX% elim H0. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) (S y R ?1) S ?1 R y %PhoX% intro 2. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 R y %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 x y0 ((S y0 R x) S x R y0) %PhoX% intro. 1 goal created. goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 y0 ((S y0 R ?2) S ?2 R y0) %PhoX% instance ?2 y. Here is the goal: goal 1/1 H := x y0 ((S y0 R x) S x R y0) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 y0 ((S y0 R y) S y R y0) %PhoX% intro 2. 1 goal created. goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) False %PhoX% elim H3. 1 goal created. goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) (S y0 R y) S y R y0 %PhoX% intro 2. 1 goal created. goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y R y0 %PhoX% elim H. 1 goal created. goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y x y1 ((S y1 R x) S x R y1) %PhoX% intro. 1 goal created. goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y y1 ((S y1 R ?3) S ?3 R y1) %PhoX% instance ?3 y0. Here is the goal: goal 1/1 H := x y1 ((S y1 R x) S x R y1) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y y1 ((S y1 R y0) S y0 R y1) %PhoX% intro 2. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) False %PhoX% elim H6. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) (S y1 R y0) S y0 R y1 %PhoX% intro 2. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 R y1 %PhoX% elim H3. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 (S y0 R y) S y R y0 %PhoX% intro 2. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 R y0 %PhoX% elim H0. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 (S y R ?1) S ?1 R y %PhoX% intro 2. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 R y %PhoX% elim H4. 1 goal created. goal 1/1 H := x y2 ((S y2 R x) S x R y2) H0 := ((S y R ?1) S ?1 R y) H1 := S y R ?1 H2 := S ?1 H3 := ((S y0 R y) S y R y0) H4 := S y0 R y H5 := S y H6 := ((S y1 R y0) S y0 R y1) H7 := S y1 R y0 H8 := S y0 S y0 %PhoX% axiom H8. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero6 = x y ((S y R x) S x R y) : theorem >PhoX> Cst f : term term. f : term term >PhoX> theorem numero7 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% intros. 1 goal created. goal 1/1 H := x y (((R (f x) R (f y)) R x) R y) False %PhoX% elim H. 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% intros. 1 goal created. goal 1/1 H := x y (((R (f x) R (f y)) R x) R y) y (((R (f ?1) R (f y)) R ?1) R y) %PhoX% intros. 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% intros. 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 H1 := R y False %PhoX% rmh H0. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H1 := R y False %PhoX% elim H. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H1 := R y x y0 (((R (f x) R (f y0)) R x) R y0) %PhoX% intros. 1 goal created. goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H1 := R y y0 (((R (f ?2) R (f y0)) R ?2) R y0) %PhoX% instance ?2 y. Here is the goal: goal 1/1 H := x y0 (((R (f x) R (f y0)) R x) R y0) H1 := R y y0 (((R (f y) R (f y0)) R y) R y0) %PhoX% intros. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y R y0 %PhoX% intros. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 False %PhoX% elim H1. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 R y %PhoX% elim H0. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 R (f y) R (f y0) %PhoX% intros. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) R (f y0) %PhoX% intros. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) False %PhoX% elim H. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (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% intros. 1 goal created. goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) y1 (((R (f ?3) R (f y1)) R ?3) R y1) %PhoX% instance ?3 y0. Here is the goal: goal 1/1 H := x y1 (((R (f x) R (f y1)) R x) R y1) H1 := R y H0 := (R (f y) R (f y0)) R y H2 := R y0 H3 := R (f y) H4 := R (f y0) y1 (((R (f y0) R (f y1)) R y0) R y1) %PhoX% intros. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H1 := R y H0 := (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 y1 %PhoX% intros. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H1 := R y H0 := (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 y1 False %PhoX% elim H2. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H1 := R y H0 := (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 y1 R y0 %PhoX% elim H5. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H1 := R y H0 := (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 y1 R (f y0) R (f y1) %PhoX% intros. 1 goal created. goal 1/1 H := x y2 (((R (f x) R (f y2)) R x) R y2) H1 := R y H0 := (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 y1 H7 := 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) H1 := R y H0 := (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 y1 H7 := R (f y0) R (f y0) %PhoX% axiom H7. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero7 = x y (((R (f x) R (f y)) R x) R y) : theorem bye