Lean4
/-- The TM1 model is a simplification and extension of TM0
(Post-Turing model) in the direction of Wang B-machines. The machine's
internal state is extended with a (finite) store `σ` of variables
that may be accessed and updated at any time.
A machine is given by a `Λ` indexed set of procedures or functions.
Each function has a body which is a `Stmt`, which can either be a
`move` or `write` command, a `branch` (if statement based on the
current tape value), a `load` (set the variable value),
a `goto` (call another function), or `halt`. Note that here
most statements do not have labels; `goto` commands can only
go to a new function. All commands have access to the variable value
and current tape value. -/
inductive Stmt
| move : Dir → Stmt → Stmt
| write : (Γ → σ → Γ) → Stmt → Stmt
| load : (Γ → σ → σ) → Stmt → Stmt
| branch : (Γ → σ → Bool) → Stmt → Stmt → Stmt
| goto : (Γ → σ → Λ) → Stmt
| halt : Stmt
