English
Auxiliary lemmas about take and alternatingWord enabling prefix computations; see detailed parity-based cases.
Русский
Вспомогательные леммы о take и alternatingWord для вычисления префиксов; учитываются случаи по паритету.
LaTeX
$$$$ \text{(parity-based equalities for take and alternatingWord)} $$$$
Lean4
theorem listTake_succ_alternatingWord (i j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) :
List.take (k + 1) (alternatingWord i j (2 * p)) = i :: (List.take k (alternatingWord j i (2 * p))) :=
by
rw [listTake_alternatingWord j i p k (by cutsat), listTake_alternatingWord i j p (k + 1) h]
by_cases h_even : Even k
· simp [Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]
·
simp [(by rw [Nat.not_even_iff_odd] at h_even; exact Odd.add_one h_even : Even (k + 1)), alternatingWord_succ',
h_even]
