:: deftheorem defines BitFTA2AdderOutputP FTACELL1:def 17 :
for am, bp, cm, dp, cin being set holds BitFTA2AdderOutputP (am,bp,cm,dp,cin) = GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);