theorem :: SCMFSA_X:17

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