Online Otter-λ

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

Examplessmall logo



Examples -> LambdaLogic -> lambda4.prf


1 [] x=x.
2 [] ap(c,ap(lambda(x,ap(c,ap(x,x))),lambda(x,ap(c,ap(x,x)))))!=ap(lambda(x,ap(c,ap(x,x))),lambda(x,ap(c,ap(x,x)))).
3 [binary,2.1,1.1] $F.