English
In the reverse direction, if b2 ∈ eval f2 a2 then there exists b1 with tr b1 b2 and b1 ∈ eval f1 a1, given the respect condition.
Русский
В обратном направлении, если b2 ∈ eval f2 a2, то существует b1 с tr b1 b2 и b1 ∈ eval f1 a1, при условии соблюдения отношений.
LaTeX
$$$\\forall {f_1 f_2 tr} (H : Respects f_1 f_2 tr) \\forall {a_1 b_2 a_2}, tr a_1 a_2 \\to b_2 \\in eval f_2 a_2 \\Rightarrow \\exists b_1, tr b_1 b_2 \\wedge b_1 \\in eval f_1 a_1$$$
Lean4
theorem tr_eval_rev {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ b₂ a₂} (aa : tr a₁ a₂)
(ab : b₂ ∈ eval f₂ a₂) : ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁ :=
by
obtain ⟨ab, b0⟩ := mem_eval.1 ab
rcases tr_reaches_rev H aa ab with ⟨c₁, c₂, bc, cc, ac⟩
cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc
refine ⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩
have := H cc
rcases hfc : f₁ c₁ with - | d₁
· rfl
rw [hfc] at this
rcases this with ⟨d₂, _, bd⟩
rcases TransGen.head'_iff.1 bd with ⟨e, h, _⟩
cases b0.symm.trans h
