>PhoX> Sort term. Sort term defined >PhoX> Cst R : term term prop. R : term term prop >PhoX> Cst Infix[3] x "o" y : term term term. $o : term term term >PhoX> Cst Infix[3] x "#" y : term term term. $# : term term term >PhoX> Cst Infix[5] x "<=" y : term term prop. $<= : term term prop >PhoX> goal >PhoX> x,a,b ((R x (a o b))y(x <= y (R y a R y b))) >PhoX> x,a,b (R x (a # b) (R x a R x b)) >PhoX> x,y,z (x <= y x <= z (y <= z z <= y)) >PhoX> x,y,a (R x a x <= y (R y a)) >PhoX> x,a,b (R x ((a o b) # (b o a))). Here is the goal: goal 1/1 x,a,b (R x (a o b) y (x <= y R y a R y b)) x,a,b (R x (a # b) R x a R x b) x,y,z (x <= y x <= z y <= z z <= y) x,y,a (R x a x <= y R y a) x,a,b R x ((a o b) # (b o a)) %PhoX% intro F1 F2 F3 F4. 1 goal created. goal 1/1 F1 := x,a,b (R x (a o b) y (x <= y R y a R y b)) F2 := x,a,b (R x (a # b) R x a R x b) F3 := x,y,z (x <= y x <= z y <= z z <= y) F4 := x,y,a (R x a x <= y R y a) x,a,b R x ((a o b) # (b o a)) %PhoX% intro 3. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) R x ((a o b) # (b o a)) %PhoX% elim F2 with [r]. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) R x (a o b) R x (b o a) %PhoX% by_absurd. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := (R x (a o b) R x (b o a)) R x (a o b) R x (b o a) %PhoX% elim False. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := (R x (a o b) R x (b o a)) False %PhoX% rewrite_hyp H demorganl. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := R x (a o b) R x (b o a) False %PhoX% left H. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := R x (a o b) H0 := R x (b o a) False %PhoX% elim H. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := R x (a o b) H0 := R x (b o a) R x (a o b) %PhoX% elim F1 with [r]. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y (x0 <= y R y a0 R y b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y,z (x0 <= y x0 <= z y <= z z <= y) F4 := x0,y,a0 (R x0 a0 x0 <= y R y a0) H := R x (a o b) H0 := R x (b o a) y (x <= y R y a R y b) %PhoX% intros. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y0 (x0 <= y0 R y0 a0 R y0 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y0,z (x0 <= y0 x0 <= z y0 <= z z <= y0) F4 := x0,y0,a0 (R x0 a0 x0 <= y0 R y0 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a R y b %PhoX% by_absurd. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y0 (x0 <= y0 R y0 a0 R y0 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y0,z (x0 <= y0 x0 <= z y0 <= z z <= y0) F4 := x0,y0,a0 (R x0 a0 x0 <= y0 R y0 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b R y b %PhoX% elim H0. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y0 (x0 <= y0 R y0 a0 R y0 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y0,z (x0 <= y0 x0 <= z y0 <= z z <= y0) F4 := x0,y0,a0 (R x0 a0 x0 <= y0 R y0 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b R x (b o a) %PhoX% elim F1 with [r]. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y0 (x0 <= y0 R y0 a0 R y0 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y0,z (x0 <= y0 x0 <= z y0 <= z z <= y0) F4 := x0,y0,a0 (R x0 a0 x0 <= y0 R y0 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b y0 (x <= y0 R y0 b R y0 a) %PhoX% intros. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b R y0 a %PhoX% by_absurd. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a R y0 a %PhoX% elim F3 with H1 and H4. 2 goals created. goal 2/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y0 a goal 1/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 R y0 a %PhoX% elim H6. 1 goal created. goal 1/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 R y0 a %PhoX% elim F4 with H2 H7. 1 goal created. goal 1/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 R y a y <= y0 %PhoX% intro. 2 goals created. goal 2/3 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 y <= y0 goal 1/3 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 R y a %PhoX% axiom H2. 0 goal created. goal 2/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y0 a goal 1/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y <= y0 y <= y0 %PhoX% axiom H7. 0 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y0 a %PhoX% elim H3. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y b %PhoX% elim F4 with H5 H7. 1 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y0 b y0 <= y %PhoX% intro. 2 goals created. goal 2/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y y0 <= y goal 1/2 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y R y0 b %PhoX% axiom H5. 0 goal created. goal 1/1 F1 := x0,a0,b0 (R x0 (a0 o b0) y1 (x0 <= y1 R y1 a0 R y1 b0)) F2 := x0,a0,b0 (R x0 (a0 # b0) R x0 a0 R x0 b0) F3 := x0,y1,z (x0 <= y1 x0 <= z y1 <= z z <= y1) F4 := x0,y1,a0 (R x0 a0 x0 <= y1 R y1 a0) H := R x (a o b) H0 := R x (b o a) H1 := x <= y H2 := R y a H3 := R y b H4 := x <= y0 H5 := R y0 b H6 := R y0 a H7 := y0 <= y y0 <= y %PhoX% axiom H7. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = x,a,b (R x (a o b) y (x <= y R y a R y b)) x,a,b (R x (a # b) R x a R x b) x,y,z (x <= y x <= z y <= z z <= y) x,y,a (R x a x <= y R y a) x,a,b R x ((a o b) # (b o a)) : theorem bye