# Online Otter-λ

-->

## Examples

Examples -> ExternalSimplification -> sumofnsquared.in

% prove the formula sum(k,k^2,0,n) = n(n+1)(2n+1)/6 by induction, using external simplification
% for the induction step, and lambda-unification to find the instance of induction.

set(simplify).
set(binary_res).
set(hyper_res).
set(lambda).
set(induction).
set(para_into).
set(para_all).
%set(very_verbose).

op(450, xfy, +).
op(350, fy, ~).
op(400, xfy, *).
op(300, xfx, ^).

assign(max_weight,50).
assign(max_distinct_vars,3).
weight_list(pick_and_purge).
weight(g(\$(0)),1). %every g-term counts like a constant
weight(junk,50).
end_of_list.

list(demodulators).
x/y = junk. % These two lines ensure that all the functors returned from simplify will lead from arguments in N to results in N.
-(x) = junk.
x+0 = x.
sum(u,v,x,x) = Ap(lambda(u,v),x).
sum(u,v,x,1+y) = sum(u,v,x,y) + Ap(lambda(u,v),1+y).
sum(u,v,x,y+1) = sum(u,v,x,y) + Ap(lambda(u,v),1+y).
sum(u,v,x,x) = Ap(lambda(u,v),x).
%x* (y+z) = x*y + x*z.
%(x+y)* z = x*z + y*z.
end_of_list.

list(usable).
x = x.
x + 1 != 0.
x + 1 != y + 1 | x = y.
-ap(y,0) | ap(y,g(y)) | ap(y,z).
-ap(y,0) | -ap(y,g(y)+1) | ap(y,z).
sum(u,v,x,1+y) = sum(u,v,x,y) + Ap(lambda(u,v),1+y).
end_of_list.

list(sos).
6*sum(x,x^2,0,n) != n* (n+1)* (2*n+1).
end_of_list.