English
In the translation of a return node that conses a continuation in the TM2-to-Parts mapping, the translation NaN yields a goto sequence leading to a specific stack arrangement and the translation of the subcontinuation.
Русский
В переводе узла возврата, который добавляет продолжение, формируется последовательность goto и соответствующая конфигурация стека.
LaTeX
$$$\\operatorname{tr}(\\Lambda'.ret(Cont'.cons₁ fs k)) = \\text{goto }(\\cdots)\\;\\text{(specific stack transformation and translation of }fs\\text{)}$$$
Lean4
@[simp]
theorem tr_ret_cons₁ (fs k) :
tr (Λ'.ret (Cont'.cons₁ fs k)) =
goto fun _ =>
move₂ (fun _ => false) main aux <|
move₂ (fun s => s = Γ'.consₗ) stack main <| move₂ (fun _ => false) aux stack <| trNormal fs (Cont'.cons₂ k) :=
rfl
