theorem :: SCM_HALT:54

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting keepInt0_1 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