theorem :: SCMFSA_X:36

for I being MacroInstruction of SCM+FSA
for a being Int-Location holds if>0 (a,(I ';' (goto 0))) = ((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA) by COMPOS_1:29;