:: deftheorem defines BitGFA1Circ GFACIRC1:def 26 :
for x, y, z being set holds BitGFA1Circ (x,y,z) = (GFA1AdderCirc (x,y,z)) +* (GFA1CarryCirc (x,y,z));