Online Otter-λ

Examples

Examples -> PeanoArithmetic -> le2.prf

1 [] a!=0.
3 [] s(x)!=0.
6 [] ap(y,0)|ap(y,s(g(y)))| -ap(y,z).
9 [] -exists(lambda(x,ap(Z,x)))|ap(Z,e(Z)).
11 [] x+0=x.
12 [] x+s(y)=s(x+y).
13 [] (u<=v)=exists(lambda(x,u+x=v)).
14 [] a<=0.
16 [14,demod,13] exists(lambda(x,a+x=0)).
17 [binary,16.1,9.1,demod,beta] a+e(lambda(x,a+x=0))=0.
18 [binary,17.1,6.3,demod,beta,11,beta,12,unit_del,1,3] $F.