Mathlib Map

Theorems · Inductive type · logic and foundations

Turing.TM1.Cfg

(Γ : Type u_1) → Type u_2 → Type u_3 → [Inhabited Γ] → Type (max (max u_1 u_2) u_3)

The configuration of a TM1 machine is given by the currently evaluating statement, the variable store value, and the tape.

Defined in
Mathlib.Computability.TuringMachine.PostTuringMachine
Cited by
20 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Inhabited
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Turing.TM1.stepAux · cited by 12TM1.stepAuxTuring.TM1.step · cited by 10TM1.stepTuring.TM2to1.TrCfg · cited by 4TM2to1.TrCfgTuring.TM1.stepAux.eq_def · cited by 3stepAux.eq_defTuring.TM1.eval · cited by 3TM1.evalTuring.TM1.init · cited by 3TM1.initTuring.TM1.Cfg.Tape · cited by 3Cfg.TapeTuring.TM2to1.trCfg_init · cited by 2TM2to1.trCfg_initTuring.TM2to1.tr_respects · cited by 2TM2to1.tr_respectsTuring.TM1to0.trCfg · cited by 2TM1to0.trCfgTuring.TM1to1.stepAux_move · cited by 2TM1to1.stepAux_moveTuring.TM1to1.trCfg · cited by 2TM1to1.trCfgTuring.TM2to1.TrCfg.casesOn · cited by 2TrCfg.casesOnTuring.TM1.Cfg.l · cited by 2Cfg.lTuring.TM0to1.trCfg · cited by 1TM0to1.trCfgTM1.CfgCITED BYCITES

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 by39

Results whose statement or proof uses this declaration.