Online Otter-λ
-->
Examples
1 [] x=x.
2 [] u*x=v|u!=v*i(x).
3 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).
4 [] f(w)=exists(lambda(x,and(H(x),x*a=w))).
5 [] H(g(X)).
6 [] -f(Ap(X,g(X)))|$ANS(X)|Ap(X,Ap(Y,r(Y)))!=r(Y)|$ANS(Y).
10 [6,demod,4] -exists(lambda(x,and(H(x),x*a=Ap(y,g(y)))))|$ANS(y)|Ap(y,Ap(z,r(z)))!=r(z)|$ANS(z).
22 [binary,10.1,3.2,demod,beta] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -and(H(z),z*a=Ap(x,g(x))).
23 [split -and,22] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -H(z)|z*a!=Ap(x,g(x)).
26 [binary,23.3,1.1,demod,beta,unit_del,5] $ANS(lambda(x,x*a))|Ap(y,r(y))*a!=r(y)|$ANS(y).
28 [binary,26.1,2.1] $ANS(lambda(x,x*a))|$ANS(y)|Ap(y,r(y))!=r(y)*i(a).
29 [binary,28.1,1.1] $ANS(lambda(x,x*a))|$ANS(lambda(y,y*i(a))).