theorem :: SCM_HALT:76

for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ) holds
while>0 (a,I) is InitHalting by Lm9;