:: deftheorem defines GFA3CarryOutput GFACIRC1:def 45 :
for x, y, z being set holds GFA3CarryOutput (x,y,z) = [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];