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