% problem-set/algebra/boolean/prob4_part2.ver2
% created: 08/08/89
% revised: 08/08/89

% description:
%
% This problem is designed to prove that x + (x * y) = x in boolean
% algebra.  

% This version uses equality representation and demodulators.
% Paramodulation is the inference rule.

% representation:
%
% prod(a,b) = c  means a * b = c.
% sum(a,b) = c  means a + b = c.
%
% declare_functions(2,[sum, prod]).
% declare_function(1,comp).
% declare_variables([x,y,z,u,v,v1,v2,v3,v4]).
% declare_constants([0,1,a,b]).

% reflexivity
(x = x).

% commutativity
(sum(x,y) = sum(y,x)).
(prod(x,y) = prod(y,x)).

% distributivity
(sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))).
(sum(x, prod(y,z)) = prod(sum(x,y), sum(x,z))).
(prod(sum(x,y), z) = sum(prod(x,z), prod(y,z))).
(prod(x, sum(y,z)) = sum(prod(x,y), prod(x,z))).

% existence of complements
(sum(x, comp(x)) = 1).
(sum(comp(x), x) = 1).
(prod(x, comp(x)) = 0).
(prod(comp(x), x) = 0).

% existence of identities
(sum(x,0) = x).
(sum(0,x) = x).
(prod(x,1) = x).
(prod(1,x) = x).

% denial of the theorem 

-(sum(a,prod(a,b)) = a).

% commutativity
(sum(x,y) = sum(y,x)).
(prod(x,y) = prod(y,x)).

% distributivity
(sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))).
(sum(z, prod(x,y)) = prod(sum(z,x), sum(z,y))).

% existence of complements
(sum(x, comp(x)) = 1).
(sum(comp(x), x) = 1).
(prod(x, comp(x)) = 0).
(prod(comp(x), x) = 0).

% existence of identities
(sum(x,0) = x).
(sum(0,x) = x).
(prod(x,1) = x).
(prod(1,x) = x).