Four sequential disjunctions on B → B → B. Left-or (lor) queries the first argument first and can return true without looking at the second; right-or is the symmetric sequential strategy. Parallel-or is not among them: no innocent strategy can return true when either argument is true and the other diverges.
Type B → B → B
Enabling structure of the arena (each move drawn once). Hover a move for its role. Enabling.
Left-or: query x, return tt immediately on tt, else query y.
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.
Right-or: query y first.
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.
Strict left-then-right or: always inspect both, left first.
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.
Strict right-then-left or.
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.