:: deftheorem defines BitFTA1Str FTACELL1:def 7 :
for ap, bm, cp, dm, cin being set holds BitFTA1Str (ap,bm,cp,dm,cin) = (BitGFA1Str (ap,bm,cp)) +* (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm));