Triedenie
budeme pouzívat premennú m, 1 ? m ? N a v kazdom bode výpoctu bude platit
(a) y[m + 1 .. N] je utriedené
? ? i, j: m < i < j ? N:: y[i] < y[j] ?
(b) všetky prvky y[1 .. m] sú menšie nez prvky y[m + 1 .. N]
? ? i, j: 1 ? i ? m < j ? N:: y[i] < y[j] ?
ked zlúcime (a) a (b) dohromady, dostaneme
? ? i, j: 1 ? i < j ? N ? m < j :: y[i] < y[j] ?
na zaciatku m = N to zarucuje
ak chceme znízit m, tak musíme permutovat y[1 .. m] tak, aby pre nejaké k, 1 < k ? m, pole y[k .. m] bolo utriedené a elementy tohoto pola y[k .. m] boli väcšie nez prvky pola y[1 .. k ? 1]; potom polozíme m := k ? 1
invariant y je permutáciou x
? ? ? i, j: 1 ? i < j ? N ? m < j :: y[i] < y[j] ? (5)
? ?k: k > 1:: m = k ? m < k ? (7)
Dôkaz správnosti: cvicenie.