theorem Th11: :: SCMISORT:17

for I being InitHalting good really-closed 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 holds
( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) holds
while>0 (a,I) is InitHalting