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

Online Otter-λ

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

Examplessmall logo



Examples -> SetTheory -> cantor2.prf


1 [] w!=not(w).
2 [] u!=v|v=u.
4 [] Ap(x,z)=Ap(Ap(c,J(x)),z)|$ANS(x)|$ANS(z).
5 [binary,4.1,2.1] $ANS(x)|$ANS(y)|Ap(Ap(c,J(x)),y)=Ap(x,y).
6 [binary,5.1,1.1] $ANS(lambda(x,not(Ap(Ap(c,x),x))))|$ANS(J(lambda(x,not(Ap(Ap(c,x),x))))).