theorem :: SCMFSA_X:14

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