theorem :: FTACELL2:21

for n being Nat
for ap, bm, cp, dm being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA1Circ (ap,bm,cp,dm)) holds Following (s,4) is stable