:: deftheorem defines BitGFA1CarryOutput GFACIRC1:def 27 :
for x, y, z being set holds BitGFA1CarryOutput (x,y,z) = [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3];