theorem :: SCMFSA_X:35

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;