>PhoX> Cst a : prop. a : prop >PhoX> Cst b : prop. b : prop >PhoX> Cst c : prop. c : prop >PhoX> theorem numero2 ( b b ) ( (a b)a b). Here is the goal: goal 1/1 ( b b) (a b) a b %PhoX% intro 3. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a b %PhoX% elim H. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a b %PhoX% intro. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a H2 := b False %PhoX% elim H0. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a H2 := b (a b) %PhoX% intro. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a H2 := b H3 := a b False %PhoX% elim H2. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a H2 := b H3 := a b b %PhoX% elim H3. 1 goal created. goal 1/1 H := b b H0 := (a b) H1 := a H2 := b H3 := a b a %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero2 = ( b b) (a b) a b : theorem >PhoX> theorem numero3 ((a b) (( a c) ((b c) c))). Here is the goal: goal 1/1 ((a b) ( a c) (b c) c) %PhoX% intro. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) False %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) (a b) ( a c) (b c) c %PhoX% intro 3. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c c %PhoX% elim H1. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c a %PhoX% intro. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c H3 := a False %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c H3 := a (a b) ( a c) (b c) c %PhoX% intro 3. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c H3 := a c %PhoX% elim H2. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c H3 := a b %PhoX% elim H0. 1 goal created. goal 1/1 H := ((a b) ( a c) (b c) c) H0 := a b H1 := a c H2 := b c H3 := a a %PhoX% axiom H3. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero3 = ((a b) ( a c) (b c) c) : theorem >PhoX> theorem numero4 (( b a) (a b)). Here is the goal: goal 1/1 (( b a) a b) %PhoX% intro. 1 goal created. goal 1/1 H := (( b a) a b) False %PhoX% elim H. 1 goal created. goal 1/1 H := (( b a) a b) ( b a) a b %PhoX% intro 2. 1 goal created. goal 1/1 H := (( b a) a b) H0 := b a H1 := a b %PhoX% elim H0. 2 goals created. goal 2/2 H := (( b a) a b) H0 := b a H1 := a a goal 1/2 H := (( b a) a b) H0 := b a H1 := a b %PhoX% intro. 1 goal created. goal 1/2 H := (( b a) a b) H0 := b a H1 := a H2 := b False %PhoX% elim H. 1 goal created. goal 1/2 H := (( b a) a b) H0 := b a H1 := a H2 := b ( b a) a b %PhoX% intro 2. 1 goal created. goal 1/2 H := (( b a) a b) H0 := b a H1 := a H2 := b b %PhoX% axiom H2. 0 goal created. goal 1/1 H := (( b a) a b) H0 := b a H1 := a a %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero4 = (( b a) a b) : theorem >PhoX> theorem numero5 (((a b)a)a). Here is the goal: goal 1/1 (((a b) a) a) %PhoX% intro. 1 goal created. goal 1/1 H := (((a b) a) a) False %PhoX% elim H. 1 goal created. goal 1/1 H := (((a b) a) a) ((a b) a) a %PhoX% intro. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a a %PhoX% elim H0. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a a b %PhoX% intro. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a H1 := a b %PhoX% (* la commande suivante correspond à la règle d'absurdité intuitionniste*) %PhoX% elim False. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a H1 := a False %PhoX% elim H. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a H1 := a ((a b) a) a %PhoX% intro. 1 goal created. goal 1/1 H := (((a b) a) a) H0 := (a b) a H1 := a a %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero5 = (((a b) a) a) : theorem >PhoX> theorem numero6 ((ab c)(ac)or(bc)). Here is the goal: goal 1/1 ((a b c) (a c) (b c)) %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) False %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) (a b c) (a c) (b c) %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c (a c) (b c) %PhoX% intro l. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c a c %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a c %PhoX% (* la commande suivante correspond à la règle d'absurdité intuitionniste*) %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a (a b c) (a c) (b c) %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a (a c) (b c) %PhoX% intro r. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a b c %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a H3 := b c %PhoX% elim H0. 1 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a H3 := b a b %PhoX% intro. 2 goals created. goal 2/2 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a H3 := b b goal 1/2 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a H3 := b a %PhoX% axiom H1. 0 goal created. goal 1/1 H := ((a b c) (a c) (b c)) H0 := a b c H1 := a H3 := b b %PhoX% axiom H3. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero6 = ((a b c) (a c) (b c)) : theorem >PhoX> theorem numero7 ((a b c)(ab)or(ac)). Here is the goal: goal 1/1 ((a b c) (a b) (a c)) %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) False %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) (a b c) (a b) (a c) %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c (a b) (a c) %PhoX% intro l. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c a b %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a b %PhoX% elim H0. 3 goals created. goal 3/3 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c b goal 2/3 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := b b goal 1/3 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a a %PhoX% axiom H1. 0 goal created. goal 2/2 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c b goal 1/2 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := b b %PhoX% axiom H2. 0 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c b %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c (a b c) (a b) (a c) %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c (a b) (a c) %PhoX% intro r. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c a c %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a b) (a c)) H0 := a b c H1 := a H2 := c c %PhoX% axiom H2. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero7 = ((a b c) (a b) (a c)) : theorem >PhoX> theorem numero8 ((a b c)(a b) c). Here is the goal: goal 1/1 ((a b c) (a b) c) %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) c) False %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a b) c) (a b c) (a b) c %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c (a b) c %PhoX% intro l. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c a b %PhoX% intro. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c H1 := a b %PhoX% elim H0. 3 goals created. goal 3/3 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c b goal 2/3 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := b b goal 1/3 H := ((a b c) (a b) c) H0 := a b c H1 := a a %PhoX% axiom H1. 0 goal created. goal 2/2 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c b goal 1/2 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := b b %PhoX% axiom H2. 0 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c b %PhoX% elim H. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c (a b c) (a b) c %PhoX% intros. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c (a b) c %PhoX% intro r. 1 goal created. goal 1/1 H := ((a b c) (a b) c) H0 := a b c H1 := a H2 := c c %PhoX% axiom H2. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero8 = ((a b c) (a b) c) : theorem >PhoX> theorem numero10 (((a b) b) a b). Here is the goal: goal 1/1 (((a b) b) a b) %PhoX% intros. 1 goal created. goal 1/1 H := (((a b) b) a b) False %PhoX% elim H. 1 goal created. goal 1/1 H := (((a b) b) a b) ((a b) b) a b %PhoX% intros. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b a b %PhoX% intro r. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b b %PhoX% elim H0. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b a b %PhoX% intro. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b H1 := a b %PhoX% elim H. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b H1 := a ((a b) b) a b %PhoX% intros. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b H1 := a a b %PhoX% intro l. 1 goal created. goal 1/1 H := (((a b) b) a b) H0 := (a b) b H1 := a a %PhoX% axiom H1. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero10 = (((a b) b) a b) : theorem bye