Online Otter-λ

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

Examplessmall logo



Examples -> LambdaLogic -> divides2.in


% prove the transitivity of "divides"
% this uses the "second law of existence", formulated using Hilbert's epsilon symbol

set(lambda).
set(demod_inf).
set(binary_res).
set(para_into).
set(para_from).
assign(max_distinct_vars,1).
assign(max_weight,32).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($(0),$(0)),1). %every g-term counts like a constant
end_of_list.


list(usable).
x = x.
-Ap(Z,w) | exists(lambda(x, Ap(Z,x))). % first law of existence
-exists(lambda(x,Ap(Z,x))) | Ap(Z, e(Z)). % second law of existence
% e is Hilbert's epsilon ex.Zx = e(lambda(x,Ap(Z,x))) = e(Z).
% or, we could formulate this using Ap(e,Z) instead of e(Z).
divides(u,v) = exists(lambda(x,u*x = v)).
end_of_list.

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

list(sos).
divides(a,b).
divides(b,c).
-divides(a,c).
end_of_list.