theorem :: FTACELL1:20

for ap, bm, cp, dm being non pair set
for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] holds
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin)) holds Following (s,4) is stable