Triedenie ? Sekvencné architektúry
Dôkaz. Musíme ukázat, ze P3 splna (5), (6), (7). Z textu programu zrejme platia (5), (8), (9).
Dôkaz (7): ? ?k: k > 1:: m = k ? m < k ?
m = k ? k > 1 ? top[1] ? m < k (12)
Potom m = k ? (m = k ? top[1]) ? m < k z PSP aplikované na (10), (11) a z predchádzajúceho a (12) máme
(11) a (12) platia priamo z P3, ostáva dokázat (10).
Dôkaz (10): true ? top[1]
d = ? +i: top[i]:: pocet vrcholov v podstrome s korenom i ?
Vykonaním príkazu, ktorý polozí top[i] := true pre nejaké i sa zvýši hodnota d (lebo podstrom s korenom jeho synom je menší)
d = D ensures top[1] ? d > D
avšak hodnota d je ohranicená, teda
m > 1 ? m ? 1 /* zo (7) */
Ak p ? q, vieme, ze platí FP ? (p ? q), teda ak p ? ?p, vieme, ze FP ? ?p. Nech p ? m > 1, potom FP ? m ? 1. Z textu programu vieme, ze m ? 1 ? FP.