Examples
Examples -> PeanoArithmetic -> PA-Trichotomy.prf1 [] x+0=x.
2 [] (x+y)+z=x+y+z.
11 [] -exists(lambda(x,Ap(Z,x)))|Ap(Z,e(Z)).
16 [] -(x<=y)|exists(lambda(z,x+z=y)).
18 [] x+y!=x|y=0.
20 [] x+y!=0|y=0.
21 [] a<=b.
22 [] b<=a.
23 [] a!=b.
24 [ur,21,16] exists(lambda(x,a+x=b)).
26 [ur,22,16] exists(lambda(x,b+x=a)).
31 [ur,24,11,demod,beta] a+e(lambda(x,a+x=b))=b.
32 [ur,26,11,demod,beta] b+e(lambda(x,b+x=a))=a.
35 [para_from,31.1.1,18.1.1] b!=a|e(lambda(x,a+x=b))=0.
58 [para_into,32.1.1.1,31.1.2,demod,2] a+e(lambda(x,a+x=b))+e(lambda(y,b+y=a))=a.
66 [para_from,32.1.2,23.1.1] b+e(lambda(x,b+x=a))!=b.
91 [para_from,35.2.1,31.1.1.2,demod,1] a=b|b!=a.
94 [para_into,91.1.1,32.1.2] b+e(lambda(x,b+x=a))=b|b!=a.
275 [ur,58,18] e(lambda(x,a+x=b))+e(lambda(y,b+y=a))=0.
820 [ur,94,66] b!=a.
823 [para_into,820.1.1,31.1.2] a+e(lambda(x,a+x=b))!=a.
1308 [ur,275,20] e(lambda(x,b+x=a))=0.
1321 [para_from,1308.1.1,58.1.1.2.2,demod,1] a+e(lambda(x,a+x=b))=a.
1322 [binary,1321.1,823.1] $F.
