Online Otter-λ

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

Examplessmall logo



Examples -> PeanoArithmetic -> le2.in


% prove x <= 0 implies x = 0
% from the definition of <= in PA in terms of exists

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


list(usable).
a != 0.
x = x.
s(x) != 0.
s(x) != s(y) | x = y.
ap(y,0) | -ap(y,g(y)) | -ap(y,z).
ap(y,0) | ap(y,s(g(y))) | -ap(y,z).
x+0 = 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
end_of_list.

list(demodulators).
(x+y)+z = x + y+z.
x+0 = x.
x + s(y) = s(x+y).
(u <= v) = exists(lambda(x,u+x = v)).
end_of_list.

list(sos).
a <= 0.
end_of_list.