theorem Th24: :: SCMFSA8C:32

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