let p0, n be Element of NAT ; :: thesis: ( p0 >= 7 implies QuickSort n,p0 is parahalting )
assume p0 >= 7 ; :: thesis: QuickSort n,p0 is parahalting
then for s being State of SCMPDS holds QuickSort n,p0 is_halting_on s by Lm29;
hence QuickSort n,p0 is parahalting by SCMPDS_6:35; :: thesis: verum