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