 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.