:: deftheorem defines BitFTA1AdderOutputQ FTACELL1:def 12 :
for ap, bm, cp, dm, cin being set holds BitFTA1AdderOutputQ (ap,bm,cp,dm,cin) = GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm);