Problem, calculus, and result. Implement the book-owned queue fixture using the possibility-set and lifted update definitions of chapter 88. The program must retain both enqueue orders, prune to [2] after return 1, reject the forced singleton [2,1], retain a singleton exchanger fixture, and check successor nonemptiness and stability.
Representation and invariant. Use four closed queue states for [1,2], [2,1], [2], and [1]; represent a possibility set by a finite list. The invariant is that every retained state has the concrete overlay projection and a target transition for the observed return. A function-valued predicate matches the Rocq artifact more closely, but a finite list exposes emptiness and the exact retained witnesses to the acceptance test.
First complete version. Implement the target dequeue relation. It maps [1,2] under return 1 to [2], maps [2,1] under return 2 to [1], and rejects the crossed labels. Filter the initial two-state list with that partial transition and print the successor list.
Remaining cases in proof order. First check that the successor is inhabited. Then run the same update from the forced singleton [2,1] and require an empty result. Add a one-element exchanger witness to record that multiple possibilities are not always needed. Finally rerun the queue update to check the fixed stability fixture.
A failing version. Retain [2,1] after observing return 1. The resulting list {[2],[2,1]} contains a state with no compatible target transition and therefore differs from the named singleton oracle. The mutation check must detect it.
Acceptance test. Require the two exact queue traces, the no-compatible-possibility line, the exchanger and stability PASS lines, the mutation verdict, the final six-case summary, and audit output [].
Mathematical boundary. The explorer illustrates proposition 88.4 and the nonemptiness side condition. It does not prove LHL soundness, semantic completeness, linearizability of the exchanger, or any theorem in the native Rocq artifact.