Proponent is a term of type ((B → B) → B) → B: it receives an oracle f and queries it by supplying an argument strategy (identity, negation, or constant true). Each interrogation of that argument is a separate P-view; innocence forbids a hidden call counter.
Type ((B → B) → B) → B
Enabling structure of the arena (each move drawn once). Hover a move for its role. Enabling.
Query the oracle with the identity function and copy its answer.
Trace against auto. (stuck — Ω)
P-view
Unfolding against every legal Opponent continuation, up to the page bound. O branches fan out; P is a single reply. Click a reply count to expand folded Opponent options.
Query the oracle with negation.
Trace against auto. (stuck — Ω)
P-view
Unfolding against every legal Opponent continuation, up to the page bound. O branches fan out; P is a single reply. Click a reply count to expand folded Opponent options.
Query the oracle with the constant-true thunk.
Trace against auto. (truncated by bound)
P-view
Unfolding against every legal Opponent continuation, up to the page bound. O branches fan out; P is a single reply. Click a reply count to expand folded Opponent options.
The empty strategy Ω: Proponent never moves.
Trace against auto. (stuck — Ω)
P-view
Unfolding against every legal Opponent continuation, up to the page bound. O branches fan out; P is a single reply. Click a reply count to expand folded Opponent options.