:: deftheorem defines BitGFA2Circ GFACIRC1:def 38 :
for x, y, z being set holds BitGFA2Circ (x,y,z) = (GFA2AdderCirc (x,y,z)) +* (GFA2CarryCirc (x,y,z));