English
For every Dyck word p, its semilength equals the number of nodes of the tree corresponding to p under the equivalence.
Русский
Для каждого слова Дайк p semilength равен числу узлов дерева, соответствующего p через эквивалентность.
LaTeX
$$$ \operatorname{semilength}(p) = \operatorname{numNodes}(\text{equivTree } p) $$$
Lean4
@[nolint unusedHavesSuffices]
theorem semilength_eq_numNodes_equivTree (p) : p.semilength = (equivTree p).numNodes :=
by
by_cases h : p = 0
· simp [h, equivTree, equivTreeToFun]
· rw [equivTree, Equiv.coe_fn_mk, equivTreeToFun]
simp_rw [h, dite_false, numNodes]
have := semilength_insidePart_lt h
have := semilength_outsidePart_lt h
rw [← semilength_insidePart_add_semilength_outsidePart_add_one h, semilength_eq_numNodes_equivTree p.insidePart,
semilength_eq_numNodes_equivTree p.outsidePart];
rfl
termination_by p.semilength
