:: deftheorem defines BitFTA2AdderOutputQ FTACELL1:def 18 :
for am, bp, cm, dp, cin being set holds BitFTA2AdderOutputQ (am,bp,cm,dp,cin) = GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);