Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



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.