theorem :: FTACELL2:11

for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA0Circ (ap,bp,cp,dp)) holds Following (s,4) is stable