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
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