>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