:: deftheorem defines BitFTA0Circ FTACELL1:def 2 :
for ap, bp, cp, dp, cin being set holds BitFTA0Circ (ap,bp,cp,dp,cin) = (BitGFA0Circ (ap,bp,cp)) +* (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp));