Basic
📁 Source: Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsSingleTapeTM, Cfg, space_used, state, Outputs, OutputsWithinTime, PolyTimeComputable, comp, id, poly, toTimeComputable, State, Stmt, movement, symbol, TimeComputable, comp, id, time_bound, tm, TransitionRelation, compComputer, haltCfg, idComputer, inhabitedStmt, initCfg, instFintypeState, instInhabitedCfg, default, instInhabitedState, instInhabitedStmt, default, q₀, stateFintype, step, tr | 36 |
| 7 | |
| Total | 43 |
Turing
Definitions
| Name | Category | Theorems |
|---|---|---|
SingleTapeTM 📖 | CompData | — |
Turing.SingleTapeTM
Definitions
| Name | Category | Theorems |
|---|---|---|
Cfg 📖 | CompData | — |
Outputs 📖 | MathDef | — |
OutputsWithinTime 📖 | MathDef | |
PolyTimeComputable 📖 | CompData | — |
State 📖 | CompOp | |
Stmt 📖 | CompData | — |
TimeComputable 📖 | CompData | — |
TransitionRelation 📖 | MathDef | — |
compComputer 📖 | CompOp | |
haltCfg 📖 | CompOp | |
idComputer 📖 | CompOp | — |
inhabitedStmt 📖 | CompOp | — |
initCfg 📖 | CompOp | |
instFintypeState 📖 | CompOp | — |
instInhabitedCfg 📖 | CompOp | — |
instInhabitedState 📖 | CompOp | — |
instInhabitedStmt 📖 | CompOp | — |
q₀ 📖 | CompOp | |
stateFintype 📖 | CompOp | — |
step 📖 | CompOp | — |
tr 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
compComputer_q₀_eq 📖 | mathematical | — | q₀compComputerState | — | — |
output_length_le_input_length_add_time 📖 | — | OutputsWithinTime | — | — | — |
Turing.SingleTapeTM.Cfg
Definitions
| Name | Category | Theorems |
|---|---|---|
space_used 📖 | CompOp | |
state 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
space_used_haltCfg 📖 | mathematical | — | space_usedTuring.SingleTapeTM.haltCfg | — | Turing.BiTape.space_used_mk₁ |
space_used_initCfg 📖 | mathematical | — | space_usedTuring.SingleTapeTM.initCfg | — | Turing.BiTape.space_used_mk₁ |
space_used_step 📖 | mathematical | Turing.SingleTapeTM.stepTuring.SingleTapeTM.Cfg | space_used | — | Turing.BiTape.space_used_writeTuring.BiTape.space_used_move |
Turing.SingleTapeTM.PolyTimeComputable
Definitions
| Name | Category | Theorems |
|---|---|---|
comp 📖 | CompOp | — |
id 📖 | CompOp | — |
poly 📖 | CompOp | |
toTimeComputable 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
bounds 📖 | mathematical | — | Turing.SingleTapeTM.TimeComputable.time_boundtoTimeComputablepoly | — | — |
Turing.SingleTapeTM.Stmt
Definitions
| Name | Category | Theorems |
|---|---|---|
movement 📖 | CompOp | — |
symbol 📖 | CompOp | — |
Turing.SingleTapeTM.TimeComputable
Definitions
| Name | Category | Theorems |
|---|---|---|
comp 📖 | CompOp | — |
id 📖 | CompOp | — |
time_bound 📖 | CompOp | |
tm 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
outputsFunInTime 📖 | mathematical | — | Turing.SingleTapeTM.OutputsWithinTimetmtime_bound | — | — |
Turing.SingleTapeTM.instInhabitedCfg
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Turing.SingleTapeTM.instInhabitedStmt
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---