:: deftheorem defines GFA1CarryICirc GFACIRC1:def 18 :
for x, y, z being set holds GFA1CarryICirc (x,y,z) = ((1GateCircuit (x,y,and2c)) +* (1GateCircuit (y,z,and2a))) +* (1GateCircuit (z,x,and2));