>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