% A Problem in combinatory logic.
%
% Given combinators L and Q,
%
%   Lxy = x(yy)
%   Qxyz =  y(xz)
%
% show that there does not necessarily exist a fixed
% point combinator F, where Fx=x(Fx).

assign(iterate_up_to, 10).

% set(verbose).

clauses(theory).

a(a(L,x),y) = a(x,a(y,y)).
a(a(a(Q,x),y),z) = a(y,a(x,z)).

end_of_list.

formulas(theory).

% There does not exist a fixed-point combinator.

-(exists F all x (a(F,x) = a(x,a(F,x)))).

end_of_list.