structure AP.Alt₁.Point : Type

• x : ℤ
• y : ℤ

theorem AP.Alt₁.Point.ext {x y : Point} : x.x = y.x → x.y = y.y → x = y

theorem AP.Alt₁.Point.ext_iff {x y : Point} : x = y ↔ x.x = y.x ∧ x.y = y.y

instance AP.Alt₁.instNonemptyPoint : Nonempty Point

def AP.Alt₁.center : Point

Equations

• AP.Alt₁.center = { x := 0, y := 0 }

def AP.Alt₁.dist (p₁ p₂ : Point) : ℕ

Equations

• AP.Alt₁.dist p₁ p₂ = (max |p₁.x - p₂.x| |p₁.y - p₂.y|).toNat

structure AP.Alt₁.Board : Type

• squares : Set Point
• A : Point

theorem AP.Alt₁.Board.ext {x y : Board} (squares : x.squares = y.squares) (A : x.A = y.A) : x = y

theorem AP.Alt₁.Board.ext_iff {x y : Board} : x = y ↔ x.squares = y.squares ∧ x.A = y.A

def AP.Alt₁.board₀ : Board

Equations

• AP.Alt₁.board₀ = { squares := Set.univ, A := AP.Alt₁.center }

@[reducible, inline]

abbrev AP.Alt₁.AMove : Type

Equations

• AP.Alt₁.AMove = AP.Alt₁.Point

@[reducible, inline]

abbrev AP.Alt₁.DMove : Type

Equations

• AP.Alt₁.DMove = Option AP.Alt₁.Point

def AP.Alt₁.AMoveValid (pw : ℕ) (b : Board) (p : AMove) : Prop

Equations

• AP.Alt₁.AMoveValid pw b p = (p ≠ b.A ∧ AP.Alt₁.dist p b.A ≤ pw ∧ p ∈ b.squares)

def AP.Alt₁.DMoveValid (b : Board) : DMove → Prop

Equations

• AP.Alt₁.DMoveValid b none = True
• AP.Alt₁.DMoveValid b (some p) = (p ≠ b.A ∧ p ∈ b.squares)

structure AP.Alt₁.ValidAMove (pw : ℕ) (b : Board) : Type

• m : AMove
• h : AMoveValid pw b self.m

structure AP.Alt₁.ValidDMove (b : Board) : Type

• m : DMove
• h : DMoveValid b self.m

def AP.Alt₁.AHasValidMove (pw : ℕ) (b : Board) : Prop

Equations

• AP.Alt₁.AHasValidMove pw b = ∃ (m : AP.Alt₁.AMove), AP.Alt₁.AMoveValid pw b m

structure AP.Alt₁.State : Type

• board : Board
• history : List Board
• act : Prop

theorem AP.Alt₁.State.ext {x y : State} (board : x.board = y.board) (history : x.history = y.history) (act : x.act = y.act) : x = y

theorem AP.Alt₁.State.ext_iff {x y : State} : x = y ↔ x.board = y.board ∧ x.history = y.history ∧ x.act = y.act

def AP.Alt₁.initState (b : Board) : State

Equations

• AP.Alt₁.initState b = { board := b, history := [], act := True }

def AP.Alt₁.state₀ : State

Equations

• AP.Alt₁.state₀ = AP.Alt₁.initState AP.Alt₁.board₀

def AP.Alt₁.State.finish (s : State) : State

Equations

• s.finish = { board := s.board, history := s.history, act := False }

structure AP.Alt₁.A (pw : ℕ) : Type

• f (s : State) : s.act → AHasValidMove pw s.board → ValidAMove pw s.board

structure AP.Alt₁.D : Type

• f (s : State) : s.act → ValidDMove s.board

def AP.Alt₁.applyMove (s : State) (b : Board) : State

Equations

• AP.Alt₁.applyMove s b = { board := b, history := s.history ++ [s.board], act := s.act }

def AP.Alt₁.applyAMoveB (b : Board) (m : AMove) : Board

Equations

• AP.Alt₁.applyAMoveB b m = { squares := b.squares, A := m }

def AP.Alt₁.applyDMoveB (b : Board) : DMove → Board

Equations

• AP.Alt₁.applyDMoveB b none = b
• AP.Alt₁.applyDMoveB b (some p) = { squares := b.squares \ {p}, A := b.A }

def AP.Alt₁.applyAMove (s : State) (m : AMove) : State

