Triedenie ? Sekvencné architektúry
strom: y[i] má synov y[2i] a y[2i + 1] (a opacne byt_synom)
potomok: nereflexívny tranzitívny uzáver relácie byt_synom
zavedieme pole top[1 .. N] of boolean,
top[i] ? y[i] je väcšie ako y[j],
kde j je potomok i a 1 ? j ? m
formálne:
invariant
? ? i, j: 1 ? i ? m ? j ? m ? j je potomok i ? top[i] ::
y[i] > y[j] ? (8)
top[1] ? y[1] = ? max j: 1 ? j ? m:: y[j] ?.
Budeme pouzívat nasledujúci
invariant
? ? i: < i ? N :: top[i] ? (9)
teda top[i] platí pre všetky listy a usporiadanú cast y.
Predpokladajme, ze N je nepárne.
Myšlienka: ak top[2i] a top[2i + 1] platia, tak top[i] bude platit, ak y[i] := max(y[i], y[2i], y[2i + 1]).
Nech ?[i] oznacuje index toho syna i, ktorý je väcší, ak i nemá syna, potom ?[i] = 2i