:: deftheorem defines BitFTA3Circ FTACELL1:def 20 :
for am, bm, cm, dm, cin being set holds BitFTA3Circ (am,bm,cm,dm,cin) = (BitGFA3Circ (am,bm,cm)) +* (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm));