:: deftheorem Def5 defines RWNotIn-seq SCMFSA_M:def 5 :
for L being finite Subset of Int-Locations
for b₂ being sequence of (bool NAT) holds
( b₂ = RWNotIn-seq L iff ( b₂ . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st b₂ . i = sn holds
b₂ . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b₂ . i is infinite ) ) );