% problem-set/puzzles/birds/bird5.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 5,
% 'An Exercise in Composition'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Hypothesis: For all birds x, y, and z, there exists a bird u such 
% that for all w, uw = x(y(zw)).
% Finding clause (using xy to replace response(x,y) for compactness):
%   - (FAx FAy FAz TEu FAw (uw = x(y(zw)))).
%   TEx TEy TEz FAu TEw -(uw = x(y(zw))).
%   Letting w = f(u), x = A, y = B, and z = C,
%   -[(u)f(u) = A(B((C)f(u)))].
% Denial clause:

-EQUAL(response(u,f(u)),response(A,response(B,response(C,f(u))))) |
   $ans(u).