Documentation

Projects.AP.Defense.Edge.Cnd

source
def AP.Edge.cnd₀ (s : State) :
Prop
Equations
Instances For
    source
    def AP.Edge.cnd₁ (d : ℤ) (arr : Array Bool) (offset : ℕ) :
    Prop
    Equations
    Instances For
      source
      def AP.Edge.aMove₀' (m : Fin 8) :
      PointZ
      Equations
      Instances For
        source
        def AP.Edge.aMove₀ (p : PointZ) (m : Fin 8) :
        PointZ
        Equations
        Instances For
          source
          @[instance_reducible]
          instance AP.Edge.instDecidableCnd₀ {s : State} :
          Decidable (cnd₀ s)
          Equations
          source
          @[instance_reducible]
          instance AP.Edge.instDecidableCnd₁ {d : ℤ} {arr : Array Bool} {offset : ℕ} :
          Decidable (cnd₁ d arr offset)
          Equations
          source
          @[simp]
          theorem AP.Edge.size_ptsArr {s : State} {offset : ℤ} {n : ℕ} :
          (edge₀.ptsArr s offset n).size = n
          source
          theorem AP.Edge.cnd₀_iff_f₁_edge₀_eq_none_of_neg_aPos_y {s : State} (h : s.aPos.y < 0) :
          cnd₀ s ↔ edge₀.f₁ s = none
          source
          theorem AP.Edge.neg_aPos_y_of_cnd₀ {s : State} (h : cnd₀ s) :
          s.aPos.y < 0
          source
          theorem AP.Edge.cnd₀_of_aPos_y_le_neg_6 {s : State} (h : s.aPos.y ≤ -6) :
          cnd₀ s
          source
          theorem AP.Edge.cnd₀_iff_cnd₁ {s : State} :
          cnd₀ s ↔ cnd₁ (-s.aPos.y) (edge₀.ptsArr s (-3) 7) 0
          source
          theorem AP.Edge.cnd₁_iff_cnd₁_extract {arr : Array Bool} {offset : ℕ} {d : ℤ} :
          cnd₁ d arr offset ↔ cnd₁ d (arr.extract offset (offset + 7)) 0
          source
          theorem AP.Edge.cnd₁_iff_cnd₁_append {arr : Array Bool} {offset : ℕ} {d : ℤ} {n : ℕ} :
          cnd₁ d arr offset ↔ cnd₁ d { toList := arr.toList ++ List.replicate n false } offset
          source
          theorem AP.Edge.cnd₁_iff_cnd₁_min_6 {arr : Array Bool} {offset : ℕ} {d : ℤ} :
          cnd₁ d arr offset ↔ cnd₁ (min 6 d) arr offset
          source
          @[simp]
          theorem AP.Edge.ptsArr_eq_empty_iff {e : Edge} {s : State} {z : ℤ} {n : ℕ} :
          e.ptsArr s z n = #[] ↔ n = 0
          source
          @[simp]
          theorem AP.Edge.ptsArr_zero {e : Edge} {s : State} {z : ℤ} :
          e.ptsArr s z 0 = #[]
          source
          theorem AP.Edge.getBorderPoint_add {p : PointZ} {n m : ℤ} :
          edge₀.getBorderPoint p (n + m) = edge₀.getBorderPoint p n + { x := m, y := 0 }
          source
          @[simp]
          theorem AP.Edge.extract_ptsArr {s : State} {z : ℤ} {n i j : ℕ} :
          (edge₀.ptsArr s z n).extract i j = edge₀.ptsArr s (z + ↑i) (min n j - i)
          source
          theorem AP.Edge.exi_aMove₀_of_dist_eq_one {p p' : PointZ} (h : Point.dist p' p = 1) :
          ∃ (m : Fin 8), aMove₀ p m = p'
          source
          theorem AP.Edge.exi_aMove₀_of_tr_eq_some {s : State} [hpw : Fact (s.pw = 1)] {s' : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s') :
          ∃ (m : Fin 8), aMove₀ s.aPos m = p
          source
          theorem AP.Edge.aMove₀_dist_eq_one (p : PointZ) (m : Fin 8) :
          Point.dist (aMove₀ p m) p = 1
          source
          @[simp]
          theorem AP.Edge.le_one_add_aMove₀_x {p : PointZ} {m : Fin 8} :
          p.x ≤ 1 + (aMove₀ p m).x
          source
          @[simp]
          theorem AP.Edge.one_add_aMove₀_le_two_add_x {p : PointZ} {m : Fin 8} :
          1 + (aMove₀ p m).x ≤ 2 + p.x
          source
          @[simp]
          theorem AP.Edge.f₄_lt_7 {d : ℤ} {f : ℕ → Bool} :
          f₄ d f < 7
          source
          theorem AP.Edge.ptsArr_eq_of_taken_eq {s s' : State} {z : ℤ} {n : ℕ} (h : s'.taken = s.taken) :
          edge₀.ptsArr s' z n = edge₀.ptsArr s (z + s'.aPos.x - s.aPos.x) n
          source
          theorem AP.Edge.ptsArr_eq_of_aPos_eq_and_taken_eq_insert.proof₁ {s s' : State} {p : PointZ} (h₁ : s'.taken = s.taken.insert p) (h₃ : ∃ (z : ℤ), |z| ≤ 3 ∧ edge₀.getBorderPoint s.aPos z = p) :
          (p.x - s.aPos.x + 3).toNat < (edge₀.ptsArr s (-3) 7).size
          source
          theorem AP.Edge.ptsArr_eq_of_aPos_eq_and_taken_eq_insert {s s' : State} {p : PointZ} (h₂ : s'.aPos = s.aPos) (h₁ : s'.taken = s.taken.insert p) (h₃ : ∃ (z : ℤ), |z| ≤ 3 ∧ edge₀.getBorderPoint s.aPos z = p) :
          edge₀.ptsArr s' (-3) 7 = (edge₀.ptsArr s (-3) 7).set (p.x - s.aPos.x + 3).toNat true ⋯
          source
          theorem AP.Edge.exi_fin_y_of_f_eq_some {s : State} {p : PointZ} (h : edge₀.f s = some p) :
          ∃ (y : Fin 6), s.aPos.y = -↑↑y