>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