Online Otter-λ
-->
Examples
1 [] a!=0.
2 [] a!=s(0).
3 [] x=x.
4 [] s(x)!=0.
5 [] s(x)!=s(y)|x=y.
6 [] ap(y,0)| -ap(y,g(y))| -ap(y,z).
7 [] ap(y,0)|ap(y,s(g(y)))| -ap(y,z).
8 [] x+0=x.
9 [] -ap(Z,w)|exists(lambda(x,ap(Z,x))).
10 [] -exists(lambda(x,ap(Z,x)))|ap(Z,e(Z)).
12 [] x+0=x.
13 [] x+s(y)=s(x+y).
14 [] (u<=v)=exists(lambda(x,u+x=v)).
15 [] a<=s(0).
18 [binary,15.1,7.3,demod,14,beta,14,14,beta,factor_simp] exists(lambda(x,a+x=s(0))).
19 [binary,18.1,10.1,demod,beta] a+e(lambda(x,a+x=s(0)))=s(0).
21 [binary,19.1,7.3,demod,beta,12,beta,13,unit_del,2] s(a+g(lambda(x,a+x=s(0))))=s(0).
22 [binary,19.1,6.3,demod,beta,12,beta,unit_del,2] a+g(lambda(x,a+x=s(0)))!=s(0).
32 [binary,21.1,5.1] a+g(lambda(x,a+x=s(0)))=0.
34 [para_from,21.1.1,5.1.2] s(x)!=s(0)|x=a+g(lambda(y,a+y=s(0))).
44 [binary,32.1,9.1,demod,beta] exists(lambda(x,a+g(lambda(y,a+y=s(0)))=0)).
45 [para_from,32.1.1,22.1.1] 0!=s(0).
46 [para_from,32.1.2,8.1.1.2] x+a+g(lambda(y,a+y=s(0)))=x.
49 [para_from,32.1.2,1.1.2] a!=a+g(lambda(x,a+x=s(0))).
90 [para_into,44.1.1.2.1,32.1.1] exists(lambda(x,0=0)).
92 [para_into,90.1.1.2.2,32.1.2] exists(lambda(x,0=a+g(lambda(y,a+y=s(0))))).
130 [binary,92.1,10.1,demod,beta] 0=a+g(lambda(x,a+x=s(0))).
176 [para_from,34.2.2,130.1.2] 0=x|s(x)!=s(0).
182 [para_from,34.2.2,49.1.2] a!=x|s(x)!=s(0).
195 [binary,176.2,7.2,demod,beta,beta,unit_del,45] 0=g(lambda(x,x=s(0)))|y!=s(0).
248 [binary,195.2,46.1] 0=g(lambda(x,x=s(0))).
252 [para_into,248.1.1,130.1.1] a+g(lambda(x,a+x=s(0)))=g(lambda(y,y=s(0))).
267 [para_from,248.1.1,4.1.2] s(x)!=g(lambda(y,y=s(0))).
358 [binary,182.1,7.1,demod,beta,beta,unit_del,3] a=s(g(lambda(x,a=x)))|a!=y.
370 [binary,358.2,3.1] a=s(g(lambda(x,a=x))).
375 [para_from,370.1.1,252.1.1.1] s(g(lambda(x,a=x)))+g(lambda(y,a+y=s(0)))=g(lambda(z,z=s(0))).
441 [binary,375.1,7.3,demod,beta,12,beta,13,unit_del,267,267] $F.