theorem :: SCMFSA_X:11

for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 4) = halt SCM+FSA