length'_cons — Mathlib

English

The modified length' of the sequence cons x s equals the modified length' of s plus one.

Русский

Длина' последовательности, образованной как cons x s, равна длине' последовательности s плюс единица.

LaTeX

$$$\mathrm{length}'(\mathrm{cons}(x, s)) = \mathrm{length}'(s) + 1$$$

Lean4

@[simp]
theorem length'_cons (x : α) (s : Seq α) : (cons x s).length' = s.length' + 1 :=
  by
  by_cases h : (cons x s).Terminates <;> have h' := h <;> rw [terminates_cons_iff] at h'
  · simp [length'_of_terminates h, length'_of_terminates h', length_cons h']
  · simp [length'_of_not_terminates h, length'_of_not_terminates h']

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