English
Let t1, t2 be ordinal trees, x ∈ α, and o1, o2 bounds. If t1 is bounded by o1 and x, and t2 is valid with root x, then the combined configuration is valid with bounds o1 on the left and o2 on the right.
Русский
Пусть t1, t2 — деревья, x ∈ α, и границы o1, o2. Если t1 ограничено o1 и x, а t2 допустимо с корнем x, то совместная структура допустима с границами o1 слева и o2 справа.
LaTeX
$$$\\forall t_1,t_2:\\ Ordnode(\\alpha), \\forall x:\\alpha, \\forall o_1,o_2,\\; t_1.\\text{Bounded}(o_1, o_1, x) \\wedge (\\operatorname{Valid}'(x,t_2,o_2)) \\Rightarrow \\operatorname{Valid}'(o_1,t_2,o_2).$$$
Lean4
theorem trans_left {t₁ t₂ : Ordnode α} {x : α} {o₁ o₂} (h : Bounded t₁ o₁ x) (H : Valid' x t₂ o₂) : Valid' o₁ t₂ o₂ :=
⟨h.trans_left H.1, H.2, H.3⟩
