Online Otter-λ
-->
Examples
% test file for lambda and ap.
% Demonstrates beta reduction and renaming of bound variables to avoid capture.
set(lambda).
set(demod_inf).
set(binary_res).
list(usable).
x = x.
end_of_list.
list(demodulators).
x *x = x.
end_of_list.
list(sos).
ap(ap(lambda(x,lambda(y,x)),c*c),y) != c | % beta reduction works fine combined with ordinary demodulation
ap(lambda(x,lambda(y,x)),y) != lambda(z,y) | % y will not be captured in the beta-reduction
lambda(x,x) != lambda(z,z) | % these two differ by renaming a bound variable
lambda(z,a) != lambda(z,x) | % succeeds with x:= a
lambda(w,a) != lambda(z,x). % also succeeds with x:= a
end_of_list.
% Note: lambda(x,a) != lambda(z,x) would be illegal input, since x occurs both free and lambda-bound in the same clause.
% The bound x would have to be renamed first.