contsAux_stable_step_of_terminated

English

If n ≤ m and g.TerminatedAt n, then contsAux m = contsAux (n+1).

Русский

Если n ≤ m и g.TerminatedAt n, то contsAux m = contsAux (n+1).

LaTeX

$$$$\text{If } n \le m \text{ and } \text{TerminatedAt}(g,n),\; \text{then } \text{contsAux}(m) = \text{contsAux}(n+1).$$$$

Lean4

theorem contsAux_stable_step_of_terminated (terminatedAt_n : g.TerminatedAt n) :
    g.contsAux (n + 2) = g.contsAux (n + 1) :=
  by
  rw [terminatedAt_iff_s_none] at terminatedAt_n
  simp only [contsAux, terminatedAt_n]

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