Online Otter-λ

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

Examplessmall logo



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.