Online Otter-λ

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

Examplessmall logo



Examples -> PeanoArithmetic -> le3.in


% prove x <= s(0) implies x = 0 | x = s(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).
%set(very_verbose).
assign(max_distinct_vars,1).
assign(max_binding_depth,2).
assign(max_weight,32).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($dots(g($(0)))), 1000). % discard nested g terms
weight(g($(0)),1). %every g-term counts like a constant
end_of_list.


list(usable).
a != 0.
a != s(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 <= s(0).
end_of_list.