:: deftheorem defines BitFTA3AdderOutputP FTACELL1:def 23 :
for am, bm, cm, dm, cin being set holds BitFTA3AdderOutputP (am,bm,cm,dm,cin) = GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm);