for n being Nat
for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitGFA0Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable