theorem Th16: :: SCPISORT:16

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for k0, k being Nat st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being Nat st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )