:: deftheorem defines GFA1CarryIStr GFACIRC1:def 17 :
for x, y, z being set holds GFA1CarryIStr (x,y,z) = ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) +* (1GateCircStr (<*z,x*>,and2));