let p0, n be Nat; :: thesis: ( p0 >= 7 implies QuickSort (n,p0) is parahalting )
assume A1: p0 >= 7 ; :: thesis: QuickSort (n,p0) is parahalting
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds QuickSort (n,p0) is_halting_on s,P

proof

let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS holds QuickSort (n,p0) is_halting_on s,P
let P be Instruction-Sequence of SCMPDS; :: thesis: QuickSort (n,p0) is_halting_on s,P
QuickSort (n,p0) is_halting_on Initialize s,P by A1, Lm28;
hence QuickSort (n,p0) is_halting_on s,P by SCMPDS_6:126; :: thesis: verum

end;

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