Lean4
theorem tr_respects_aux {q v T k} {S : ∀ k, List (Γ k)}
(hT : ∀ k, ListBlank.map (proj k) T = ListBlank.mk ((S k).map some).reverse) (o : StAct K Γ σ k)
(IH :
∀ {v : σ} {S : ∀ k : K, List (Γ k)} {T : ListBlank (∀ k, Option (Γ k))},
(∀ k, ListBlank.map (proj k) T = ListBlank.mk ((S k).map some).reverse) →
∃ b,
TrCfg (TM2.stepAux q v S) b ∧
Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b) :
∃ b,
TrCfg (TM2.stepAux (stRun o q) v S) b ∧
Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b :=
by
simp only [trNormal_run, step_run]
have hgo := tr_respects_aux₁ M o q v (hT k) _ le_rfl
obtain ⟨T', hT', hrun⟩ := tr_respects_aux₂ (Λ := Λ) hT o
have := hgo.tail' rfl
rw [tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hT k),
List.getElem?_eq_none (le_of_eq List.length_reverse), Option.isNone, cond, hrun, TM1.stepAux] at this
obtain ⟨c, gc, rc⟩ := IH hT'
refine ⟨c, gc, (this.to₀.trans (tr_respects_aux₃ M _) c (TransGen.head' rfl ?_)).to_reflTransGen⟩
rw [tr, TM1.stepAux, Tape.mk'_head, addBottom_head_fst]
exact rc
