class Ruleset (R : Type u) : Type (max u (u_1 + 1))

• toGameForm : R → GameForm
• moves_toGameForm (p : Player) (r : R) (g' : GameForm) : g' ∈ Moves.moves p (toGameForm r) → ∃ (r' : R), toGameForm r' = g'

def Ruleset.Forms (R : Type u) [Ruleset R] (g : GameForm) : Prop

Set of GameForms created by the positions in ruleset R.

Equations

• Ruleset.Forms R g = ∃ (r : R), g = Ruleset.toGameForm r

theorem Ruleset.Forms.exists {R : Type u} [Ruleset R] {g : GameForm} (h_g : Forms R g) : ∃ (r : R), g = toGameForm r

theorem Ruleset.Forms.position_mem {R : Type u} [Ruleset R] (r : R) : Forms R (toGameForm r)

instance instHereditaryGameFormForms {R : Type u} [Ruleset R] : Form.Hereditary (Ruleset.Forms R)