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