theorem AP.Edge.cnd₁_of_ptsArr_subset_aux₁ {arr₁ arr₂ : Array Bool} {d : ℤ} (h₁ : cnd₁ d arr₁ 0) (h₂ : arr₁.size = 7) (h₃ : arr₂.size = 7) (h₄ : ∀ i < arr₁.size, arr₁[i]? = some true → arr₂[i]? = some true) : cnd₁ d arr₂ 0

theorem AP.Edge.cnd₁_of_ptsArr_subset_aux₂ {arr₁ arr₂ : Array Bool} {d : ℤ} (h₁ : cnd₁ d arr₁ 0) (h₂ : arr₁.size ≤ 7) (h₃ : arr₂.size ≤ 7) (h₄ : ∀ i < arr₁.size, arr₁[i]? = some true → arr₂[i]? = some true) : cnd₁ d arr₂ 0

theorem AP.Edge.cnd₁_of_ptsArr_subset {arr₁ arr₂ : Array Bool} {offset : ℕ} {d : ℤ} (h₁ : cnd₁ d arr₁ offset) (h₃ : ∀ i < arr₁.size, arr₁[i]? = some true → arr₂[i]? = some true) : cnd₁ d arr₂ offset

theorem AP.Edge.cnd₀_of_taken_subset {s s' : State} (h₁ : cnd₀ s) (h₃ : s'.aPos = s.aPos) (h₂ : s.taken ⊆ s'.taken) : cnd₀ s'

theorem AP.Edge.neg_aPos_y_of_tr_aState_cnd₀ {s : State} [hpw : Fact (s.pw = 1)] {s' : State} {p : PointZ} [hs : AState s] (h₁ : cnd₀ s) (h₂ : sys.tr s p = some s') : s'.aPos.y < 0

theorem AP.Edge.cnd₀_of_tr_tr_aState {sa sd sa' : State} {pa pd : PointZ} [hsa : AState sa] [hpw : Fact (sa.pw = 1)] (h₀ : cnd₀ sa) (h₁ : sys.tr sa pa = some sd) (h₂ : sys.tr sd pd = some sa') (h₃ : edge₀.f sd = some pd) : cnd₀ sa'

theorem AP.Edge.not_mem_taken_f₁_of_not_cnd₀ {s : State} {p : PointZ} (h₃ : edge₀.f₁ s = some p) : p ∉ s.taken

theorem AP.Edge.cnd₀_of_tr_tr_st_aState {sa sd sa' : State} {p : PointZ} {d : DStrat} [hsa : AState sa] [hpw : Fact (sa.pw = 1)] (h₀ : cnd₀ sa) (h₁ : sys.tr sa p = some sd) (h₂ : sys.tr sd ((edge₀.defense.st d).f sd) = some sa') : cnd₀ sa'

theorem AP.Edge.cnd₀_simulate_mul_two_full_of_aState {s : State} [hpw : Fact (s.pw = 1)] {s₁ : State} {a : AStrat} {d : DStrat} {n : ℕ} [hs : AState s] (h₁ : cnd₀ s) (h₂ : sys.simulate { a := a, d := edge₀.defense.st d }.f s (n * 2) = (s₁, 0)) : cnd₀ s₁

theorem AP.Edge.edge₀_simulate_full_neg_aPos_y_of_aState {s : State} [hpw : Fact (s.pw = 1)] {s₁ : State} {a : AStrat} {d : DStrat} {n : ℕ} [hs : AState s] (h₁ : s.aPos.y ≤ -6) (h₂ : sys.simulate { a := a, d := edge₀.defense.st d }.f s n = (s₁, 0)) : s₁.aPos.y < 0

theorem AP.Edge.edge₀_simulate_neg_aPos_y_of_aState {s : State} [hpw : Fact (s.pw = 1)] {a : AStrat} {d : DStrat} {n : ℕ} [hs : AState s] (h : s.aPos.y ≤ -6) : (sys.simulate { a := a, d := edge₀.defense.st d }.f s n).1.aPos.y < 0

theorem AP.Edge.edge₀_simulate_neg_aPos_y {s : State} [hpw : Fact (s.pw = 1)] {a : AStrat} {d : DStrat} {n : ℕ} [hs : sys.WF s] (h : s.aPos.y ≤ -6) : (sys.simulate { a := a, d := edge₀.defense.st d }.f s n).1.aPos.y < 0

theorem AP.Edge.wf_defense_edge₀ : edge₀.defense.WF

theorem AP.Edge.wf_defense_of_down {e : Edge} (h : e.dir = Dir.down) : e.defense.WF

theorem AP.Edge.wf_defense_of_left {e : Edge} (h : e.dir = Dir.left) : e.defense.WF

theorem AP.Edge.wf_defense_of_up {e : Edge} (h : e.dir = Dir.up) : e.defense.WF

theorem AP.Edge.wf_defense_of_right {e : Edge} (h : e.dir = Dir.right) : e.defense.WF

theorem AP.Edge.wf_defense {e : Edge} : e.defense.WF

@[simp]

instance AP.Edge.instWFDefense {e : Edge} : e.defense.WF