:: deftheorem defines BitGFA3Str GFACIRC1:def 49 :
for x, y, z being set holds BitGFA3Str (x,y,z) = (GFA3AdderStr (x,y,z)) +* (GFA3CarryStr (x,y,z));