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