dnl We want to set up two ways of adding 4-bit numbers
dnl and prove that they are equivalent.
dnl
dnl adder(S,Co,Ci,A,B) means
dnl S and Co are the sum and carry outputs of an adder with inputs A,B,Ci.
define(adder1,`a(e($2,o(a($3,$4),o(a($3,$5),a($4,$5)))),
                 e($1,e(e($3,n($4)),n($5))))')dnl
define(adder2,`a(e($2,o(a(n($3),a($4,$5)),a($3,o($4,$5)))),
                 e($1,o(a($3,a($4,$5)),o(a($3,a(n($4),n($5))),
	 	      o(a(n($3),a($4,n($5))),a(n($3),a(n($4),$5)))))))')dnl
define(x1,t,   x2,f,   x3,f,   x4,t,
       y1,v5,  y2,v6,  y3,v7,  y4,v8,
       s1,v9,  s2,v10, s3,v11, s4,v12,
       c1,v13, c2,v14, c3,v15, c4,v16, c0,f,
       d1,v17, d2,v18, d3,v19, d4,v20, d0,c0)dnl
define(sum1, `a(adder1(s1,c1,c0,x1,y1),
              a(adder1(s2,c2,c1,x2,y2),
              a(adder1(s3,c3,c2,x3,y3),
                adder1(s4,c4,c3,x4,y4))))')dnl
define(sum2, `a(adder2(s1,d1,d0,x1,y1),
              a(adder2(s2,d2,d1,x2,y2),
              a(adder2(s3,d3,d2,x3,y3),
                adder2(s4,d4,d3,x4,y4))))')dnl
a(sum1,a(sum2,e(c4,d4)))