:: deftheorem defines GFA1CarryCirc GFACIRC1:def 20 :
for x, y, z being set holds GFA1CarryCirc (x,y,z) = (GFA1CarryICirc (x,y,z)) +* (1GateCircuit ([<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2],or3));