Online Otter-λ

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

Examplessmall logo



Examples -> ExternalSimplification -> sumofn.in


% prove the formula sum(k,k,0,n) = n(n+1)/2 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,40).
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). % the bound variable is the first argument, in Otter-lambda
sum(u,v,x,y+1) = sum(u,v,x,y) + Ap(lambda(u,v),1+y).
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).
%x+y = z | y != z-x. // if you put this in, you can drop set(para_into).
end_of_list.

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