:: deftheorem defines BitFTA2Circ FTACELL1:def 14 :
for am, bp, cm, dp, cin being set holds BitFTA2Circ (am,bp,cm,dp,cin) = (BitGFA2Circ (am,bp,cm)) +* (BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp));