Examples
Examples -> PeanoArithmetic -> PA-cancellation.prf1 [] x+0=x.
4 [] s(x)!=s(y)|x=y.
8 [] ap(y,0)| -ap(y,g(y))| -ap(y,z).
9 [] ap(y,0)|ap(y,s(g(y)))| -ap(y,z).
10 [] x+s(y)=s(x+y).
12 [] a+n=b+n.
13 [] a!=b.
16 [binary,12.1,9.3,demod,beta,1,1,beta,unit_del,13] a+s(g(lambda(x,a+x=b+x)))=b+s(g(lambda(x,a+x=b+x))).
17 [binary,12.1,8.3,demod,beta,1,1,beta,unit_del,13] a+g(lambda(x,a+x=b+x))!=b+g(lambda(x,a+x=b+x)).
21 [binary,17.1,4.2] s(a+g(lambda(x,a+x=b+x)))!=s(b+g(lambda(x,a+x=b+x))).
23 [para_into,16.1.2,10.1.1] a+s(g(lambda(x,a+x=b+x)))=s(b+g(lambda(x,a+x=b+x))).
189 [para_into,21.1.1,10.1.2] a+s(g(lambda(x,a+x=b+x)))!=s(b+g(lambda(x,a+x=b+x))).
190 [binary,189.1,23.1] $F.
