:: deftheorem defines BitGFA0Circ GFACIRC1:def 14 :
for x, y, z being set holds BitGFA0Circ (x,y,z) = (GFA0AdderCirc (x,y,z)) +* (GFA0CarryCirc (x,y,z));