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