>PhoX> Import PA.
Loading PA
*** adding constants: $* N0 $S $+ N
*** adding axioms: A5 A4 P0 A1 A2 A3 A6 A7
>PhoX> goal F (F N0  F (S N0) x (F x  F (S S x)) x F x).
Here is the goal:
goal 1/1
    F (F N0  F (S N0)  x:F  F (S S x)  x F x)

%PhoX% intro.
1 goal created.

goal 1/1
    F N0  F (S N0)  x:F  F (S S x)  x F x

%PhoX% intro.
1 goal created.

goal 1/1
H := F N0  F (S N0)  x:F  F (S S x)
    x F x

%PhoX% intro.
1 goal created.

goal 1/1
H := F N0  F (S N0)  x0:F  F (S S x0)
    F x

%PhoX% lefts H.
1 goal created.

goal 1/1
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    F x

%PhoX% apply 3 P0 with \x (F x  F (S x)).
3 goals created.

goal 3/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
G := x0 (F x0  F (S x0))
    F x

goal 2/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    x0 (F x0  F (S x0)  F (S x0)  F (S S x0))

goal 1/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    F N0  F (S N0)

%PhoX% intro.
2 goals created.

goal 2/4
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    F (S N0)

goal 1/4
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    F N0

%PhoX% axiom H.
0 goal created.

goal 3/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
G := x0 (F x0  F (S x0))
    F x

goal 2/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    x0 (F x0  F (S x0)  F (S x0)  F (S S x0))

goal 1/3
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    F (S N0)

%PhoX% axiom H1.
0 goal created.

goal 2/2
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
G := x0 (F x0  F (S x0))
    F x

goal 1/2
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
    x0 (F x0  F (S x0)  F (S x0)  F (S S x0))

%PhoX% intro 2.
1 goal created.

goal 1/2
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0  F (S x0)
    F (S x0)  F (S S x0)

%PhoX% left H2.
1 goal created.

goal 1/2
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0
H3 := F (S x0)
    F (S x0)  F (S S x0)

%PhoX% intro.
2 goals created.

goal 2/3
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0
H3 := F (S x0)
    F (S S x0)

goal 1/3
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0
H3 := F (S x0)
    F (S x0)

%PhoX% axiom H3.
0 goal created.

goal 2/2
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
G := x0 (F x0  F (S x0))
    F x

goal 1/2
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0
H3 := F (S x0)
    F (S S x0)

%PhoX% elim H0.
1 goal created.

goal 1/2
H0 := x1:F  F (S S x1)
H := F N0
H1 := F (S N0)
H2 := F x0
H3 := F (S x0)
    F x0

%PhoX% axiom H2.
0 goal created.

goal 1/1
H0 := x0:F  F (S S x0)
H := F N0
H1 := F (S N0)
G := x0 (F x0  F (S x0))
    F x

%PhoX% elim G.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = F (F N0  F (S N0)  x:F  F (S S x)  x F x) : theorem

bye