def Lookback (m : ℕ) (k : ℕ) (t : ℕ) {n : ℕ} (x : Mathlib.Vector (Fin 2) n) : Prop

Equations

• Lookback m k t x = ∀ u < t, (↑x).getI (m + u) = (↑x).getI (m + u - k)