= Solution
A <sentinel node> is a permanent header whose key is ignored and whose `next` field holds the first data node. Every data node then has a predecessor, including the first, so unlinking always updates a predecessor's `next` field.
``
function DelMin(hd: List): List
require hd != nil and hd.next != nil
bestPrev := hd
p := hd.next
while p.next != nil do
if p.next.x < bestPrev.next.x then
bestPrev := p
p := p.next
result := bestPrev.next
bestPrev.next := result.next
result.next := nil
return result
``
The processed data prefix ends at `p`. Its minimum is `bestPrev.next`, and `bestPrev` remains that node's actual predecessor. This <loop invariant> is initialized by the first node and preserved when a strictly smaller next node is found. The unprocessed suffix length is a <loop variant>. At exit, the final splice removes the first minimum in one uniform case. This is <linked-list minimum extraction>; it requires at least one data node, rather than treating the dummy header as an element.
Back to article page
