:: deftheorem defines BitFTA1AdderOutputP FTACELL1:def 11 :
for ap, bm, cp, dm, cin being set holds BitFTA1AdderOutputP (ap,bm,cp,dm,cin) = GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm);