Solution (source code)

= Solution

A <sentinel node> supplies a permanent predecessor for the first real node. Inserting or deleting at the front then uses the same `predecessor.next` update as an interior operation. Its datum is \b[not a <multiset> element]: the chosen extreme <integer> is merely unused sentinel data.

A <representation invariant> requires a nonnull fixed header, a finite acyclic chain starting at `bagHeader.next`, and exclusion of the header from that chain. Each node identity occurs once, although different nodes may have equal data. Representation links are owned by the implementation, so outside mutation cannot alter them unexpectedly.

The <abstraction function> counts occurrences:
$$
\mathrm{bag}(x)=\bigl|\{u\in L(\mathrm{bagHeader.next}):u.\mathrm{datum}=x\}\bigr|.
$$
This yields nonnegative multiplicities and finite support. Initialization with a null successor gives the empty <multiset>. Excluding the sentinel is essential even when a real item equals its datum.