:: deftheorem defines BitFTA2CarryOutput FTACELL1:def 15 :
for am, bp, cm, dp, cin being set holds BitFTA2CarryOutput (am,bp,cm,dp,cin) = GFA2CarryOutput (am,bp,cm);