structure GeographyGame.Position (V : Type u_2) : Type u_2

A position in Generalized Geography: the current vertex (whose owner is about to move) together with the set of already-visited vertices.

• current : V
• visited : Finset V

def GeographyGame.ValidMove {V : Type u_1} (G : Digraph V) (pos : Position V) (next : V) : Prop

next is a valid move from pos in G: there is an edge from the current vertex to next, and next has not been visited.

def GeographyGame.makeMove {V : Type u_1} [DecidableEq V] (pos : Position V) (next : V) : Position V

Update a position by moving the token to next, marking it visited.

def GeographyGame.IsStuck {V : Type u_1} (G : Digraph V) (pos : Position V) : Prop

A position is stuck if no valid move exists — the player to move loses.

inductive GeographyGame.HasWinningStrategy {V : Type u_1} [DecidableEq V] (G : Digraph V) : Position V → Bool → Prop

The "has winning strategy" relation for Generalized Geography. HasWinningStrategy G pos b holds when the player whose turn it is (b = true for Player I, b = false for Player II) has a strategy to win from position pos:

• Player I (true) wins by choosing some valid move leading to a position where Player II loses.
• Player II (false) wins immediately if the position is stuck (Player I cannot move), or if every valid move by Player I leads to a Player-I-winning position.

• playerI_moves {V : Type u_1} [DecidableEq V] {G : Digraph V} {pos : Position V} {next : V} (hmove : ValidMove G pos next) (hwin : HasWinningStrategy G (makeMove pos next) false) : HasWinningStrategy G pos true
• playerII_stuck {V : Type u_1} [DecidableEq V] {G : Digraph V} {pos : Position V} (hstuck : IsStuck G pos) : HasWinningStrategy G pos false
• playerII_moves {V : Type u_1} [DecidableEq V] {G : Digraph V} {pos : Position V} (hnotStuck : ¬IsStuck G pos) (hwin : ∀ (next : V), ValidMove G pos next → HasWinningStrategy G (makeMove pos next) true) : HasWinningStrategy G pos false

def GeographyGame.initPosition {V : Type u_1} (s : V) : Position V

The initial position of the game starting at vertex s, with s already visited.

def GeographyGame.GG {V : Type u_1} [DecidableEq V] (G : Digraph V) (s : V) : Prop

Sipser, Lecture 19. The language GG = {⟨G, a⟩ | Player I has a forced win in Generalized Geography on G from a}. GG is PSPACE-complete.