English
Let q1 and q2 be configurations in a binary-encoded TM-to-Partial-Rec machine. The translation of the predicate Λ'.pred(q1, q2) is realized by a TM2 program that begins with a pop from the main stack and then branches on the next symbol, possibly performing pushes and gotos to implement the predicate computation, and finally proceeds to the appropriate branch depending on the input states q1 and q2. This shows how the predicate operation is encoded in the target machine.
Русский
Пусть q1 и q2 — конфигурации в бинарной кодированной системе TM-to-Partrec. Перевод Λ'.pred(q1, q2) реализуется в TM2-процессе как последовательность действий: начинается со считывания из главного стека (pop), затем идет ветвление по следующему символу, с возможными операциями вставки (push) и переходами (goto) для реализации вычисления предиката, в зависимости от входных состояний q1 и q2 осуществляется переход к соответствующей ветви.
LaTeX
$$$$\operatorname{tr}(\Lambda'.\mathrm{pred}(q_1,q_2)) = \mathrm{pop'}\,\mathrm{main}\Bigl(\mathrm{branch}\bigl(\lambda s. s = \mathrm{some}\, \Gamma'.\mathrm{bit0}\bigr)\Bigl(\bigl(\mathrm{push}\, \mathrm{rev}\, (\lambda _ . \Gamma'.\mathrm{bit1})\bigr) \Big|\goto\ (\lambda _ . \Lambda'.\mathrm{pred}(q_1,q_2))\Bigr) \;\middle|\; \mathrm{branch}\bigl(\lambda s. \operatorname{natEnd}s.iget\bigr)\left(\goto\ (\lambda _ . q_1)\right)\left(\mathrm{peek'}\,\mathrm{main}\Bigl(\mathrm{branch}\bigl(\lambda s. \operatorname{natEnd}s.iget\bigr)\left(\goto(\lambda _ . unrev q_2)\right)\bigl( (\mathrm{push}\, \mathrm{rev}\, (\lambda _ . \Gamma'.\mathrm{bit0}) )\goto(\lambda _ . unrev q_2) \Bigr)\Bigr)\right) \Bigr)$$$$
Lean4
@[simp]
theorem tr_pred (q₁ q₂) :
tr (Λ'.pred q₁ q₂) =
pop' main
(branch (fun s => s = some Γ'.bit0) ((push rev fun _ => Γ'.bit1) <| goto fun _ => Λ'.pred q₁ q₂) <|
branch (fun s => natEnd s.iget) (goto fun _ => q₁)
(peek' main <|
branch (fun s => natEnd s.iget) (goto fun _ => unrev q₂)
((push rev fun _ => Γ'.bit0) <| goto fun _ => unrev q₂))) :=
rfl
