skip to: page content | links on this page | site navigation | footer (site information)

Online Otter-λ

Utility Link | Utility Link | Utility Link
Upload | Enter | Create
Algebra | ExternalSimplification | FirstOrderLogic | Induction | More >
-->

Examplessmall logo



Examples -> PeanoArithmetic -> PA-multcom.prf


1 [] x+0=x.
2 [] x*0=0.
3 [] 0*x=0.
12 [] x=x.
15 [] -ap(y,0)|ap(y,g(z,y))|ap(y,z).
16 [] -ap(y,0)| -ap(y,s(g(z,y)))|ap(y,z).
18 [] x+y+z= (x+y)+z.
19 [] x+y=y+x.
20 [] x*s(y)=x*y+x.
21 [] x+s(y)=s(x)+y.
23 [] m*n!=n*m.
24 [binary,23.1,16.3,demod,beta,3,2,beta,unit_del,12] s(g(m,lambda(x,x*n=n*x)))*n!=n*s(g(m,lambda(x,x*n=n*x))).
25 [binary,23.1,15.3,demod,beta,3,2,beta,unit_del,12] g(m,lambda(x,x*n=n*x))*n=n*g(m,lambda(x,x*n=n*x)).
28 [para_from,25.1.2,20.1.2.1] n*s(g(m,lambda(x,x*n=n*x)))=g(m,lambda(x,x*n=n*x))*n+n.
54 [para_from,28.1.1,24.1.2] s(g(m,lambda(x,x*n=n*x)))*n!=g(m,lambda(y,y*n=n*y))*n+n.
125 [binary,54.1,16.3,demod,beta,2,2,1,beta,unit_del,12] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))!=g(m,lambda(x,x*n=n*x))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))+s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))).
126 [binary,54.1,15.3,demod,beta,2,2,1,beta,unit_del,12] s(g(m,lambda(x,x*n=n*x)))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))=g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)).
230 [para_from,126.1.1,20.1.2.1] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))= (g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))+s(g(m,lambda(x,x*n=n*x))).
877 [para_into,125.1.2.1,20.1.1] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))!= (g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+g(m,lambda(x,x*n=n*x)))+s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))).
1773 [para_into,230.1.2,18.1.2] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))=g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+s(g(m,lambda(x,x*n=n*x))).
21899 [para_into,877.1.2,18.1.2] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))!=g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+g(m,lambda(x,x*n=n*x))+s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))).
23692 [para_into,1773.1.2.2,19.1.2] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))=g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+s(g(m,lambda(x,x*n=n*x)))+g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)).
89895 [para_into,21899.1.2.2,21.1.1] s(g(m,lambda(x,x*n=n*x)))*s(g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)))!=g(m,lambda(x,x*n=n*x))*g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y))+s(g(m,lambda(x,x*n=n*x)))+g(n,lambda(y,s(g(m,lambda(z,z*n=n*z)))*y=g(m,lambda(u,u*n=n*u))*y+y)).
89896 [binary,89895.1,23692.1] $F.