theorem :: FSCIRC_2:26

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