Mathlib Map

Theorems · Inductive type · logic and foundations

Turing.TM0.Stmt

Type u_1 → Type u_1

A Turing machine "statement" is just a command to either move left or right, or write a symbol on the tape.

Defined in
Mathlib.Computability.TuringMachine.PostTuringMachine
Cited by
16 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Turing.TM0.step · cited by 6TM0.stepTuring.TM0.Machine · cited by 5TM0.MachineTuring.TM0.Supports · cited by 4TM0.SupportsTuring.TM1to0.tr · cited by 3TM1to0.trTuring.TM1to0.trAux · cited by 3TM1to0.trAuxTuring.TM0.Machine.map · cited by 2Machine.mapTuring.TM0.Stmt.casesOn · cited by 2Stmt.casesOnTuring.TM0.step_supports · cited by 1TM0.step_supportsTuring.TM0to1.tr · cited by 1TM0to1.trTuring.TM1to0.tr_respects · cited by 1TM1to0.tr_respectsTuring.TM0.Machine.map_step · cited by 1Machine.map_stepTuring.TM0.Stmt.map · cited by 1Stmt.mapTuring.TM0.Stmt.move.inj · cited by 1move.injTuring.TM0.Stmt.move.noConfusion · cited by 1move.noConfusionTuring.TM0.Stmt.write.inj · cited by 1write.injTM0.StmtCITED 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 by44

Results whose statement or proof uses this declaration.