theorem :: FTACELL1:40

for am, bm, cm, dm being non pair set
for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable