theorem AP.State.forall_dWins_bounded_of_forall_dWins {s : State} [hs : sys.WF s] {d : DStrat} [Hd : d.WF] (h : ∀ (a : AStrat), a.WF → s.dWins { a := a, d := d }) : ∃ (n : ℕ), ∀ (a : AStrat), a.WF → (sys.simulate { a := a, d := d }.f s n).2 ≠ 0

theorem AP.State.forall_dWins_iff_forall_dWins_bounded {s : State} [hs : sys.WF s] {d : DStrat} [Hd : d.WF] : (∀ (a : AStrat), a.WF → s.dWins { a := a, d := d }) ↔ ∃ (n : ℕ), ∀ (a : AStrat), a.WF → (sys.simulate { a := a, d := d }.f s n).2 ≠ 0

theorem AP.State.dHws_bounded_of_dHws {s : State} [hs : sys.WF s] (h : s.dHws) : ∃ (n : ℕ) (d : DStrat), d.WF ∧ ∀ (a : AStrat), a.WF → (sys.simulate { a := a, d := d }.f s n).2 ≠ 0

theorem AP.State.dHws_iff_dHws_bounded' {s : State} [hs : sys.WF s] : s.dHws ↔ ∃ (n : ℕ) (d : DStrat), d.WF ∧ ∀ (a : AStrat), a.WF → (sys.simulate { a := a, d := d }.f s n).2 ≠ 0

theorem AP.State.dHws_iff_dHws_bounded {s : State} [hs : sys.WF s] : s.dHws ↔ ∃ (n : ℕ) (d : DStrat), d.WF ∧ ∀ (a : AStrat), a.WF → ∃ (s' : State) (r : ℕ), sys.simulate { a := a, d := d }.f s n = (s', r) ∧ r ≠ 0

def AP.State.aTrap (s : State) : Set PointZ

Equations

