theorem Th2: :: SCMFSA_X:2

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