:: deftheorem defines GFA3CarryStr GFACIRC1:def 43 :
for x, y, z being set holds GFA3CarryStr (x,y,z) = (GFA3CarryIStr (x,y,z)) +* (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3));