Online Otter-λ

Examples

Examples -> LambdaLogic -> divides.prf

2 [] 2*3=6.
3 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).
4 [] divides(u,v)=exists(lambda(x,u*x=v)).
5 [] -divides(2,6).
6 [5,demod,4] -exists(lambda(x,2*x=6)).
7 [binary,6.1,3.2,demod,beta] 2*x!=6.
8 [binary,7.1,2.1] $F.