English
If a relation tr is respected by f1,f2 via a predicate tr and aa, and ab is a Reaches₁ step for f1, then there exists a corresponding b₂ with tr b₁ b₂ and Reaches₁ f2 a₂ b₂.
Русский
Если отношение tr сохраняется в переходах f1,f2 и a1 связан с a2 отношением tr, и ab — это достижение Reaches₁ для f1, то существует соответствующая цель b₂, такая что tr b₁ b₂ и Reaches₁ f₂ a₂ b₂.
LaTeX
$$$\\forall {\\sigma_1 \\sigma_2 f_1 f_2} \\{tr: \\sigma_1 \\to \\sigma_2 \\to \\mathrm{Prop}\\},\\n \\text{Respects } f_1 f_2 tr \\to \\forall {a_1 a_2}, tr\\ a_1 a_2 \\to \\forall {b_1}, Reaches₁ f_1 a_1 b_1 \\to \\exists b_2, tr b_1 b_2 \\wedge Reaches₁ f_2 a_2 b_2$$$
Lean4
theorem tr_reaches₁ {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ a₂} (aa : tr a₁ a₂) {b₁}
(ab : Reaches₁ f₁ a₁ b₁) : ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂ := by
induction ab with
| single ac =>
have := H aa
rwa [show f₁ a₁ = _ from ac] at this
| @tail c₁ d₁ _ cd IH =>
rcases IH with ⟨c₂, cc, ac₂⟩
have := H cc
rw [show f₁ c₁ = _ from cd] at this
rcases this with ⟨d₂, dd, cd₂⟩
exact ⟨_, dd, ac₂.trans cd₂⟩
