% 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).

% set(verbose).

formulas(assumptions).

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(goals).

% existence of a fixed point combinator

  (exists Q all x (a(Q,x) = a(x,a(Q,x)))) # label(fixed_point_combinator).

end_of_list.
