theorem :: SCPQSORT:15

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for p0, n being Nat st p0 >= 7 holds
ex f, g being FinSequence of INT st
( len f = n & f is_FinSequence_on s,p0 & len g = n & g is_FinSequence_on IExec ((QuickSort (n,p0)),P,s),p0 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by Lm28;