:: deftheorem defines BitFTA0AdderOutputP FTACELL1:def 5 :
for ap, bp, cp, dp, cin being set holds BitFTA0AdderOutputP (ap,bp,cp,dp,cin) = GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp);