>PhoX> Sort term. Sort term defined >PhoX> Cst R : term term prop. R : term term prop >PhoX> Cst S : term prop. S : term prop >PhoX> def F = x R x x x,y(R x y R y x) x,y,z(R x y R y z R x z). F = x R x x x,y (R x y R y x) x,y,z (R x y R y z R x z) : prop >PhoX> def G = x,y (S x (R x y S y)). G = x,y (S x R x y S y) : prop >PhoX> def H = x S x x(S x y (S y R x y)). H = x S x x:S y (S y R x y) : prop >PhoX> goal F (G H). Here is the goal: goal 1/1 F G H %PhoX% intro 3. 2 goals created. goal 2/2 H0 := F H1 := H G goal 1/2 H0 := F H1 := G H %PhoX% intro. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x S x x:S y (S y R x y) %PhoX% elim H2. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x x0:S y (S y R x0 y) %PhoX% intro. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x S ?1 y (S y R ?1 y) %PhoX% instance ?1 x. Here are the goals: goal 2/2 H0 := F H1 := H G goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x S x y (S y R x y) %PhoX% intro . 2 goals created. goal 2/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x y (S y R x y) goal 1/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x S x %PhoX% axiom H3. 0 goal created. goal 2/2 H0 := F H1 := H G goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x y (S y R x y) %PhoX% intro 2. 2 goals created. goal 2/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x R x y S y goal 1/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x S y R x y %PhoX% intro. 1 goal created. goal 1/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := S y R x y %PhoX% apply -2 (y) -3 H3 H1. 1 goal created. goal 1/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := S y G0 := R x y S y R x y %PhoX% elim G0. 1 goal created. goal 1/3 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := S y G0 := R x y S y S y %PhoX% axiom H4. 0 goal created. goal 2/2 H0 := F H1 := H G goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x R x y S y %PhoX% intro. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := R x y S y %PhoX% apply -2 (y) -3 H3 H1. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := R x y G0 := R x y S y S y %PhoX% elim G0. 1 goal created. goal 1/2 H0 := F H1 := G H2 := x0 S x0 H3 := S x H4 := R x y G0 := R x y S y R x y %PhoX% axiom H4. 0 goal created. goal 1/1 H0 := F H1 := H G %PhoX% intro 3. 1 goal created. goal 1/1 H0 := F H1 := H H2 := S x R x y S y %PhoX% use x(S x y(S y R x y)). 2 goals created. goal 2/2 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 1/2 H0 := F H1 := H H2 := S x G0 := x0:S y0 (S y0 R x0 y0) R x y S y %PhoX% elim G0. 1 goal created. goal 1/2 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 y0 (S y0 R x0 y0) R x y S y %PhoX% left H3. 1 goal created. goal 1/2 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x y S y %PhoX% use R x0 x. 2 goals created. goal 2/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x R x y S y %PhoX% intro 2. 2 goals created. goal 2/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y R x y goal 1/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y S y %PhoX% elim H4. 1 goal created. goal 1/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y R x0 y %PhoX% left H0. 1 goal created. goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x0 y %PhoX% elim H6. 1 goal created. goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x0 ?2 R ?2 y %PhoX% instance ?2 x. Here are the goals: goal 4/4 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 3/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 2/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y R x y goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x0 x R x y %PhoX% intro. 2 goals created. goal 2/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x y goal 1/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x0 x %PhoX% axiom G1. 0 goal created. goal 4/4 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 3/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 2/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y R x y goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := R x y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H6 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x y %PhoX% axiom H5. 0 goal created. goal 3/3 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 2/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y R x y %PhoX% elim H4. 1 goal created. goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S ?3 R x0 ?3 H7 := R x0 ?3 S ?3 R x y %PhoX% instance ?3 y. Here are the goals: goal 3/3 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 2/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x y %PhoX% use R x0 y. 2 goals created. goal 2/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x0 y goal 1/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y R x y %PhoX% left H0. 1 goal created. goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H0 := x1 R x1 x1 x1,y0 (R x1 y0 R y0 x1) H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) R x y %PhoX% left H0. 1 goal created. goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x y %PhoX% use R x x0. 2 goals created. goal 2/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x x0 goal 1/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x y %PhoX% elim H8. 1 goal created. goal 1/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x ?4 R ?4 y %PhoX% instance ?4 x0. Here are the goals: goal 5/5 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 4/5 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 3/5 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x0 y goal 2/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x x0 goal 1/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x x0 R x0 y %PhoX% intro. 2 goals created. goal 2/6 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x0 y goal 1/6 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x x0 %PhoX% axiom G3. 0 goal created. goal 5/5 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 4/5 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 3/5 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x0 y goal 2/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x x0 goal 1/5 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) G3 := R x x0 R x0 y %PhoX% axiom G2. 0 goal created. goal 4/4 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 3/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 2/4 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x0 y goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x x0 %PhoX% elim H9. 1 goal created. goal 1/4 H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y G2 := R x0 y H8 := x1,y0,z (R x1 y0 R y0 z R x1 z) H0 := x1 R x1 x1 H9 := x1,y0 (R x1 y0 R y0 x1) R x0 x %PhoX% axiom G1. 0 goal created. goal 3/3 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 2/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y R x0 y %PhoX% elim H6. 1 goal created. goal 1/3 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) G1 := R x0 x H5 := S y H6 := S y R x0 y H7 := R x0 y S y S y %PhoX% axiom H5. 0 goal created. goal 2/2 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) goal 1/2 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) R x0 x %PhoX% elim H4. 1 goal created. goal 1/2 H0 := F H1 := H H2 := S x G0 := x1:S y0 (S y0 R x1 y0) H3 := S x0 H4 := y0 (S y0 R x0 y0) S x %PhoX% axiom H2. 0 goal created. goal 1/1 H0 := F H1 := H H2 := S x x0:S y0 (S y0 R x0 y0) %PhoX% elim H1. 1 goal created. goal 1/1 H0 := F H1 := H H2 := S x x0 S x0 %PhoX% intro. 1 goal created. goal 1/1 H0 := F H1 := H H2 := S x S ?5 %PhoX% axiom H2. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = F G H : theorem bye