:: deftheorem defines BitGFA3Circ GFACIRC1:def 50 :
for x, y, z being set holds BitGFA3Circ (x,y,z) = (GFA3AdderCirc (x,y,z)) +* (GFA3CarryCirc (x,y,z));