English
Mapping respects the step operation under a right inverse and compatibility condition.
Русский
Отображение сохраняет переходы шага под условием обратной совместности и совместимости.
LaTeX
$$$\\forall {S} (ss : Supports M S) (f_1 f_2 \\text{ etc}),\\; \\text{Respects}(\\mathrm{step}\ M, \\mathrm{step}(M.map\\ f_1 f_2 \\ g_1 \\ g_2))\\ (\\lambda a b => a.q \\in S \\wedge \\mathrm{Cfg.map} f_1 g_1 a = b)$$$
Lean4
theorem map_respects (g₁ : PointedMap Λ Λ') (g₂ : Λ' → Λ) {S} (ss : Supports M S) (f₂₁ : Function.RightInverse f₁ f₂)
(g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q) :
Respects (step M) (step (M.map f₁ f₂ g₁ g₂)) fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁ a = b :=
by
intro c _ ⟨cs, rfl⟩
cases e : step M c
· rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
rfl
· refine ⟨_, ⟨step_supports M ss e cs, rfl⟩, TransGen.single ?_⟩
rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
rfl
