Examples
Examples -> PeanoArithmetic -> PA-TwoToTheN.in% prove 1 < a => n < a^n in PA
%
set(lambda).
set(binary_res).
set(hyper_res).
set(induction).
set(demod_inf).
set(para_into).
set(para_from).
% set(para_from_units_only).
assign(max_distinct_vars,0).
assign(max_binding_depth,1).
assign(max_weight,18).
assign(pick_given_ratio,4).
assign(bsub_hint_wt,1).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($(0)),1). %every g-term counts like a constant
end_of_list.
%set(very_verbose).
op(450, xfy, +).
op(440, fx, -). %unary minus should be parenthesized a + (-b) + c
op(400, xfx, /).
op(350, fy, ~).
op(400, xfy, *).
op(300, xfx, ^).
list(demodulators).
x+0 = x.
x*0 = 0.
0*x = 0.
s(s(s(x))) = junk.
x^s(y) = x * x^y. % exponentiation
end_of_list.
list(usable).
% Peano axioms:
x = x.
s(x) != s(y) | x = y.
s(x) != 0.
-ap(y,0) | ap(y,g(y)) | ap(y,z).
-ap(y,0) | -ap(y,s(g(y))) | ap(y,z).
% exponentiation
x = 0 | x^0 = s(0).
% order
- (x < y) | - (y < z) | x < z.
%- (x < y) | - (0 < z) | z*x < z*y.
- (u < v) | x*u < x*v | - (0<x).
- (0 < x) | x^0 = s(0).
0 < s(0).
- (0 < x) | x != 0.
0 < a.
s(0) < s(s(0)).
x < y | y <= x.
-(y<=x) | - (x < y).
- (u < v) | - (v <=w) | u < w. % transitivity, see lessthan.in
- (s(0) < z) | -(0 < y) | s(y) <= z*y. % also this it should prove for itself
z = 0 | z = s(0) | -(z < s(s(0))).
-(x <= 0) | x = 0. % zero is the least element in order
s(0) < a.
end_of_list.
list(demodulators).
x*s(y) = x*y + x.
x+0 = x.
0+x = x.
x^0 = s(0).
end_of_list.
list(sos).
- (n < a^n).
end_of_list.
