theorem Th27: :: SCMFSA8C:35

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