>PhoX> Import PA.
Loading PA
*** adding constants: $* N0 $S $+ N
*** adding axioms: A5 A4 P0 A1 A2 A3 A6 A7
>PhoX> Cst A : N  N  N.
A : N  N  N
>PhoX> claim A0y y A N0 y = S y.
A0y = y A N0 y = S y : theorem
>PhoX> claim ASx0 x A (S x) N0 = A x (S  N0).
ASx0 = x A (S x) N0 = A x (S N0)
                                          : theorem
>PhoX> claim ASxSy x,y A (S x) (S y) = A x (A (S x) y).

ASxSy = x,y A (S x) (S y) = A x (A (S x) y) : theorem
>PhoX> goal x,y (A x y > y).
Here is the goal:
goal 1/1
    x,y A x y > y

%PhoX% intro.
1 goal created.

goal 1/1
    y A x y > y

%PhoX% elim P0 with x.
2 goals created.

goal 2/2
    x0 (y A x0 y > y  y A (S x0) y > y)

goal 1/2
    y A N0 y > y

%PhoX% rewrite A0y.
1 goal created.

goal 1/2
    y S y > y

%PhoX% intros.
1 goal created.

goal 1/2
    S y > y

%PhoX% intros.
1 goal created.

goal 1/2
    S y = S y + ?1

%PhoX% instance ?1 N0.
Here are the goals:
goal 2/2
    x0 (y A x0 y > y  y A (S x0) y > y)

goal 1/2
    S y = S y + N0

%PhoX% rewrite A4.
1 goal created.

goal 1/2
    S y = S y

%PhoX% intro.
0 goal created.

goal 1/1
    x0 (y A x0 y > y  y A (S x0) y > y)

%PhoX% intros.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
    A (S x0) y > y

%PhoX% elim P0 with y.
2 goals created.

goal 2/2
H := y0 A x0 y0 > y0
    x1 (A (S x0) x1 > x1  A (S x0) (S x1) > S x1)

goal 1/2
H := y0 A x0 y0 > y0
    A (S x0) N0 > N0

%PhoX% rewrite ASx0.
1 goal created.

goal 1/2
H := y0 A x0 y0 > y0
    A x0 (S N0) > N0

%PhoX% elim H with S N0.
1 goal created.

goal 1/2
H := y0 A x0 y0 > y0
H0 := A x0 (S N0) = S S N0 + z
    A x0 (S N0) > N0

%PhoX% intros.
1 goal created.

goal 1/2
H := y0 A x0 y0 > y0
H0 := A x0 (S N0) = S S N0 + z
    A x0 (S N0) = S N0 + ?2

%PhoX% instance ?2 S z.
Here are the goals:
goal 2/2
H := y0 A x0 y0 > y0
    x1 (A (S x0) x1 > x1  A (S x0) (S x1) > S x1)

goal 1/2
H := y0 A x0 y0 > y0
H0 := A x0 (S N0) = S S N0 + z
    A x0 (S N0) = S N0 + S z

%PhoX% rewrite H0 A5 A5'.
1 goal created.

goal 1/2
H := y0 A x0 y0 > y0
H0 := A x0 (S N0) = S S N0 + z
    S S (N0 + z) = S S (N0 + z)

%PhoX% intro.
0 goal created.

goal 1/1
H := y0 A x0 y0 > y0
    x1 (A (S x0) x1 > x1  A (S x0) (S x1) > S x1)

%PhoX% intros.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
    A (S x0) (S x1) > S x1

%PhoX% rewrite ASxSy.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
    A x0 (A (S x0) x1) > S x1

%PhoX% elim H with A (S x0) x1.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
H1 := A x0 (A (S x0) x1) = S A (S x0) x1 + z
    A x0 (A (S x0) x1) > S x1

%PhoX% elim H0.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
H1 := A x0 (A (S x0) x1) = S A (S x0) x1 + z
H2 := A (S x0) x1 = S x1 + z0
    A x0 (A (S x0) x1) > S x1

%PhoX% rewrite H1 H2.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
H1 := A x0 (A (S x0) x1) = S A (S x0) x1 + z
H2 := A (S x0) x1 = S x1 + z0
    S (S x1 + z0) + z > S x1

%PhoX% intros.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
H1 := A x0 (A (S x0) x1) = S A (S x0) x1 + z
H2 := A (S x0) x1 = S x1 + z0
    S (S x1 + z0) + z = S S x1 + ?3

%PhoX% rewrite plus_assoc A5 A5'.
1 goal created.

goal 1/1
H := y0 A x0 y0 > y0
H0 := A (S x0) x1 > x1
H1 := A x0 (A (S x0) x1) = S A (S x0) x1 + z
H2 := A (S x0) x1 = S x1 + z0
    S S (x1 + z0 + z) = S S (x1 + ?3)

%PhoX% intro.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = x,y A x y > y : theorem

bye