:: deftheorem defines BitFTA0Str FTACELL1:def 1 :
for ap, bp, cp, dp, cin being set holds BitFTA0Str (ap,bp,cp,dp,cin) = (BitGFA0Str (ap,bp,cp)) +* (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp));