Online Otter-λ

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

Examplessmall logo



Examples -> LambdaLogic -> divides.in


% prove divides(2,6) to illustrate the use of "exists" in lambda logic.

set(lambda).
set(demod_inf).
set(binary_res).
set(very_verbose).

list(usable).
x = x.
2*3 = 6.
-Ap(Z,w) | exists(lambda(x, Ap(Z,x))).
end_of_list.

list(demodulators).
divides(u,v) = exists(lambda(x,u*x = v)).
end_of_list.

list(sos).
-divides(2,6).
end_of_list.