Examples -> LambdaLogic -> lambda.in
% test file for lambda and ap.
% Demonstrates beta reduction and renaming of bound variables to avoid capture.
x = x.
x *x = x.
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
% 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.