theorem :: SCMISORT:18

for I being InitHalting good really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),INT st
for s, t being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) holds
while>0 (a,I) is InitHalting