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