:: deftheorem defines GFA0CarryICirc GFACIRC1:def 6 :
for x, y, z being set holds GFA0CarryICirc (x,y,z) = ((1GateCircuit (x,y,and2)) +* (1GateCircuit (y,z,and2))) +* (1GateCircuit (z,x,and2));