(* Author: Carsten Schuermann *)
(* An adder for arbitrary many bits *)


(* eq x y = C 

   Invariant:
   C is a circuit that has to open ports, 
   and decides if x = y 
*)
fun eq x y = 
  ORGate (ANDGate (NOTGate x, 
		   NOTGate y), 
	  ANDGate (x, y))


(* eq4 x3 x2 x1 x0 y3 y2 y1 y0 = C 

   Invariant:
   C is a circuit that has eight open ports, 
   and decides if x3x2x1x0 = y3y2y1y0 
*)
fun eq4 x3 x2 x1 x0 y3 y2 y1 y0 = 
  ANDGate (ANDGate (eq x0 y0,
		    eq x1 y1),
	   ANDGate (eq x2 y2,
		    eq x3 y3))