English
Prefix of length k of the 2p-length alternatingWord is determined by parity: even k uses i-start, odd k uses j-start.
Русский
Префикс длины k от слова alternatingWord длины 2p определяется по чётности: чётное k — с i, нечётное — с j.
LaTeX
$$$\\\\text{List.take}(k,\\\\text{alternatingWord}(i, j, 2p)) = \\\\begin{cases} alternatingWord(i, j, k), & k \\\\text{even} \\\\cr alternatingWord(j, i, k), & k \\\\text{odd} \\\\cr \\end{cases}$$$
Lean4
theorem listTake_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
List.take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k := by
induction k with
| zero => simp only [take_zero, Even.zero, ↓reduceIte, alternatingWord]
| succ k h' =>
have hk : k < 2 * p := by omega
apply h' at hk
by_cases h_even : Even k
· simp only [h_even, ↓reduceIte] at hk
simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
rw [← List.take_concat_get (by simp; cutsat), alternatingWord_succ, ← hk]
apply congr_arg
rw [getElem_alternatingWord i j (2 * p) k (by cutsat)]
simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]
· simp only [h_even, ↓reduceIte] at hk
simp only [(by simp at h_even; exact Odd.add_one h_even : Even (k + 1)), ↓reduceIte]
rw [← List.take_concat_get (by simp; cutsat), alternatingWord_succ, hk]
apply congr_arg
rw [getElem_alternatingWord i j (2 * p) k (by cutsat)]
simp [(by apply Nat.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]
