def AP.King.state₀ : State

Equations

• AP.King.state₀ = AP.initState 1 0

def AP.King.dKingOp₂ : DStrat

Equations

• AP.King.dKingOp₂ = AP.DStrat.mk fun (s : AP.State) => (do let p ← AP.Box.interior.toList guard (p ≠ s.aPos ∧ p ∉ s.taken) pure p).head?

noncomputable def AP.King.dKingOp₂NC : DStrat

Equations

• AP.King.dKingOp₂NC = AP.DStrat.mk fun (s : AP.State) => (do let p ← AP.Box.interiorNC.toList guard (p ≠ s.aPos ∧ p ∉ s.taken) pure p).head?

def AP.King.dKingOp₁ : DStrat

Equations

• AP.King.dKingOp₁ = AP.Box.defense.st AP.King.dKingOp₂

def AP.King.dKingOp : DStrat

Equations

• AP.King.dKingOp = { f := fun (s : AP.State) => match ((AP.Box.guardTiles \ s.taken).erase s.aPos).toList.head? with | none => AP.King.dKingOp₁.f s | some p => p }

theorem AP.AState.aPos_dist_le_of_tr {s s' : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s') : Point.dist s'.aPos s.aPos ≤ ↑s.pw

theorem AP.State.aPos_dist_le_of_simulate_two {s : State} {r : State × ℕ} {f : State → PointZ} [hs : sys.WF s] (h : sys.simulate f s 2 = r) : Point.dist r.1.aPos s.aPos ≤ ↑s.pw

theorem AP.State.aPos_dist_le_of_simulate_mul_two {s : State} {r : State × ℕ} {f : State → PointZ} {n : ℕ} [hs : sys.WF s] (h : sys.simulate f s (n * 2) = r) : Point.dist r.1.aPos s.aPos ≤ ↑s.pw * ↑n

theorem AP.DState.aPos_dist_le_div_two_of_simulate {s : State} {f : State → PointZ} {n : ℕ} {r : State × ℕ} [hs : DState s] (h : sys.simulate f s n = r) : Point.dist r.1.aPos s.aPos ≤ ↑s.pw * (↑n / 2)

theorem AP.AState.of_simulate_mul_two_add_one_eq_full {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : DState s] (h : sys.simulate f s (n * 2 + 1) = (s₁, 0)) : AState s₁

theorem AP.DState.of_simulate_mul_two_add_one_eq_full {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : AState s] (h : sys.simulate f s (n * 2 + 1) = (s₁, 0)) : DState s₁

theorem AP.State.aTurn_eq_of_simulate_mul_two_eq_full {s s' : State} {f : State → PointZ} {n : ℕ} [hs : sys.WF s] (h : sys.simulate f s (n * 2) = (s', 0)) : s'.aTurn = s.aTurn

theorem AP.State.size_taken_eq_of_simulate_mul_two_eq_full {s s' : State} {f : State → PointZ} {n : ℕ} [hs : sys.WF s] (h : sys.simulate f s (n * 2) = (s', 0)) : s'.taken.size = s.taken.size + n

theorem AP.AState.size_taken_eq_of_tr {s s' : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s') : s'.taken.size = s.taken.size

theorem AP.DState.size_taken_eq_of_tr {s s' : State} {p : PointZ} [hs : DState s] (h : sys.tr s p = some s') : s'.taken.size = s.taken.size + 1

theorem AP.State.pw_eq_of_simulate_eq {s : State} {f : State → PointZ} {n : ℕ} {r : State × ℕ} [hs : sys.WF s] (h : sys.simulate f s n = r) : r.1.pw = s.pw

theorem AP.DState.size_taken_diff_eq_of_simulate_full_mul_two {s s' : State} {n : ℕ} {st : Strat} [hs : DState s] (h : sys.simulate st.f s (n * 2) = (s', 0)) : (s'.taken \ s.taken).size = n

theorem AP.DState.exi_d_move_not_mem_of_aWins {s : State} {st : Strat} (set : Set' PointZ) [hs : DState s] (h : s.aWins st) : ∃ (n : ℕ) (s' : State), DState s' ∧ sys.simulate st.f s n = (s', 0) ∧ st.d.f s' ∉ set

theorem AP.AState.exi_d_move_not_mem_of_aWins {s : State} {st : Strat} (set : Set' PointZ) [hs : AState s] (h : s.aWins st) : ∃ (n : ℕ) (s' : State), DState s' ∧ sys.simulate st.f s n = (s', 0) ∧ st.d.f s' ∉ set

theorem AP.State.exi_d_move_not_mem_of_aWins {s : State} {st : Strat} (set : Set' PointZ) [hs : sys.WF s] (h : s.aWins st) : ∃ (n : ℕ) (s' : State), DState s' ∧ sys.simulate st.f s n = (s', 0) ∧ st.d.f s' ∉ set

@[simp]

instance AP.King.instWFDKingOp₂ : dKingOp₂.WF

@[simp]

instance AP.King.instWFDKingOp₁ : dKingOp₁.WF

@[simp]

instance AP.King.instWFDKingOp : dKingOp.WF

@[simp]

instance AP.King.instDStateState₀ : DState state₀

@[simp]

theorem AP.King.pw_state₀ : state₀.pw = 1

@[simp]

theorem AP.King.aPos_state₀ : state₀.aPos = 0

@[simp]

theorem AP.King.taken_state₀ : state₀.taken = ∅

theorem AP.King.dKingOp₂_eq_dKingOp₂NC : dKingOp₂ = dKingOp₂NC

theorem AP.King.dWins_dKingOp₁_of_cnd {s : State} {a : AStrat} [hs : DState s] [ha : a.WF] (h : Box.defense.cnd s) : s.dWins { a := a, d := dKingOp₁ }

theorem AP.King.dWins_dKingOp_of_cnd {s : State} {a : AStrat} [hs : DState s] [ha : a.WF] (h : Box.defense.cnd s) : s.dWins { a := a, d := dKingOp }

theorem AP.King.dWins_dKingOp {a : AStrat} [ha : a.WF] : state₀.dWins { a := a, d := dKingOp }

theorem AP.dHwsPw_one : dHwsPw 1

theorem AP.not_aHwsPw_one : ¬aHwsPw 1