theorem Th4: :: SCMFSA_X:4

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