theorem :: FTACELL1:30

for am, bp, cm, dp being non pair set
for cin being set st cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] holds
for s being State of (BitFTA2Circ (am,bp,cm,dp,cin)) holds Following (s,4) is stable