:: deftheorem defines BitGFA0Str GFACIRC1:def 13 :
for x, y, z being set holds BitGFA0Str (x,y,z) = (GFA0AdderStr (x,y,z)) +* (GFA0CarryStr (x,y,z));