>PhoX> Sort term. Sort term defined >PhoX> Cst R : term term prop. R : term term prop >PhoX> Cst f : term term term. f : term term term >PhoX> goal >PhoX> x,y,z (R x y R y z R x z) >PhoX> x,y,z (R(f (f x y) z) (f x (f y z))) >PhoX> x,y,z (R x y R (f x z) (f y z)) >PhoX> x,y (R x y R y x) >PhoX> x,y,u,v (R (f x (f (f y u) v)) (f (f (f x y) u) v)). Here is the goal: goal 1/1 x,y,z (R x y R y z R x z) x,y,z R (f (f x y) z) (f x (f y z)) x,y,z (R x y R (f x z) (f y z)) x,y (R x y R y x) x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v) %PhoX% intro A1 A2 A3 A4. 1 goal created. goal 1/1 A1 := x,y,z (R x y R y z R x z) A2 := x,y,z R (f (f x y) z) (f x (f y z)) A3 := x,y,z (R x y R (f x z) (f y z)) A4 := x,y (R x y R y x) x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v) %PhoX% intros. 1 goal created. goal 1/1 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f x (f (f y u) v)) (f (f (f x y) u) v) %PhoX% elim A4. 1 goal created. goal 1/1 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f (f x y) u) v) (f x (f (f y u) v)) %PhoX% elim A1. 1 goal created. goal 1/1 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f (f x y) u) v) ?1 R ?1 (f x (f (f y u) v)) %PhoX% intro. 2 goals created. goal 2/2 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R ?1 (f x (f (f y u) v)) goal 1/2 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f (f x y) u) v) ?1 %PhoX% next. Here are the goals: goal 2/2 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f (f x y) u) v) ?1 goal 1/2 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R ?1 (f x (f (f y u) v)) %PhoX% elim A2. 0 goal created. goal 1/1 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f (f x y) u) v) (f (f x (f y u)) v) %PhoX% elim A3. 1 goal created. goal 1/1 A1 := x0,y0,z (R x0 y0 R y0 z R x0 z) A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z)) A3 := x0,y0,z (R x0 y0 R (f x0 z) (f y0 z)) A4 := x0,y0 (R x0 y0 R y0 x0) R (f (f x y) u) (f x (f y u)) %PhoX% elim A2. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = x,y,z (R x y R y z R x z) x,y,z R (f (f x y) z) (f x (f y z)) x,y,z (R x y R (f x z) (f y z)) x,y (R x y R y x) x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v) : theorem bye