theorem :: SCMFSA8C:91

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good really-closed parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1