:: deftheorem defines BitGFA2Str GFACIRC1:def 37 :
for x, y, z being set holds BitGFA2Str (x,y,z) = (GFA2AdderStr (x,y,z)) +* (GFA2CarryStr (x,y,z));