% problem-set/circuits/two.inverter.ver1.clauses
% created : 08/28/86
% revised : 07/14/88

% description:
%
% The two inverter puzzle given in the text, "Automated
% Reasoning" by Larry Wos et al.(page 186 - 219).
%
% To design a circuit using as many AND and OR gates as you like, but 
% using only two NOT gates. The circuit should be designed according to
% the following specification:
%
% o1 = not(i1)
% o2 = not(i2)
% o3 = not(i3)
%
% where, o1, o2, o3 are the outputs and i1, i2, i3 are the
% related inputs.  

% representation:
%
% See pages 186 - 219 in the above mentioned text. 

-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | 
OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
    and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | 
OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
    or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),
 	not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3),
 	not(x4),not(x5),not(x6),not(x7),not(x8))),
 	makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4),
 	not(x5),not(x6),not(x7),not(x8)),v))).
-TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | 
OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8),
addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),
not(x8)))).

OUTPUT(0,0,0,0,1,1,1,1,x).
OUTPUT(0,0,1,1,0,0,1,1,x).
OUTPUT(0,1,0,1,0,1,0,1,x).
-OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) |
-OUTPUT(1,0,1,0,1,0,1,0,v).

Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(or(x,0),x).
Equal(or(x,1),1).
Equal(not(0),1).
Equal(not(1),0).

% list handling

Equal(addinv(l(x,y),z),l(x,addinv(y,z))).
Equal(addinv(x,y),l(y,x)).
Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)),
	lr(possrev(R00m,x000,x001),
 	lr(possrev(R01m,x010,x011),
	lr(possrev(R10m,x100,x101),
 	lr(possrev(R11m,x110,x111),
	lr(possrev(R0m0,x000,x010),
 	lr(possrev(R0m1,x001,x011),
 	lr(possrev(R1m0,x100,x110),
 	lr(possrev(R1m1,x101,x111),
	lr(possrev(Rm00,x000,x100),
 	lr(possrev(Rm01,x001,x101),
 	lr(possrev(Rm10,x010,x110),
 	lr(possrev(Rm11,x011,x111),
 	makerevlist(v)))))))))))))).
Equal(makerevlist(v),end).
Equal(possrev(xname,1,0),xname).
Equal(possrev(xname,0,1),notrev).
Equal(possrev(xname,x,x),notrev).
Equal(lr(notrev,x),x).
Equal(lr(x,lr(y,z)),lr(y,lr(x,z))).
Equal(lr(x,lr(x,y)),lr(x,y)).