>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