theorem :: SCMFSA9A:57

for I being good really-closed parahalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
Initialize ((intloc 0) .--> 1) is Times (a,I) -halted