Examples
Examples -> PeanoArithmetic -> PA-OrderTransitivity.prf8 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).
9 [] -exists(lambda(x,Ap(Z,x)))|Ap(Z,e(Z)).
11 [] -(x<=y)|exists(lambda(z,x+z=y)).
12 [] -exists(lambda(z,x+z=y))|x<=y.
13 [] (x+y)+z=x+y+z.
14 [] a<=b.
15 [] b<=c.
16 [] -(a<=c).
17 [binary,14.1,11.1] exists(lambda(x,a+x=b)).
19 [binary,15.1,11.1] exists(lambda(x,b+x=c)).
21 [binary,16.1,12.2] -exists(lambda(x,a+x=c)).
31 [binary,17.1,9.1,demod,beta] a+e(lambda(x,a+x=b))=b.
33 [binary,19.1,9.1,demod,beta] b+e(lambda(x,b+x=c))=c.
36 [binary,21.1,8.2,demod,beta] a+x!=c.
40 [para_into,36.1.1,13.1.2] (a+x)+y!=c.
367 [para_into,33.1.1.1,31.1.2] (a+e(lambda(x,a+x=b)))+e(lambda(y,b+y=c))=c.
368 [binary,367.1,40.1] $F.