• s.aTrap = {p : PointZ | ∃ (s' : AP.State), AP.sys.Reachable s s' ∧ s'.aPos = p}

def AP.State.aTrapped (s : State) : Prop

Equations

• s.aTrapped = s.aTrap.Finite

def AP.State.aTrappedIn (s : State) (ps : Set PointZ) : Prop

Equations

• s.aTrappedIn ps = ∀ (s' : AP.State), AP.sys.Reachable s s' → s'.aPos ∈ ps

def AP.State.dEntrapsAIn (s : State) (st : Strat) (ps : Set PointZ) : Prop

Equations

• s.dEntrapsAIn st ps = ∃ (n : ℕ), (AP.sys.simulate st.f s n).1.aTrappedIn ps

theorem AP.State.aTrappedIn_iff_of_not_hasTr {sa : State} {ps : Set PointZ} (h : ¬sys.hasTr sa) : sa.aTrappedIn ps ↔ sa.aPos ∈ ps

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

theorem AP.State.dEntrapsAIn_of_forall_dWins {s : State} [hs : sys.WF s] {d : DStrat} [Hd : d.WF] (h : ∀ (a : AStrat), a.WF → s.dWins { a := a, d := d }) : ∃ (N : ℕ), ∀ (a : AStrat), a.WF → s.dEntrapsAIn { a := a, d := d } {p : PointZ | p ∈ Point.nbhd 0 ↑N}

theorem AP.State.aTrapped_of_aTrappedIn_and_finite {s : State} {ps : Set PointZ} (h₁ : s.aTrappedIn ps) (h₂ : ps.Finite) : s.aTrapped

theorem AP.State.aTrap_eq_of_not_hasTr {s : State} (h : ¬sys.hasTr s) : s.aTrap = {s.aPos}

theorem AP.State.aTrapped_of_not_hasTr {s : State} (h : ¬sys.hasTr s) : s.aTrapped

theorem AP.State.mem_aTrap_iff {s : State} {p : PointZ} : p ∈ s.aTrap ↔ ∃ (s' : State), sys.Reachable s s' ∧ s'.aPos = p

inductive AP.State.AReachable (s : State) : PointZ → Prop

• mk₁ {s : State} : s.AReachable s.aPos
• mk₂ {s : State} {p p' : PointZ} : s.AReachable p → Point.dist p p' ≤ ↑s.pw → p' ∉ s.taken → s.AReachable p'

theorem AP.State.aReachable_of_mem_aTrap {s : State} {p : PointZ} [hs : sys.WF s] (h : p ∈ s.aTrap) : s.AReachable p

@[simp]

theorem AP.ASTate.tr_eq_none_iff {s : State} {p : PointZ} [hs : AState s] : sys.tr s p = none ↔ s.aPos = p ∨ p ∈ s.taken ∨ ↑s.pw < Point.dist p s.aPos

@[simp]

theorem AP.DSTate.tr_eq_none_iff {s : State} {p : PointZ} [hs : DState s] : sys.tr s p = none ↔ s.aPos = p ∨ p ∈ s.taken

instance AP.instWFMk'OfSimFnStatePointZSys_2 {f : State → PointZ} [hf : sys.SimFn f] : { f := f }.WF

instance AP.instWFMk'OfSimFnStatePointZSys_3 {f : State → PointZ} [hf : sys.SimFn f] : { f := f }.WF

theorem AP.exi_strat_of_simFn (f : State → PointZ) [hf : sys.SimFn f] : ∃ (a : AStrat) (d : DStrat), a.WF ∧ d.WF ∧ f = { a := a, d := d }.f

theorem AP.exi_strat_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : ∃ (a : AStrat) (d : DStrat) (n : ℕ), a.WF ∧ d.WF ∧ sys.simulate { a := a, d := d }.f s n = (s', 0)

theorem AP.taken_subset_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s.taken ⊆ s'.taken

theorem AP.taken_subset_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : s.taken ⊆ s'.taken

theorem AP.State.exi_taken_disjoint_of_reachable {s₀ s : State} [hs₀ : sys.WF s₀] {ps : Set PointZ} (h₁ : ps.Finite) (h₂ : ∀ p ∈ ps, p ∉ s₀.taken) (h₃ : sys.Reachable s₀ s) : ∃ (s₁ : State), sys.Reachable s₀ s₁ ∧ s₁.aTurn = s.aTurn ∧ s₁.aPos = s.aPos ∧ ∀ p ∈ ps, p ∉ s₁.taken

theorem AP.State.exi_taken_disjoint_of_reachable_with_turn {s₀ s : State} [hs₀ : sys.WF s₀] {ps : Set PointZ} {t : Bool} (h₁ : ps.Finite) (h₂ : ∀ p ∈ ps, p ∉ s₀.taken) (h₃ : sys.Reachable s₀ s) (h₄ : s.aTurn = true → t = true) : ∃ (s₁ : State), sys.Reachable s₀ s₁ ∧ s₁.aTurn = t ∧ s₁.aPos = s.aPos ∧ ∀ p ∈ ps, p ∉ s₁.taken

theorem AP.State.mem_aTrap_of_aReachable {s : State} {p : PointZ} [hs : sys.WF s] (h : s.AReachable p) : p ∈ s.aTrap

@[simp]

theorem AP.State.mem_aTrap_iff_aReachable {s : State} {p : PointZ} [hs : sys.WF s] : p ∈ s.aTrap ↔ s.AReachable p

@[simp]

theorem AP.State.aReachable_aPos {s : State} : s.AReachable s.aPos

theorem AP.State.not_mem_taken_of_tr {s s' : State} {p p' : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') (h₂ : p' ∉ s'.taken) : p' ∉ s.taken

theorem AP.AState.aTrap_eq_of_tr {s s' : State} {p : PointZ} [hs : AState s] (h₂ : sys.tr s p = some s') : s'.aTrap = s.aTrap

theorem AP.aReachable_of_tr {s s' : State} {p' p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p' = some s') (h₂ : s'.AReachable p) : s.AReachable p

theorem AP.aReachable_of_reachable {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.Reachable s s') (h₂ : s'.AReachable p) : s.AReachable p

theorem AP.aTrap_subset_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s'.aTrap ⊆ s.aTrap

theorem AP.aTrap_subset_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : s'.aTrap ⊆ s.aTrap

theorem AP.aTrapped_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') (h₂ : s.aTrapped) : s'.aTrapped

theorem AP.aTrapped_of_reachable {s s' : State} [hs : sys.WF s] (h₁ : sys.Reachable s s') (h₂ : s.aTrapped) : s'.aTrapped

theorem AP.not_aReachable_of_mem_taken {s : State} {p : PointZ} [hs : sys.WF s] (h : p ∈ s.taken) : ¬s.AReachable p

theorem AP.DState.mem_taken_of_tr {s s' : State} {p : PointZ} [hs : DState s] (h : sys.tr s p = some s') : p ∈ s'.taken

theorem AP.DState.not_aReachable_of_tr {s s' : State} {p : PointZ} [hs : DState s] (h : sys.tr s p = some s') : ¬s'.AReachable p

theorem AP.AState.aReachable_strat_of_hasTr {a : AStrat} {s : State} [hs : AState s] [ha : a.WF] (h : sys.hasTr s) : s.AReachable (a.f s)

theorem AP.AState.aReachable_strat_of_tr {a : AStrat} {s s' : State} {p : PointZ} [hs : AState s] [ha : a.WF] (h : sys.tr s p = some s') : s.AReachable (a.f s)

theorem AP.aPos_ne_of_mem_taken {s : State} {p : PointZ} [hs : sys.WF s] (hp : p ∈ s.taken) : s.aPos ≠ p

theorem AP.not_mem_taken_of_aReachable {s : State} {p : PointZ} [hs : sys.WF s] (h : s.AReachable p) : p ∉ s.taken

@[simp]

theorem AP.aTrap_nonempty {s : State} [hs : sys.WF s] : s.aTrap.Nonempty

theorem AP.aTrap_ncard_pos_of_aTrapped {s : State} [hs : sys.WF s] (h : s.aTrapped) : 0 < s.aTrap.ncard

theorem AP.State.exi_dWins_of_aTrapped {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] (h : s.aTrapped) : ∃ (d : DStrat), d.WF ∧ s.dWins { a := a, d := d }

theorem AP.State.exi_dWins_of_simulate_aTrapped {s : State} [hs : sys.WF s] {n : ℕ} {a : AStrat} [Ha : a.WF] {d : DStrat} [Hd : d.WF] (h : (sys.simulate { a := a, d := d }.f s n).1.aTrapped) : ∃ (d : DStrat), d.WF ∧ s.dWins { a := a, d := d }

theorem AP.State.exi_dWins_iff_exi_aTrapped {s : State} [hs : sys.WF s] {a : AStrat} [Ha : a.WF] : (∃ (d : DStrat), d.WF ∧ s.dWins { a := a, d := d }) ↔ ∃ (n : ℕ) (d : DStrat), d.WF ∧ (sys.simulate { a := a, d := d }.f s n).1.aTrapped

theorem AP.State.dHws_iff_exi_dEntrapsAIn {s : State} [hs : sys.WF s] : s.dHws ↔ ∃ (N : ℕ) (d : DStrat), d.WF ∧ ∀ (a : AStrat), a.WF → s.dEntrapsAIn { a := a, d := d } {p : PointZ | p ∈ Point.nbhd 0 ↑N}

theorem AP.State.dHws_of_exi_aTrapped {s : State} [hs : sys.WF s] (h : ∃ (d : DStrat), d.WF ∧ ∀ (a : AStrat), a.WF → ∃ (n : ℕ), (sys.simulate { a := a, d := d }.f s n).1.aTrapped) : s.dHws