Online Otter-λ
-->
Examples
---------------- PROOF ----------------
27 [] 1!=0.
28 [] x*y!=0|x=0|y=0.
30,29 [] pow(s(x),y)=y*pow(x,y).
32,31 [] pow(o,x)=1.
35 [] ap(x,o)| -ap(x,g(y,x))| -ap(x,y).
36 [] ap(x,o)|ap(x,s(g(y,x)))| -ap(x,y).
37 [] b!=0.
39 [] pow(n,b)=0.
41 [binary,39.1,36.3,demod,beta,32,beta,30,unit_del,27] b*pow(g(n,lambda(x,pow(x,b)=0)),b)=0.
43 [binary,39.1,35.3,demod,beta,32,beta,unit_del,27] pow(g(n,lambda(x,pow(x,b)=0)),b)!=0.
136 [binary,41.1,28.1,unit_del,37,43] $F.
------------ end of proof -------------