## Examples

Examples -> LambdaLogic -> lambda.in% 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.