:: deftheorem defines GFA2CarryCirc GFACIRC1:def 32 :
for x, y, z being set holds GFA2CarryCirc (x,y,z) = (GFA2CarryICirc (x,y,z)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2],nor3));