Theorems · Inductive type · logic and foundations
Turing.TM0.Cfg
(Γ : Type u_1) → Type u_2 → [Inhabited Γ] → Type (max u_1 u_2)
The configuration state of a Turing machine during operation
consists of a label (machine state), and a tape.
The tape is represented in the form (a, L, R), meaning the tape looks like L.rev ++ [a] ++ R
with the machine currently reading the a. The lists are
automatically extended with blanks as the machine moves around.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Inhabited
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by25
Results whose statement or proof uses this declaration.
- Turing.TM0.stepstatement and proof · cited by 6
- Turing.TM0.Cfg.mapstatement and proof · cited by 3
- Turing.TM0.Cfg.qstatement and proof · cited by 3
- Turing.TM0.Cfg.Tapestatement and proof · cited by 2
- Turing.TM1to0.trCfgstatement and proof · cited by 2
- Turing.TM0.evalproof · cited by 1
- Turing.TM0.initstatement · cited by 1
- Turing.TM0.step_supportsstatement and proof · cited by 1
- Turing.TM0to1.trCfgstatement and proof · cited by 1
- Turing.TM1to0.tr_respectsstatement · cited by 1
- Turing.TM0.Machine.map_stepstatement and proof · cited by 1
- Turing.TM0.Cfg.mk.injstatement · cited by 1