theorem :: SCMFSA8C:69

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