theorem Th27: :: SCMISORT:34

for s being State of SCM+FSA
for t being FinSequence of INT
for P being Instruction-Sequence of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Insert-Sort-Algorithm c= P holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )