theorem Th8: :: SCMFSA_X:8

for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
(card I) + k in dom (while>0 (a,I))