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

Equations

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