# Online Otter-λ

-->

## Examples

Examples -> ExternalSimplification -> bernoulli.in

% Bernoulli's inequality. 1 + nx <= (1+x)^n
% here n is a natural number and x is real.
% so the typings are as follows:
% type(R, ^(R,N)).
% type(R, +(R,R)) (We never need to add exponents)
% type(R, *(R,R)) (We never need to multiply exponents)
% type(o,N)
% type(1,R)
% type(0,R)
% type(R,i(N)) (i injects N into R)
% type(N, s(N))

set(simplify_rule).
set(binary_res).
set(hyper_res).
set(lambda).
set(induction).
set(para_into).
set(para_all).
assign(pick_given_ratio,4).
%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, ^).

assign(max_weight,36).
assign(max_distinct_vars,0).
weight_list(pick_and_purge).
weight(g(\$(0)),1). %every g-term counts like a constant
weight(i(\$(1)),0). % don't count 'i' as a symbol, it's just an injection of N into R
weight(junk,50).
end_of_list.

list(usable).
x = x.
x <=x.
x + 1 != 0.
-(x<x).
-(0<x) | x^o = 1.
x + 1 != y + 1 | x = y.
-ap(y,o) | ap(y,g(y)) | ap(y,z). %induction
-ap(y,o) | -ap(y,s(g(y))) | ap(y,z).
x <= y | y < x.
- (x<y) | - (z <= x) | z < y. % transitivity
x < y | x = y | y < x.
-(x<= y) | -(y <x) .
0 < a+1.
-(x <= y) | - (0 < z) | z*x <= z*y.
-(x <= y) | - (0 < z) | x*z <= y*z.
-(x <= y) | - (0 < z) | x*z <= z*y.
-(x <= y) | - (0 < z) | z*x <= y*z.
0 <= x^2.
- (x<y) | x + (- (y)) < 0.
(x <= y) | y < x.
(x < y) | y <= x.
x^o = 1 | x = 0.
0 <= i(x). % i embeds N into R
end_of_list.

list(demodulators).
x/y = junk. % Division is irrelevant in this problem.
i(o) = 0.
i(s(x)) = i(x)+1.
x^s(y)= x*x^y.
x*0 = 0.
x+0=x.
0+x = x.
0*x = 0.
% The following demodulators are used only on terms created by Simplify, and converts them to correctly typed terms.
% The second two are never actually used but are theoretically necessary to keep + out of the exponent.
x^ (y+1) = x*x^y.
x^ (y+z) = (x^y) * (x^z).
x^1 = x.
end_of_list.

list(sos).
-( 1 + i(n)*a <= (1+a)^n ).
end_of_list.