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