Multi-tape Turing machines

DefinitionSuccessor under a transition function#✓fully proved

Let \(\delta\) be a transition function of a multi-tape Turing machine with \(k\) work tapes, assigning an action to each state, input symbol and tuple of \(k\) work tape symbols, where a symbol may be blank. The successor of a configuration \(c\) under \(\delta\) is \(c\) itself if \(c\) is halted, and otherwise the configuration obtained by applying to \(c\) the action \(\delta(q, a, b)\), where \(q\) is the state of \(c\), \(a\) the symbol under its input head and \(b\) the symbols under its work tape heads.

def stepWith (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State)
    (cfg : Cfg k Symbol State input) : Cfg k Symbol State input :=
  match cfg.state with
  | none => cfg
  | some q => (tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg

Used by 5

Used byRuns of a machine given by a transition function · Step of a machine given by a transition function · Codes denote finite-state machines · The evaluator simulates the machine step for step · Step of the machine of a code

TheoremStep of a machine given by a transition function#✓fully proved

Let \(M\) be the deterministic multi-tape Turing machine with initial state \(q_0\) and transition function \(\delta\). For every configuration \(c\), the step of \(M\) from \(c\) is the successor of \(c\) under \(\delta\): \(c\) itself if \(c\) is halted, and otherwise the result of applying to \(c\) the action that \(\delta\) selects for the state of \(c\) and the symbols under its input and work tape heads.

theorem step_ofTr (q₀ : State)
    (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State)
    (cfg : Cfg k Symbol State input) : (MultiTapeTM.ofTr q₀ tr).step cfg = stepWith tr cfg

Uses 1 · Used by 2

Statement usesSuccessor under a transition function

Used byRuns of a machine given by a transition function · Step of the machine of a code

TheoremRuns of a machine given by a transition function#✓fully proved

Let \(\delta\) be a transition function that assigns an action to every state, symbol or blank read on the input tape, and tuple of symbols or blanks read on the work tapes, and let \(M\) be the deterministic multi-tape Turing machine with initial state \(q_0\) and transition function \(\delta\). Let \(S_\delta\) be the map on configurations that fixes every halted configuration and sends a running configuration in state \(q\) to the result of applying to it the action that \(\delta\) selects for \(q\) and the symbols or blanks under its heads. For every configuration \(c\) and every \(t \in \mathbb{N}\), the run of \(M\) from \(c\) is in configuration \(S_\delta^t(c)\) after \(t\) steps, where \(S_\delta^t\) is the \(t\)-fold iterate of \(S_\delta\).

theorem runFrom_ofTr (q₀ : State)
    (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State)
    (cfg : Cfg k Symbol State input) (t : ℕ) :
    (MultiTapeTM.ofTr q₀ tr).runFrom cfg t = (stepWith tr)^[t] cfg

Uses 2

Statement usesSuccessor under a transition function

Proof usesStep of a machine given by a transition function

TheoremStep determinism#✓fully proved

Let \(M\) be a deterministic multi-tape Turing machine, with the one-step relation it inherits as a nondeterministic machine. If a configuration \(c\) steps to both \(c_1\) and \(c_2\), then \(c_1 = c_2\).

theorem step_deterministic {c c₁ c₂ : Cfg k Symbol State input} (h₁ : tm.Step c c₁)
    (h₂ : tm.Step c c₂) : c₁ = c₂

TheoremPeeling off the first step of a run#✓fully proved

For a configuration \(c\) of a deterministic multi-tape Turing machine and every \(t \in \mathbb{N}\), the run from \(c\) after \(t + 1\) steps is in the same configuration as the run from the successor of \(c\) after \(t\) steps.

theorem runFrom_succ' (cfg : Cfg k Symbol State input) (t : ℕ) :
    tm.runFrom cfg (t + 1) = tm.runFrom (tm.step cfg) t

TheoremHalted configurations are fixed#✓fully proved

If a configuration \(c\) of a deterministic multi-tape Turing machine is halted, then for every \(t \in \mathbb{N}\) the run from \(c\) is in configuration \(c\) after \(t\) steps.

theorem runFrom_of_halted {cfg : Cfg k Symbol State input} (h : cfg.Halted) (t : ℕ) :
    tm.runFrom cfg t = cfg

TheoremHalting persists along a run#✓fully proved

For a configuration \(c\) of a deterministic multi-tape Turing machine and steps \(s \le t\), if the run from \(c\) is halted after \(s\) steps, then it is halted after \(t\) steps.

theorem halted_runFrom_mono {cfg : Cfg k Symbol State input} {s t : ℕ} (hst : s ≤ t)
    (h : (tm.runFrom cfg s).Halted) : (tm.runFrom cfg t).Halted

Used by 1

Used byHalting space-bounded runs obey the core-count time bound

TheoremHalting at step zero#✓fully proved

A deterministic multi-tape Turing machine started in a configuration \(c\) halts at step \(0\) if and only if \(c\) is halted.

@[simp]
theorem haltsAt_zero_iff {cfg : Cfg k Symbol State input} : tm.HaltsAt cfg 0 ↔ cfg.Halted

TheoremRun composition for halting#✓fully proved

Let \(c\) be a configuration of a deterministic multi-tape Turing machine and let \(m, n \in \mathbb{N}\). If the run from \(c\) is not halted after any \(s < m\) steps, and the run from the configuration reached after \(m\) steps halts at step \(n\) (it is halted after \(n\) steps and not halted after fewer), then the run from \(c\) halts at step \(m + n\).

theorem haltsAt_add {cfg : Cfg k Symbol State input} {m n : ℕ}
    (hm : ∀ s < m, ¬(tm.runFrom cfg s).Halted) (hn : tm.HaltsAt (tm.runFrom cfg m) n) :
    tm.HaltsAt cfg (m + n)

TheoremHalting step after a run prefix#✓fully proved

Let \(M\) be a deterministic multi-tape Turing machine, \(c\) a configuration of \(M\) and \(m, n\) natural numbers. If \(M\) started in \(c\) halts at step \(m + n\), that is, it is halted after \(m + n\) steps and not halted after any fewer, then \(M\) started in the configuration reached from \(c\) after \(m\) steps halts at step \(n\).

theorem HaltsAt.runFrom {cfg : Cfg k Symbol State input} {m n : ℕ}
    (h : tm.HaltsAt cfg (m + n)) : tm.HaltsAt (tm.runFrom cfg m) n

TheoremA time bound forces halting#✓fully proved

If a deterministic multi-tape Turing machine runs in time \(t\) on input \(w\), then the run from the initial configuration on \(w\) is halted after \(t\) steps.

theorem halted_runFrom_of_runsInTime {t : ℕ} (h : tm.RunsInTime input t) :
    (tm.runFrom (tm.initCfg input) t).Halted

Used by 3

Used byTime bounds space on one input · Output at a time bound · Time bounds of deterministic machines

TheoremTime bounds of deterministic machines#✓fully proved

Let \(M\) be a deterministic multi-tape Turing machine, \(w\) an input and \(t\) a natural number. Then \(M\) runs in time \(t\) on \(w\), that is, every computation path of \(M\) on \(w\) with at least \(t\) steps ends in a halted configuration, if and only if \(M\) started in its initial configuration on \(w\) is halted after \(t\) steps.

theorem runsInTime_iff_halted {t : ℕ} :
    tm.RunsInTime input t ↔ (tm.runFrom (tm.initCfg input) t).Halted

Uses 1 · Used by 2

Proof usesA time bound forces halting

Used byRelabelling preserves time bounds · The evaluator returns within the clock exactly when the machine runs in time

TheoremOutput determinism#✓fully proved

A deterministic machine computes at most one output on an input.

theorem computes_unique {o₁ o₂ : List Symbol} (h₁ : tm.Computes input o₁)
    (h₂ : tm.Computes input o₂) : o₁ = o₂

Used by 3

Used byA predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Output at a time bound

TheoremComputing an output means halting with it#✓fully proved

A deterministic multi-tape Turing machine computes the output \(o\) on input \(w\) if and only if there is a step \(t\) at which the run from the initial configuration on \(w\) halts (it is halted after \(t\) steps and not halted after any \(s < t\) steps) and the configuration it reaches after \(t\) steps has output tape \(o\).

theorem computes_iff_exists_haltsAt {o : List Symbol} :
    tm.Computes input o ↔
      ∃ t, tm.HaltsAt (tm.initCfg input) t ∧ (tm.runFrom (tm.initCfg input) t).output = o

TheoremOutput at a time bound#✓fully proved

If a deterministic multi-tape Turing machine runs in time \(t\) on input \(w\), then for every word \(o\) the machine computes \(o\) on \(w\) if and only if the configuration reached from the initial configuration on \(w\) after \(t\) steps has output tape \(o\).

theorem computes_iff_output_of_runsInTime {t : ℕ} (h : tm.RunsInTime input t)
    {o : List Symbol} :
    tm.Computes input o ↔ (tm.runFrom (tm.initCfg input) t).output = o

Uses 2

Proof usesOutput determinism · A time bound forces halting

TheoremSpace of the deterministic computation path#✓fully proved

Let \(M\) be a deterministic multi-tape Turing machine, \(x\) an input and \(t \in \mathbb{N}\). The number of work-tape cells visited along the computation path of \(M\) on \(x\) made of the first \(t\) steps from the initial configuration equals the space used by the run of \(M\) from the initial configuration on \(x\) up to step \(t\). Both count the visited cells on each work tape separately and sum over the work tapes.

theorem space_ofDeterministic (tm : MultiTapeTM k Symbol State) (x : List Symbol) (t : ℕ) :
    (MultiTapeNTM.ComputationPath.ofDeterministic tm x t).space =
      tm.spaceUsed (tm.initCfg x) t

Used by 1

Used bySpace bounds of deterministic machines

TheoremSpace bounds of deterministic machines#✓fully proved

Let \(M\) be a deterministic multi-tape Turing machine, \(x\) an input and \(s \in \mathbb{N}\). Then \(M\) runs in space \(s\) on \(x\), that is, every computation path of \(M\) on \(x\) visits at most \(s\) work-tape cells, if and only if for every \(t \in \mathbb{N}\) the run of \(M\) from the initial configuration on \(x\) visits at most \(s\) work-tape cells within its first \(t\) steps. Visited cells are counted on each work tape separately and summed over the work tapes.

theorem runsInSpace_iff_forall_spaceUsed_le {tm : MultiTapeTM k Symbol State} {x : List Symbol}
    {s : ℕ} : tm.RunsInSpace x s ↔ ∀ t, tm.spaceUsed (tm.initCfg x) t ≤ s

Uses 1 · Used by 1

Proof usesSpace of the deterministic computation path

Used byRelabelling preserves space bounds

DefinitionRelabelling the successor state of an action#✓fully proved

For a map \(f : Q \to Q'\) of states and an action \(a\) of a machine with \(k\) work tapes and states \(Q\), the relabelled action is the action with states \(Q'\) that moves the input head, writes and moves on the work tapes and outputs exactly as \(a\) does, and whose successor state is \(f(q)\) when \(a\) goes to state \(q\) and is halting when \(a\) halts.

def relabelAction (f : State → State') (a : Action k Symbol State) : Action k Symbol State' :=
  ⟨a.inputTape, a.workTapes, a.output, a.state.map f⟩

Used by 8

Used byApplying a relabelled action · Simulation up to a state relabelling · Every machine is a relabelling of itself · Relabelled machines step in lockstep · Relabellings compose · The code of a machine simulates it · A code's machine simulates its finite-state machine · Decoding the coding of an action

TheoremApplying a relabelled action#✓fully proved

Let \(f : Q \to Q'\) be a map of states; relabelling by \(f\) replaces a state \(q\) by \(f(q)\) and keeps the halting state. For every action \(a\) of a machine with \(k\) work tapes and states \(Q\) and every configuration \(c\) of such a machine, applying \(a\) with its successor state relabelled by \(f\) to \(c\) with its state relabelled by \(f\) gives the configuration obtained by applying \(a\) to \(c\) and then relabelling its state by \(f\).

theorem apply_relabelAction (f : State → State') (a : Action k Symbol State)
    (cfg : Cfg k Symbol State input) :
    (relabelAction f a).apply (cfg.mapState (Option.map f)) =
      (a.apply cfg).mapState (Option.map f)

Uses 1 · Used by 1

Statement usesRelabelling the successor state of an action

Used byRelabelled machines step in lockstep

StructureSimulation up to a state relabelling#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the same alphabet, with state sets \(Q\) and \(Q'\), and let \(f : Q \to Q'\). Then \(M'\) simulates \(M\) up to the relabelling \(f\) when the initial state of \(M'\) is \(f(q_0)\), where \(q_0\) is the initial state of \(M\), and for every state \(q \in Q\), every possibly blank symbol \(a\) under the input head and every tuple \(w\) of possibly blank symbols under the work heads, the action of \(M'\) in state \(f(q)\) reading \(a\) and \(w\) is the action of \(M\) in state \(q\) reading \(a\) and \(w\) with its successor state relabelled by \(f\) (a successor state \(q'\) becomes \(f(q')\), and halting stays halting).

Nothing is required of \(M'\) in states outside the range of \(f\), and \(f\) need not be injective.

structure IsRelabelling (f : State → State') (tm : MultiTapeTM k Symbol State)
    (tm' : MultiTapeTM k Symbol State') : Prop where
  /-- The initial state is relabelled. -/
  q₀ : tm'.q₀ = f tm.q₀
  /-- Transitions commute with the relabelling. -/
  tr : ∀ q a w, tm'.tr (f q) a w = relabelAction f (tm.tr q a w)

Uses 1 · Used by 19

Statement usesRelabelling the successor state of an action

Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Relabelling preserves computing a function within time and space bounds · Relabelling preserves what a machine computes · Relabelling preserves deciding a language · Initial configurations under relabelling · Every machine is a relabelling of itself · Lockstep runs · Lockstep runs from the initial configuration · Relabelling preserves space bounds · Relabelling preserves time bounds · Relabelled machines step in lockstep · Relabellings compose · Computability over codes · Decidability over codes · Every finite-state machine has a code · The code of a machine simulates it · A code's machine simulates its finite-state machine

TheoremRelabelling preserves halting#✓fully proved

Let \(f\) be a map of states. For every configuration \(c\), the configuration obtained from \(c\) by replacing its state \(q\) by \(f(q)\), and keeping the halting state, is halted if and only if \(c\) is halted.

@[simp]
theorem halted_mapState_iff (f : State → State') (cfg : Cfg k Symbol State input) :
    (cfg.mapState (Option.map f)).Halted ↔ cfg.Halted

Used by 2

Used byRelabelling preserves what a machine computes · Relabelling preserves time bounds

TheoremEvery machine is a relabelling of itself#✓fully proved

Every deterministic machine with \(k\) work tapes simulates itself up to the identity relabelling of its states.

theorem refl (tm : MultiTapeTM k Symbol State) : IsRelabelling id tm tm

Uses 2

Statement usesSimulation up to a state relabelling

Proof usesRelabelling the successor state of an action

TheoremRelabellings compose#✓fully proved

Let \(M\), \(M'\) and \(M''\) be multi-tape Turing machines with the same number of work tapes and the same alphabet, with state sets \(Q\), \(Q'\) and \(Q''\). If \(M'\) simulates \(M\) up to the state relabelling \(f : Q \to Q'\) and \(M''\) simulates \(M'\) up to the state relabelling \(g : Q' \to Q''\), then \(M''\) simulates \(M\) up to the state relabelling \(g \circ f\).

theorem trans {State'' : Type*} {g : State' → State''} {tm'' : MultiTapeTM k Symbol State''}
    (h : IsRelabelling f tm tm') (h' : IsRelabelling g tm' tm'') :
    IsRelabelling (g ∘ f) tm tm''

Uses 2

Statement usesSimulation up to a state relabelling

Proof usesRelabelling the successor state of an action

TheoremRelabelled machines step in lockstep#✓fully proved

Let \(M\) and \(M'\) be multi-tape Turing machines with the same number of work tapes and the same alphabet, with state sets \(Q\) and \(Q'\), such that \(M'\) simulates \(M\) up to the state relabelling \(f : Q \to Q'\). For a configuration \(c\) of \(M\), write \(f_*(c)\) for the configuration of \(M'\) obtained by replacing the state \(q\) of \(c\) by \(f(q)\) and keeping the input head, the work tapes, the work heads and the output (a halted configuration stays halted). Then for every configuration \(c\) of \(M\), one step of \(M'\) from \(f_*(c)\) gives \(f_*(c')\), where \(c'\) is the result of one step of \(M\) from \(c\).

theorem step (h : IsRelabelling f tm tm') (cfg : Cfg k Symbol State input) :
    tm'.step (cfg.mapState (Option.map f)) = (tm.step cfg).mapState (Option.map f)

Uses 3 · Used by 1

Statement usesSimulation up to a state relabelling

Proof usesApplying a relabelled action · Relabelling the successor state of an action

Used byLockstep runs

TheoremLockstep runs#✓fully proved

Let \(M\) and \(M'\) be multi-tape Turing machines with the same number of work tapes and the same alphabet, with state sets \(Q\) and \(Q'\), such that \(M'\) simulates \(M\) up to the state relabelling \(f : Q \to Q'\). For a configuration \(c\) of \(M\), write \(f_*(c)\) for the configuration of \(M'\) obtained by replacing the state \(q\) of \(c\) by \(f(q)\) and keeping the input head, the work tapes, the work heads and the output (a halted configuration stays halted). Then for every configuration \(c\) of \(M\) and every \(t \in \mathbb{N}\), running \(M'\) for \(t\) steps from \(f_*(c)\) gives \(f_*(c_t)\), where \(c_t\) is the configuration reached by running \(M\) for \(t\) steps from \(c\).

theorem runFrom (h : IsRelabelling f tm tm') (cfg : Cfg k Symbol State input) (t : ℕ) :
    tm'.runFrom (cfg.mapState (Option.map f)) t = (tm.runFrom cfg t).mapState (Option.map f)

Uses 2 · Used by 1

Statement usesSimulation up to a state relabelling

Proof usesRelabelled machines step in lockstep

Used byLockstep runs from the initial configuration

TheoremInitial configurations under relabelling#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for every input word \(x\), the initial configuration of \(M'\) on \(x\) is the initial configuration of \(M\) on \(x\) with its state \(q\) replaced by \(f(q)\).

theorem initCfg (h : IsRelabelling f tm tm') (x : List Symbol) :
    tm'.initCfg x = (tm.initCfg x).mapState (Option.map f)

Uses 1 · Used by 1

Statement usesSimulation up to a state relabelling

Used byLockstep runs from the initial configuration

TheoremLockstep runs from the initial configuration#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for every input word \(x\) and every \(t \in \mathbb{N}\), the configuration of \(M'\) after \(t\) steps on input \(x\) is the configuration of \(M\) after \(t\) steps on input \(x\) with its state relabelled by \(f\): a state \(q\) becomes \(f(q)\) and the halting state stays halting.

theorem runFrom_initCfg (h : IsRelabelling f tm tm') (x : List Symbol) (t : ℕ) :
    tm'.runFrom (tm'.initCfg x) t = (tm.runFrom (tm.initCfg x) t).mapState (Option.map f)

Uses 3 · Used by 3

Statement usesSimulation up to a state relabelling

Proof usesInitial configurations under relabelling · Lockstep runs

Used byRelabelling preserves what a machine computes · Relabelling preserves space bounds · Relabelling preserves time bounds

TheoremRelabelling preserves what a machine computes#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for all words \(x\) and \(o\) over the alphabet, \(M'\) started on input \(x\) eventually halts with output \(o\) if and only if \(M\) does.

theorem computes_iff (h : IsRelabelling f tm tm') {x o : List Symbol} :
    tm'.Computes x o ↔ tm.Computes x o

Uses 3 · Used by 5

Statement usesSimulation up to a state relabelling

Proof usesLockstep runs from the initial configuration · Relabelling preserves halting

Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Relabelling preserves computing a function within time and space bounds · Relabelling preserves deciding a language

TheoremRelabelling preserves time bounds#✓fully proved

Let \(M\) and \(M'\) be multi-tape Turing machines with the same number of work tapes and the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for every input \(x\) and every \(t \in \mathbb{N}\), \(M'\) runs in time \(t\) on \(x\) if and only if \(M\) runs in time \(t\) on \(x\).

theorem runsInTime_iff (h : IsRelabelling f tm tm') {x : List Symbol} {t : ℕ} :
    tm'.RunsInTime x t ↔ tm.RunsInTime x t

Uses 4 · Used by 3

Statement usesSimulation up to a state relabelling

Proof usesLockstep runs from the initial configuration · Relabelling preserves halting · Time bounds of deterministic machines

Used byRelabelling preserves computing a function within time and space bounds · Deciding by a code is finite-state decidability · Decidability over codes

TheoremRelabelling preserves space bounds#✓fully proved

Let \(M\) and \(M'\) be multi-tape Turing machines with the same number of work tapes and the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for every input \(x\) and every \(s \in \mathbb{N}\), \(M'\) runs in space \(s\) on \(x\) if and only if \(M\) runs in space \(s\) on \(x\).

theorem runsInSpace_iff (h : IsRelabelling f tm tm') {x : List Symbol} {s : ℕ} :
    tm'.RunsInSpace x s ↔ tm.RunsInSpace x s

Uses 3 · Used by 3

Statement usesSimulation up to a state relabelling

Proof usesLockstep runs from the initial configuration · Space bounds of deterministic machines

Used byRelabelling preserves computing a function within time and space bounds · Deciding by a code is finite-state decidability · Decidability over codes

TheoremRelabelling preserves computing a function within time and space bounds#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the same alphabet such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Let \(e_{\mathrm{in}}\) and \(e_{\mathrm{out}}\) be injective encodings of types \(\alpha\) and \(\beta\) as words over the alphabet, \(g : \alpha \to \beta\) a function and \(t, s : \alpha \to \mathbb{N}\) bounds. Then \(M'\) computes \(g\) with respect to these encodings in time \(t\) and space \(s\) if and only if \(M\) does. Here a machine does so when, for every \(a \in \alpha\), on input \(e_{\mathrm{in}}(a)\) it eventually halts with output \(e_{\mathrm{out}}(g(a))\), every computation path of at least \(t(a)\) steps ends halted, and every computation path visits at most \(s(a)\) work-tape cells.

theorem computesFunInTimeAndSpace_iff (h : IsRelabelling f tm tm') {α β : Type*}
    {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {g : α → β} {t s : α → ℕ} :
    tm'.ComputesFunInTimeAndSpace encIn encOut g t s ↔
      tm.ComputesFunInTimeAndSpace encIn encOut g t s

Uses 4 · Used by 2

Statement usesSimulation up to a state relabelling

Proof usesRelabelling preserves what a machine computes · Relabelling preserves space bounds · Relabelling preserves time bounds

Used byComputation by a code is finite-state computation · Computability over codes

TheoremRelabelling preserves deciding a language#✓fully proved

Let \(M\) and \(M'\) be deterministic machines with \(k\) work tapes over the alphabet \(\{\mathrm{false}, \mathrm{true}\}\) such that \(M'\) simulates \(M\) up to a state relabelling \(f\). Then for every set \(L\) of binary words, \(M'\) decides \(L\) if and only if \(M\) decides \(L\).

theorem decides_iff {tm : MultiTapeTM k Bool State} {tm' : MultiTapeTM k Bool State'}
    (h : IsRelabelling f tm tm') {L : Set (List Bool)} : Decides tm' L ↔ Decides tm L

Uses 3 · Used by 2

Statement usesA multi-tape machine deciding a language · Simulation up to a state relabelling

Proof usesRelabelling preserves what a machine computes

Used byDeciding by a code is finite-state decidability · Decidability over codes

32 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.