EconCSLib.GameTheory.ExtensiveGame.Execution.Reachability

Payoff-aware reachability compatibility for the Arena extensive-game model.

The representation-neutral Arena.Reachable relation and the payoff-free ControlledGame.IsReachable specialization live in Structural.Reachability. This module adds only the historical ExtensiveGame.IsReachable projection.

Main definitions

• ExtensiveGame.IsReachable — reachability from an extensive game's initial state.

def ExtensiveGame.IsReachable {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : Prop

A state is reachable in the game if it is reachable from init.

Equations

• G.IsReachable s = G.IsReachable s

@[simp]

theorem ExtensiveGame.isReachable_iff_toControlledGame {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : G.IsReachable s ↔ G.IsReachable s

The historical payoff-aware reachability predicate is exactly the canonical controlled-game predicate.

theorem ExtensiveGame.isReachable_init {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : G.IsReachable G.init

The initial state is always reachable.

theorem ExtensiveGame.IsReachable.next {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} {s : G.State} (h : G.IsReachable s) (a : G.Action s) : G.IsReachable (G.next s a)

If s is reachable and we take action a, then next s a is reachable.