Online Otter-λ
-->
Examples
2 [] sum(u,v,x,x)=Ap(lambda(u,v),x).
4 [] sum(u,v,x,y+1)=sum(u,v,x,y)+Ap(lambda(u,v),1+y).
7 [] x+1!=y+1|x=y.
8 [] -Ap(y,0)|Ap(y,g(y))|Ap(y,z).
9 [] -Ap(y,0)| -Ap(y,g(y)+1)|Ap(y,z).
10 [] 2*sum(x,x,0,n)!=n* (n+1).
11 [binary,10,9,demod,beta,2,beta,beta,4,beta,simplify] 2* (sum(x,x,0,g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))+1+g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))!= (1+g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))* (2+g(lambda(y,2*sum(z,z,0,y)=y* (y+1)))).
12 [binary,10,8,demod,beta,2,beta,beta,simplify] 2*sum(x,x,0,g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))= (1+g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))*g(lambda(y,2*sum(z,z,0,y)=y* (y+1))).
22 [binary,11,7,simplify] 2*g(lambda(y,2*sum(z,z,0,y)=y* (y+1)))+2*sum(x,x,0,g(lambda(y,2*sum(z,z,0,y)=y* (y+1))))!=3*g(lambda(y,2*sum(z,z,0,y)=y* (y+1)))+g(lambda(y,2*sum(z,z,0,y)=y* (y+1)))^2.
29 [para_into,22,12,simplify] $F.