:: deftheorem defines GFA2CarryICirc GFACIRC1:def 30 :
for x, y, z being set holds GFA2CarryICirc (x,y,z) = ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,z,and2c))) +* (1GateCircuit (z,x,nor2));