>PhoX> Sort term. Sort term defined >PhoX> Cst P : term prop. P : term prop >PhoX> Cst R : term prop. R : term prop >PhoX> Cst T : term term prop. T : term term prop >PhoX> Cst S : term prop. S : term prop >PhoX> goal xy(P x (R y T x y))x,y( P x S y T x y) x( R x S x). Here is the goal: goal 1/1 x y (P x (R y T x y)) x,y ( P x S y T x y) x ( R x S x) %PhoX% intro 3. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) R x S x %PhoX% by_absurd. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) H1 := ( R x S x) R x S x %PhoX% rewrite_hyp H1 disjunction.demorgan. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) H1 := R x S x R x S x %PhoX% rewrite_hyp H1 negation.demorgan. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) H1 := R x S x R x S x %PhoX% elim False. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) H1 := R x S x False %PhoX% left H1. 1 goal created. goal 1/1 H := x0 y (P x0 (R y T x0 y)) H0 := x0,y ( P x0 S y T x0 y) H1 := R x H2 := S x False %PhoX% elim H. 1 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) False %PhoX% apply -1 (x) H3. 1 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) G := P x0 (R x T x0 x) False %PhoX% left G. 1 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x False %PhoX% apply -1 (x0) -2 (x) H0. 1 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x False %PhoX% use T x0 x. 2 goals created. goal 2/2 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x T x0 x goal 1/2 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x False %PhoX% elim G. 2 goals created. goal 2/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := T x0 x False goal 1/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x False %PhoX% elim H6. 2 goals created. goal 2/4 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x H7 := S x False goal 1/4 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x H7 := P x0 False %PhoX% elim H7. 1 goal created. goal 1/4 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x H7 := P x0 P x0 %PhoX% axiom H4. 0 goal created. goal 3/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x T x0 x goal 2/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := T x0 x False goal 1/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x H7 := S x False %PhoX% elim H7. 1 goal created. goal 1/3 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := P x0 S x H7 := S x S x %PhoX% axiom H2. 0 goal created. goal 2/2 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x T x0 x goal 1/2 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := T x0 x False %PhoX% elim H6. 1 goal created. goal 1/2 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x G0 := T x0 x H6 := T x0 x T x0 x %PhoX% axiom G0. 0 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x T x0 x %PhoX% elim H5. 1 goal created. goal 1/1 H := x1 y (P x1 (R y T x1 y)) H0 := x1,y ( P x1 S y T x1 y) H1 := R x H2 := S x H3 := y (P x0 (R y T x0 y)) H4 := P x0 H5 := R x T x0 x G := P x0 S x T x0 x R x %PhoX% axiom H1. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = x y (P x (R y T x y)) x,y ( P x S y T x y) x ( R x S x) : theorem bye