:: deftheorem defines BitGFA1Str GFACIRC1:def 25 :
for x, y, z being set holds BitGFA1Str (x,y,z) = (GFA1AdderStr (x,y,z)) +* (GFA1CarryStr (x,y,z));