Equations

• AP.Alt₁.applyAMove s m = AP.Alt₁.applyMove s (AP.Alt₁.applyAMoveB s.board m)

def AP.Alt₁.applyDMove (s : State) (m : DMove) : State

Equations

• AP.Alt₁.applyDMove s m = AP.Alt₁.applyMove s (AP.Alt₁.applyDMoveB s.board m)

structure AP.Alt₁.Game (pw : ℕ) : Type

• a : A pw
• d : D
• s : State

theorem AP.Alt₁.Game.ext_iff {pw : ℕ} {x y : Game pw} : x = y ↔ x.a = y.a ∧ x.d = y.d ∧ x.s = y.s

theorem AP.Alt₁.Game.ext {pw : ℕ} {x y : Game pw} (a : x.a = y.a) (d : x.d = y.d) (s : x.s = y.s) : x = y

def AP.Alt₁.initGame {pw : ℕ} (a : A pw) (d : D) (s : State) : Game pw

Equations

• AP.Alt₁.initGame a d s = { a := a, d := d, s := s }

def AP.Alt₁.Game.act {pw : ℕ} (g : Game pw) : Prop

Equations

• g.act = g.s.act

def AP.Alt₁.Game.setState {pw : ℕ} (g : Game pw) (s₁ : State) : Game pw

Equations

• g.setState s₁ = { a := g.a, d := g.d, s := s₁ }

def AP.Alt₁.Game.finish {pw : ℕ} (g : Game pw) : Game pw

Equations

• g.finish = g.setState g.s.finish

def AP.Alt₁.playAMoveAt' {pw pw₁ : ℕ} (a₁ : A pw₁) (g : Game pw) (hs : g.s.act) (h : AHasValidMove pw₁ g.s.board) : Game pw

Equations

• AP.Alt₁.playAMoveAt' a₁ g hs h = g.setState (AP.Alt₁.applyAMove g.s (a₁.f g.s hs h).m)

noncomputable def AP.Alt₁.playAMoveAt {pw : ℕ} (g : Game pw) : Game pw

Equations

• AP.Alt₁.playAMoveAt g = if h : g.act ∧ AP.Alt₁.AHasValidMove pw g.s.board then AP.Alt₁.playAMoveAt' g.a g ⋯ ⋯ else g.finish

def AP.Alt₁.playDMoveAt {pw : ℕ} (g : Game pw) (hs : g.s.act) : Game pw

Equations

• AP.Alt₁.playDMoveAt g hs = g.setState (AP.Alt₁.applyDMove g.s (g.d.f g.s hs).m)

noncomputable def AP.Alt₁.Game.playMove {pw : ℕ} (g : Game pw) : Game pw

Equations

• g.playMove = if hs : g.act then AP.Alt₁.playAMoveAt (AP.Alt₁.playDMoveAt g hs) else g

noncomputable def AP.Alt₁.Game.play {pw : ℕ} (g : Game pw) (n : ℕ) : Game pw

Equations

• g.play n = AP.Alt₁.Game.playMove^[n] g

def AP.Alt₁.Game.AWins {pw : ℕ} (g : Game pw) : Prop

Equations

• g.AWins = ∀ (n : ℕ), (g.play n).act

def AP.Alt₁.Game.DWins {pw : ℕ} (g : Game pw) : Prop

Equations

• g.DWins = ∃ (n : ℕ), ¬(g.play n).act

def AP.Alt₁.AHwsAt (pw : ℕ) (s : State) : Prop

Equations

• AP.Alt₁.AHwsAt pw s = ∃ (a : AP.Alt₁.A pw), ∀ (d : AP.Alt₁.D), (AP.Alt₁.initGame a d s).AWins

def AP.Alt₁.DHwsAt (pw : ℕ) (s : State) : Prop

Equations

• AP.Alt₁.DHwsAt pw s = ∃ (d : AP.Alt₁.D), ∀ (a : AP.Alt₁.A pw), (AP.Alt₁.initGame a d s).DWins

def AP.Alt₁.AHws (pw : ℕ) : Prop

Equations

• AP.Alt₁.AHws pw = AP.Alt₁.AHwsAt pw AP.Alt₁.state₀

def AP.Alt₁.DHws (pw : ℕ) : Prop

Equations

• AP.Alt₁.DHws pw = AP.Alt₁.DHwsAt pw AP.Alt₁.state₀