sent: P,Q
-
P
:(Q>P)
sent: P,Q,R
-
(P>Q)
(Q>R)
:(P>R)
sent: P,Q,R
-
(P>Q)
:(P>(R>Q))
sent: P,Q,R
-
(P>(Q>R))
Q
:(P>R)
sent: P,Q
-
P
-P
:Q
sent: P,Q,R
-
((P>Q)>R)
:(Q>R)
sent: P
-
:((-P>P)>P)
sent: P,Q
-
-(Q>-P)
:P
sent: P
-
--P
:P
sent: P,Q,R
-
(P>(Q>R))
:(Q>(P>R))
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
pred: P(1),Q(1),R(2)
-
AxAy(Px>Qy>Rxy)
Ax(Px>Qx)
:Ax(Px>Rxx)