theorem :: SCMFSA_X:22

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