:: deftheorem defines BitFTA2Str FTACELL1:def 13 :
for am, bp, cm, dp, cin being set holds BitFTA2Str (am,bp,cm,dp,cin) = (BitGFA2Str (am,bp,cm)) +* (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp));