theorem :: SCMFSA8B:12

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