:: deftheorem defines GFA3CarryICirc GFACIRC1:def 42 :
for x, y, z being set holds GFA3CarryICirc (x,y,z) = ((1GateCircuit (x,y,nor2)) +* (1GateCircuit (y,z,nor2))) +* (1GateCircuit (z,x,nor2));