pred: P(2),Q(1)
const: a
func: f(1)
-
Ax(Qx>Pxa)
Qfa
:Pfaa
pred: P(1),Q(1)
const: a
-
Ax(Pa>Qx)
Pa
:AxQx
pred: P(1)
const: a
-
Pa
:-Ax-Px
pred: P(1)
-
AxPx
:AyPy
func: f(1)
-
x=y
:fx=fy
-
:(x=y>(y=z>x=z))
func: f(1)
-
:-Ay-y=fx
func: f(1)
pred: P(1)
const: c,d
-
fc=d
Pfc
:Pd
pred: P(2)
-
AxAyPxy
:AyPyy
pred: R(2)
const: a,b
-
AxAyAz(Rxy>(Ryz>Rxz)
Ax(-Rxx)
:(Rab>-Rba)
pred: P(1),Q(1)
-
Ax(Px>Qx)
-Ax-Px
:-Ax-Qx