English
For any k, s, q, trStmts₁ (stRun s q) equals the union of {go k s q, ret q} with trStmts₁ q.
Русский
Для любых k, s, q множество trStmts₁ (stRun s q) равно объединению {go k s q, ret q} с trStmts₁ q.
LaTeX
$$$ trStmts_1(stRun s q) = \{go\, k\, s\, q, ret\, q\} \cup trStmts_1(q) $$$
Lean4
/-- The set of machine states accessible from an initial TM2 statement. -/
noncomputable def trStmts₁ : TM2.Stmt Γ Λ σ → Finset (Λ' K Γ Λ σ)
| TM2.Stmt.push k f q => {go k (StAct.push f) q, ret q} ∪ trStmts₁ q
| TM2.Stmt.peek k f q => {go k (StAct.peek f) q, ret q} ∪ trStmts₁ q
| TM2.Stmt.pop k f q => {go k (StAct.pop f) q, ret q} ∪ trStmts₁ q
| TM2.Stmt.load _ q => trStmts₁ q
| TM2.Stmt.branch _ q₁ q₂ => trStmts₁ q₁ ∪ trStmts₁ q₂
| _ => ∅
