Online Otter-λ

Examples

Examples -> LambdaLogic -> lambda.prf


1 [] x=x.
2 [] x*x=x.
3 [] ap(ap(lambda(x,lambda(y,x)),c*c),y)!=c|ap(lambda(x,lambda(y,x)),y)!=lambda(z,y)|lambda(x,x)!=lambda(z,z)|lambda(z,a)!=lambda(z,x)|lambda(w,a)!=lambda(z,x).
4 [binary,3.2,1.1,demod,2,beta,beta,unit_del,1,1] lambda(x,a)!=lambda(x,y).
5 [binary,4.1,1.1] $F.