Search a predicate N → B for a witness. exists-true queries 0,1,2,… until the predicate returns tt. When Opponent backtracks to an earlier query, innocence forces Proponent to replay the same Nat; there is no mutable search index.
Type (N → B) → B
Enabling structure of the arena (each move drawn once). Hover a move for its role. Enabling.
Search from 0 upward until the predicate returns tt.
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.
Search from 2 upward.
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.
Answer ff without querying the predicate.
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.