Documentation

Projects.AP.Defense.Edge.Basic

source
theorem AP.Edge.mem_points_iff_memPoints {e : Edge} {p : PointZ} :
p ∈ e.points ↔ e.memPoints p = true
source
@[instance_reducible]
instance AP.Edge.instDecidableMemPointZSetPoints {e : Edge} {p : PointZ} :
Decidable (p ∈ e.points)
Equations
source
theorem AP.Edge.memPoints_eq {e : Edge} {p : PointZ} :
e.memPoints p = decide (p ∈ e.points)
source
theorem AP.Edge.points_inj {e₁ e₂ : Edge} (h : e₁.points = e₂.points) :
e₁ = e₂
source
@[simp]
theorem AP.Edge.points_eq_points_iff {e₁ e₂ : Edge} :
e₁.points = e₂.points ↔ e₁ = e₂
source
@[simp]
theorem AP.Edge.ps_defense {e : Edge} :
e.defense.ps = e.points
source
@[simp]
theorem AP.Edge.getBorderPoint_inj {e : Edge} {p : PointZ} {z₁ z₂ : ℤ} :
e.getBorderPoint p z₁ = e.getBorderPoint p z₂ ↔ z₁ = z₂
source
theorem AP.Edge.mem_cndMp_of_cnd_eq_false {d : ℤ} {f : ℕ → Bool} (h : cnd d f = false) :
d ∈ cndMp
source
theorem AP.Edge.cndMp_keys :
cndMp.keys = [1, 2, 3, 4, 5]
source
@[simp]
theorem AP.Edge.mem_cndMp_iff {d : ℤ} :
d ∈ cndMp ↔ 1 ≤ d ∧ d ≤ 5
source
theorem AP.Edge.f₅_le_6_of {g : ℕ → Bool} {m : Option ℕ} (h : ∀ (n : ℕ), m = some n → n ≤ 6) :
f₅ g m ≤ 6
source
@[simp]
theorem AP.Edge.f₄_le_6 {d : ℤ} {g : ℕ → Bool} :
f₄ d g ≤ 6
source
theorem AP.Edge.of_f₁_eq_some {e : Edge} {s : State} {p : PointZ} (h : e.f₁ s = some p) :
0 < e.dist s.aPos ∧ e.dist s.aPos ≤ 5 ∧ ∃ (z : ℤ), |z| ≤ 3 ∧ e.getBorderPoint s.aPos z = p
source
theorem AP.Edge.of_f_eq_some {e : Edge} {s : State} {p : PointZ} (h : e.defense.f s = some p) :
0 < e.dist s.aPos ∧ e.dist s.aPos ≤ 5 ∧ p ∉ s.taken ∧ ∃ (z : ℤ), |z| ≤ 3 ∧ e.getBorderPoint s.aPos z = p
source
theorem AP.Edge.dist_eq_zero_of_f_eq_some {e : Edge} {s : State} {p : PointZ} (h : e.defense.f s = some p) :
e.dist p = 0
source
theorem AP.Edge.not_mem_taken_of_f_eq_some {e : Edge} {s : State} {p : PointZ} (h : e.defense.f s = some p) :
p ∉ s.taken
source
@[simp]
theorem AP.Edge.validTr_defense {e : Edge} :
e.defense.ValidTr
source
@[simp]
theorem AP.Edge.dir_edge₀ :
edge₀.dir = Dir.down
source
@[simp]
theorem AP.Edge.offset_edge₀ :
edge₀.offset = 0
source
@[simp]
theorem AP.Edge.dist_edge₀ {p : PointZ} :
edge₀.dist p = -p.y
source
theorem AP.Edge.cnd_congr {d : ℤ} {f₁ f₂ : ℕ → Bool} (h : ∀ i < 7, f₁ i = f₂ i) :
cnd d f₁ = cnd d f₂
source
@[simp]
theorem AP.Edge.get?_6_cndMp :
Map.get? 6 cndMp = none
source
@[simp]
theorem AP.Edge.get?_1_cndMp :
Map.get? 1 cndMp = some [#[false, false, true, true, true, false, false]]
source
theorem AP.Edge.f₁_eq_of_f_eq_some {e : Edge} {s : State} {p : PointZ} (h : e.f s = some p) :
e.f₁ s = some p
source
theorem AP.Edge.of_f₃_eq_some {d : ℤ} {g : ℕ → Bool} {k : ℕ} (h : f₃ d g = some k) :
1 ≤ d ∧ d ≤ 6 ∧ k ≤ 6
source
theorem AP.Edge.of_f₂_eq_some {d : ℤ} {arr : Array Bool} {offset k : ℕ} (h : f₂ d arr offset = some k) :
1 ≤ d ∧ d ≤ 6 ∧ k ≤ 6
source
@[simp]
theorem AP.Edge.cnd_const_true {d : ℤ} :
(cnd d fun (x : ℕ) => true) = true
source
theorem AP.Edge.f_eq_none_of_6_le_dist {e : Edge} {s : State} (h : 6 ≤ e.dist s.aPos) :
e.f s = none
source
theorem AP.Edge.f_defense_eq_none_of_6_le_dist {e : Edge} {s : State} (h : 6 ≤ e.dist s.aPos) :
e.defense.f s = none