English
Given a sequence s = [(a0,b0),(a1,b1),...], squashSeq(s,n) modifies the nth element by replacing (a_n,b_n) with (a_n, b_n + a_{n+1}/b_{n+1}) while leaving all other elements unchanged; if the term at n+1 terminates, squashSeq(s,n) = s.
Русский
Для последовательности s = [(a0,b0),(a1,b1),...], squashSeq(s,n) заменяет n-ый элемент парой (a_n,b_n) на (a_n, b_n + a_{n+1}/b_{n+1}) и оставляет остальные без изменений; если следующий элемент завершается, squashSeq(s,n) = s.
LaTeX
$$$\\text{squashSeq}(s,n)_i = \\begin{cases} (a_n,\, b_n + a_{n+1}/b_{n+1}) & i = n, \\\\ s_i & i \\neq n, \\end{cases}$, при условии существования $(a_n,b_n)$ и $(a_{n+1},b_{n+1})$; иначе $\\text{squashSeq}(s,n) = s$.$$
Lean4
/-- Given a sequence of `GenContFract.Pair`s `s = [(a₀, b₀), (a₁, b₁), ...]`, `squashSeq s n`
combines `⟨aₙ, bₙ⟩` and `⟨aₙ₊₁, bₙ₊₁⟩` at position `n` to `⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩`. For example,
`squashSeq s 0 = [(a₀, b₀ + a₁ / b₁), (a₁, b₁),...]`.
If `s.TerminatedAt (n + 1)`, then `squashSeq s n = s`.
-/
def squashSeq (s : Stream'.Seq <| Pair K) (n : ℕ) : Stream'.Seq (Pair K) :=
match Prod.mk (s.get? n) (s.get? (n + 1)) with
| ⟨some gp_n, some gp_succ_n⟩ =>
Stream'.Seq.nats.zipWith (fun n' gp => if n' = n then ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ else gp) s
| _ => s
