Documentation Verification Report

TMComputable

πŸ“ Source: Mathlib/Computability/TMComputable.lean

Statistics

MetricCount
DefinitionsEvalsTo, refl, steps, trans, EvalsToInTime, refl, toEvalsTo, trans, FinTM2, Cfg, K, Stmt, decidableEqK, inhabitedCfg, inhabitedStmt, inhabitedΟƒ, initialState, kDecidableEq, kFin, kβ‚€, k₁, m, main, step, Ξ“, Ξ“kβ‚€Fin, Ξ›, Ξ›Fin, Οƒ, ΟƒFin, TM2Computable, outputsFun, toTM2ComputableAux, TM2ComputableAux, inputAlphabet, outputAlphabet, tm, TM2ComputableInPolyTime, outputsFun, time, toTM2ComputableAux, toTM2ComputableInTime, TM2ComputableInTime, outputsFun, time, toTM2Computable, toTM2ComputableAux, TM2Outputs, TM2OutputsInTime, toTM2Outputs, haltList, idComputable, idComputableInPolyTime, idComputableInTime, idComputer, inhabitedEvalsToInTime, inhabitedFinTM2, inhabitedTM2Computable, inhabitedTM2ComputableAux, inhabitedTM2ComputableInPolyTime, inhabitedTM2ComputableInTime, inhabitedTM2EvalsTo, inhabitedTM2Outputs, inhabitedTM2OutputsInTime, initList
65
Theoremsevals_in_steps, steps_le_m
2
Total67

Turing

Definitions

NameCategoryTheorems
EvalsTo πŸ“–CompDataβ€”
EvalsToInTime πŸ“–CompDataβ€”
FinTM2 πŸ“–CompDataβ€”
TM2Computable πŸ“–CompDataβ€”
TM2ComputableAux πŸ“–CompDataβ€”
TM2ComputableInPolyTime πŸ“–CompDataβ€”
TM2ComputableInTime πŸ“–CompDataβ€”
TM2Outputs πŸ“–CompOpβ€”
TM2OutputsInTime πŸ“–CompOpβ€”
haltList πŸ“–CompOpβ€”
idComputable πŸ“–CompOpβ€”
idComputableInPolyTime πŸ“–CompOpβ€”
idComputableInTime πŸ“–CompOpβ€”
idComputer πŸ“–CompOpβ€”
inhabitedEvalsToInTime πŸ“–CompOpβ€”
inhabitedFinTM2 πŸ“–CompOpβ€”
inhabitedTM2Computable πŸ“–CompOpβ€”
inhabitedTM2ComputableAux πŸ“–CompOpβ€”
inhabitedTM2ComputableInPolyTime πŸ“–CompOpβ€”
inhabitedTM2ComputableInTime πŸ“–CompOpβ€”
inhabitedTM2EvalsTo πŸ“–CompOpβ€”
inhabitedTM2Outputs πŸ“–CompOpβ€”
inhabitedTM2OutputsInTime πŸ“–CompOpβ€”
initList πŸ“–CompOpβ€”

Turing.EvalsTo

Definitions

NameCategoryTheorems
refl πŸ“–CompOpβ€”
steps πŸ“–CompOp
2 mathmath: Turing.EvalsToInTime.steps_le_m, evals_in_steps
trans πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
evals_in_steps πŸ“–mathematicalβ€”Nat.iterate
steps		β€”β€”

Turing.EvalsToInTime

Definitions

NameCategoryTheorems
refl πŸ“–CompOpβ€”
toEvalsTo πŸ“–CompOp
1 mathmath: steps_le_m
trans πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
steps_le_m πŸ“–mathematicalβ€”Turing.EvalsTo.steps
toEvalsTo		β€”β€”

Turing.FinTM2

Definitions

NameCategoryTheorems
Cfg πŸ“–CompOpβ€”
K πŸ“–CompOpβ€”
Stmt πŸ“–CompOpβ€”
decidableEqK πŸ“–CompOpβ€”
inhabitedCfg πŸ“–CompOpβ€”
inhabitedStmt πŸ“–CompOpβ€”
inhabitedΟƒ πŸ“–CompOpβ€”
initialState πŸ“–CompOpβ€”
kDecidableEq πŸ“–CompOpβ€”
kFin πŸ“–CompOpβ€”
kβ‚€ πŸ“–CompOpβ€”
k₁ πŸ“–CompOpβ€”
m πŸ“–CompOpβ€”
main πŸ“–CompOpβ€”
step πŸ“–CompOpβ€”
Ξ“ πŸ“–CompOpβ€”
Ξ“kβ‚€Fin πŸ“–CompOpβ€”
Ξ› πŸ“–CompOpβ€”
Ξ›Fin πŸ“–CompOpβ€”
Οƒ πŸ“–CompOpβ€”
ΟƒFin πŸ“–CompOpβ€”

Turing.TM2Computable

Definitions

NameCategoryTheorems
outputsFun πŸ“–CompOpβ€”
toTM2ComputableAux πŸ“–CompOpβ€”

Turing.TM2ComputableAux

Definitions

NameCategoryTheorems
inputAlphabet πŸ“–CompOpβ€”
outputAlphabet πŸ“–CompOpβ€”
tm πŸ“–CompOpβ€”

Turing.TM2ComputableInPolyTime

Definitions

NameCategoryTheorems
outputsFun πŸ“–CompOpβ€”
time πŸ“–CompOpβ€”
toTM2ComputableAux πŸ“–CompOpβ€”
toTM2ComputableInTime πŸ“–CompOpβ€”

Turing.TM2ComputableInTime

Definitions

NameCategoryTheorems
outputsFun πŸ“–CompOpβ€”
time πŸ“–CompOpβ€”
toTM2Computable πŸ“–CompOpβ€”
toTM2ComputableAux πŸ“–CompOpβ€”

Turing.TM2OutputsInTime

Definitions

NameCategoryTheorems
toTM2Outputs πŸ“–CompOpβ€”

---

← Back to Index