let p0, n be Element of NAT ; :: thesis: ( p0 >= 7 implies QuickSort (n,p0) is parahalting )
assume Z: p0 >= 7 ; :: thesis: QuickSort (n,p0) is parahalting
for s being State of SCMPDS holds QuickSort (n,p0) is_halting_on s

proof

let s be State of SCMPDS; :: thesis: QuickSort (n,p0) is_halting_on s
QuickSort (n,p0) is_halting_on Initialize s by Z, Lm29;
hence QuickSort (n,p0) is_halting_on s by SCMPDS_6:140; :: thesis: verum

end;

hence QuickSort (n,p0) is parahalting by SCMPDS_6:35; :: thesis: verum