Online Otter-λ
-->
Examples
2 [] x<=x.
3 [] x+1!=0.
7 [] -ap(y,o)|ap(y,g(y))|ap(y,z).
8 [] -ap(y,o)| -ap(y,s(g(y)))|ap(y,z).
10 [] -(x<y)| -(z<=x)|z<y.
12 [] -(x<=y)| -(y<x).
13 [] 0<a+1.
17 [] -(x<=y)| -(0<z)|z*x<=y*z.
19 [] -(x<y)|x+ -y<0.
22 [] x^o=1|x=0.
23 [] 0<=i(x).
25 [] i(o)=0.
26 [] i(s(x))=i(x)+1.
27 [] x^s(y)=x*x^y.
28 [] x*0=0.
30 [] 0+x=x.
33 [] x^ (y+z)=x^y*x^z.
34 [] x^1=x.
35 [] -(1+i(n)*a<= (1+a)^n).
36 [simplify,35] (a+1)^n<a*i(n)+1.
41 [binary,36,12] -(a*i(n)+1<= (a+1)^n).
43 [binary,41,8,demod,beta,25,28,30,beta,26,27] -(1<= (a+1)^o)| -(a* (i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1)+1<= (a+1)* (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x))).
44 [binary,41,7,demod,beta,25,28,30,beta] -(1<= (a+1)^o)|a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1<= (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x)).
85 [para_into,43,22,unit_del,2,3] -(a* (i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1)+1<= (a+1)* (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x))).
117 [para_into,44,22,unit_del,2,3] a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1<= (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x)).
119 [hyper,117,17,13] (a+1)* (a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1)<= (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x))* (a+1).
160 [para_into,43,22,unit_del,2,3,simplify,85,demod,33,34] (a+1)^g(lambda(x,a*i(x)+1<= (a+1)^x))* (a+1)<a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+a+1.
298 [hyper,119,10,160] (a+1)* (a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1)<a*i(g(lambda(y,a*i(y)+1<= (a+1)^y)))+a+1.
299 [binary,298,19] (a+1)* (a*i(g(lambda(x,a*i(x)+1<= (a+1)^x)))+1)+ -(a*i(g(lambda(y,a*i(y)+1<= (a+1)^y)))+a+1)<0.
398 [binary,298,19,simplify,299] and(a!=0,i(g(lambda(x,a*i(x)+1<= (a+1)^x)))<0).
404 [split and,398] i(g(lambda(x,a*i(x)+1<= (a+1)^x)))<0.
412 [binary,404,12] -(0<=i(g(lambda(x,a*i(x)+1<= (a+1)^x)))).
413 [binary,412,23] $F.