convs'Aux_stable_step_of_terminated

English

If n ≤ m and g.TerminatedAt n, then conts m = conts n.

Русский

Если n ≤ m и g.TerminatedAt n, conts m = conts n.

LaTeX

$$$$\text{TerminatedAt}(g,n) \Rightarrow \text{conts}(m) = \text{conts}(n) \text{ for } m \ge n.$$$$

Lean4

theorem convs'Aux_stable_step_of_terminated {s : Stream'.Seq <| Pair K} (terminatedAt_n : s.TerminatedAt n) :
    convs'Aux s (n + 1) = convs'Aux s n :=
  by
  change s.get? n = none at terminatedAt_n
  induction n generalizing s with
  | zero => simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]
  | succ n IH =>
    cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some
      gp_head =>
      have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]

Похожие утверждения