Documentation Verification Report

StackTuringMachine

📁 Source: Mathlib/Computability/TuringMachine/StackTuringMachine.lean

Statistics

Metric	Count
Definitions `Cfg`, `inhabited`, `l`, `stk`, `var`, `Reaches`, `Stmt`, `inhabited`, `Supports`, `SupportsStmt`, `eval`, `init`, `step`, `stepAux`, `stmts`, `stmts₁`, `StAct`, `inhabited`, `TrCfg`, `addBottom`, `stRun`, `stVar`, `stWrite`, `stmtStRec`, `tr`, `trInit`, `trNormal`, `trStAct`, `trStmts₁`, `trSupp`, `Γ'`, `fintype`, `inhabited`, `Λ'`, `inhabited`	35
Theorems `step_supports`, `stmts_supportsStmt`, `stmts_trans`, `stmts₁_self`, `stmts₁_supportsStmt_mono`, `stmts₁_trans`, `addBottom_head_fst`, `addBottom_map`, `addBottom_modifyNth`, `addBottom_nth_snd`, `addBottom_nth_succ_fst`, `step_run`, `stk_nth_val`, `supports_run`, `trCfg_init`, `trNormal_run`, `trStmts₁_run`, `tr_eval`, `tr_eval_dom`, `tr_respects`, `tr_respects_aux`, `tr_respects_aux₁`, `tr_respects_aux₂`, `tr_respects_aux₃`, `tr_supports`	25
Total	60

Turing.TM2

Definitions

Name	Category	Theorems
`Cfg` 📖	CompData	15 math math: `Turing.PartrecToTM2.copy_ok`, `Turing.PartrecToTM2.move_ok`, `Turing.PartrecToTM2.head_stack_ok`, `Turing.PartrecToTM2.tr_respects`, `Turing.PartrecToTM2.tr_eval`, `Turing.PartrecToTM2.succ_ok`, `Turing.PartrecToTM2.clear_ok`, `Turing.PartrecToTM2.trNormal_respects`, `Turing.PartrecToTM2.pred_ok`, `Turing.PartrecToTM2.move₂_ok`, `Turing.PartrecToTM2.tr_ret_respects`, `Turing.PartrecToTM2.tr_init`, `Turing.PartrecToTM2.unrev_ok`, `Turing.PartrecToTM2.head_main_ok`, `Turing.TM2to1.tr_respects`
`Reaches` 📖	MathDef	—
`Stmt` 📖	CompData	3 math math: `stmts₁_self`, `stmts₁_trans`, `stmts_trans`
`Supports` 📖	MathDef	1 math math: `Turing.PartrecToTM2.tr_supports`
`SupportsStmt` 📖	MathDef	6 math math: `Turing.PartrecToTM2.ret_supports`, `stmts₁_supportsStmt_mono`, `Turing.PartrecToTM2.supports_singleton`, `Turing.TM2to1.supports_run`, `Turing.PartrecToTM2.supports_insert`, `stmts_supportsStmt`
`eval` 📖	CompOp	1 math math: `Turing.TM2to1.tr_eval_dom`
`init` 📖	CompOp	1 math math: `Turing.TM2to1.trCfg_init`
`step` 📖	CompOp	15 math math: `Turing.PartrecToTM2.copy_ok`, `Turing.PartrecToTM2.move_ok`, `Turing.PartrecToTM2.head_stack_ok`, `Turing.PartrecToTM2.tr_respects`, `Turing.PartrecToTM2.tr_eval`, `Turing.PartrecToTM2.succ_ok`, `Turing.PartrecToTM2.clear_ok`, `Turing.PartrecToTM2.trNormal_respects`, `Turing.PartrecToTM2.pred_ok`, `Turing.PartrecToTM2.move₂_ok`, `Turing.PartrecToTM2.tr_ret_respects`, `Turing.PartrecToTM2.tr_init`, `Turing.PartrecToTM2.unrev_ok`, `Turing.PartrecToTM2.head_main_ok`, `Turing.TM2to1.tr_respects`
`stepAux` 📖	CompOp	2 math math: `Turing.TM2to1.tr_respects_aux`, `Turing.TM2to1.step_run`
`stmts` 📖	CompOp	1 math math: `stmts_trans`
`stmts₁` 📖	CompOp	2 math math: `stmts₁_self`, `stmts₁_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`step_supports` 📖	mathematical	`Supports` `Cfg` `step` `Finset` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `instFunLikeOrderEmbedding` `Finset.insertNone` `Cfg.l`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `instFunLikeOrderEmbedding` `Finset.insertNone` `Cfg.l`	—	`Finset.some_mem_insertNone` `stepAux.eq_def` `Multiset.mem_cons_self`
`stmts_supportsStmt` 📖	mathematical	`Supports` `Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts`	`SupportsStmt`	—	`stmts₁_supportsStmt_mono`
`stmts_trans` 📖	mathematical	`Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts₁` `stmts`	`Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts`	—	`stmts₁_trans`
`stmts₁_self` 📖	mathematical	—	`Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts₁`	—	—
`stmts₁_supportsStmt_mono` 📖	mathematical	`Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts₁` `SupportsStmt`	`SupportsStmt`	—	—
`stmts₁_trans` 📖	mathematical	`Stmt` `Finset` `SetLike.instMembership` `Finset.instSetLike` `stmts₁`	`Finset` `Stmt` `Finset.instHasSubset` `stmts₁`	—	`stmts₁.eq_def` `Finset.mem_insert_of_mem` `Finset.mem_union_left` `Finset.mem_union_right`

Turing.TM2.Cfg

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`l` 📖	CompOp	1 math math: `Turing.TM2.step_supports`
`stk` 📖	CompOp	—
`var` 📖	CompOp	—

Turing.TM2.Stmt

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

Turing.TM2to1

Definitions

Name	Category	Theorems
`StAct` 📖	CompData	—
`TrCfg` 📖	CompData	3 math math: `tr_respects_aux`, `trCfg_init`, `tr_respects`
`addBottom` 📖	CompOp	10 math math: `addBottom_nth_succ_fst`, `tr_respects_aux`, `tr_respects_aux₁`, `addBottom_modifyNth`, `tr_respects_aux₃`, `tr_eval`, `addBottom_head_fst`, `addBottom_map`, `addBottom_nth_snd`, `tr_respects_aux₂`
`stRun` 📖	CompOp	5 math math: `tr_respects_aux`, `trStmts₁_run`, `trNormal_run`, `supports_run`, `step_run`
`stVar` 📖	CompOp	2 math math: `tr_respects_aux₂`, `step_run`
`stWrite` 📖	CompOp	2 math math: `tr_respects_aux₂`, `step_run`
`stmtStRec` 📖	CompOp	—
`tr` 📖	CompOp	6 math math: `tr_respects_aux`, `tr_respects_aux₁`, `tr_respects_aux₃`, `tr_eval_dom`, `tr_supports`, `tr_respects`
`trInit` 📖	CompOp	2 math math: `tr_eval_dom`, `trCfg_init`
`trNormal` 📖	CompOp	2 math math: `tr_respects_aux`, `trNormal_run`
`trStAct` 📖	CompOp	1 math math: `tr_respects_aux₂`
`trStmts₁` 📖	CompOp	1 math math: `trStmts₁_run`
`trSupp` 📖	CompOp	1 math math: `tr_supports`
`Γ'` 📖	CompOp	12 math math: `addBottom_nth_succ_fst`, `tr_respects_aux`, `tr_respects_aux₁`, `trNormal_run`, `tr_respects_aux₃`, `addBottom_head_fst`, `tr_eval_dom`, `addBottom_nth_snd`, `tr_respects_aux₂`, `trCfg_init`, `tr_supports`, `tr_respects`
`Λ'` 📖	CompData	10 math math: `tr_respects_aux`, `tr_respects_aux₁`, `trStmts₁_run`, `trNormal_run`, `tr_respects_aux₃`, `tr_eval_dom`, `tr_respects_aux₂`, `trCfg_init`, `tr_supports`, `tr_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addBottom_head_fst` 📖	mathematical	—	`Turing.ListBlank.head` `Γ'` `Γ'.inhabited` `addBottom`	—	`addBottom.eq_1` `Turing.ListBlank.head_cons`
`addBottom_map` 📖	mathematical	—	`Turing.ListBlank.map` `Γ'.inhabited` `addBottom`	—	`Turing.ListBlank.map_cons` `Turing.ListBlank.induction_on` `Turing.ListBlank.cons_head_tail`
`addBottom_modifyNth` 📖	mathematical	—	`Turing.ListBlank.modifyNth` `Γ'.inhabited` `addBottom`	—	`Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons` `Turing.ListBlank.map_modifyNth`
`addBottom_nth_snd` 📖	mathematical	—	`Turing.ListBlank.nth` `Γ'` `Γ'.inhabited` `addBottom`	—	`addBottom_map` `Turing.ListBlank.nth_map`
`addBottom_nth_succ_fst` 📖	mathematical	—	`Turing.ListBlank.nth` `Γ'` `Γ'.inhabited` `addBottom`	—	`Turing.ListBlank.nth_succ` `addBottom.eq_1` `Turing.ListBlank.tail_cons` `Turing.ListBlank.nth_map`
`step_run` 📖	mathematical	—	`Turing.TM2.stepAux` `stRun` `stVar` `Function.update` `stWrite`	—	`Function.update_eq_self`
`stk_nth_val` 📖	mathematical	`Turing.ListBlank.map` `Turing.proj`	`Turing.ListBlank.nth`	—	`Turing.proj_map_nth` `List.getI_eq_getElem?_getD`
`supports_run` 📖	mathematical	—	`Turing.TM2.SupportsStmt` `stRun`	—	—
`trCfg_init` 📖	mathematical	—	`TrCfg` `Turing.TM2.init` `Turing.TM1.init` `Γ'` `Λ'` `Λ'.inhabited` `Γ'.inhabited` `trInit`	—	`trInit.eq_1` `Turing.TM1.init.eq_1` `Turing.ListBlank.ext` `List.getI_eq_getElem?_getD` `Turing.proj.eq_1` `Turing.PointedMap.mk_val` `Function.update_self` `Function.update_of_ne`
`trNormal_run` 📖	mathematical	—	`trNormal` `stRun` `Turing.TM1.Stmt.goto` `Γ'` `Λ'` `Λ'.go`	—	—
`trStmts₁_run` 📖	mathematical	—	`trStmts₁` `stRun` `Finset` `Λ'` `Finset.instUnion` `Finset.instInsert` `Λ'.go` `Finset.instSingleton` `Λ'.ret`	—	—
`tr_eval` 📖	mathematical	`Turing.ListBlank` `Γ'` `Γ'.inhabited` `Part` `Part.instMembership` `Turing.TM1.eval` `Λ'` `Λ'.inhabited` `tr` `trInit` `Turing.TM2.eval`	`Turing.ListBlank` `addBottom` `Turing.ListBlank.map` `Turing.proj`	—	`Part.mem_map_iff` `StateTransition.tr_eval` `tr_respects` `trCfg_init` `Part.mem_unique` `Turing.Tape.mk'_right₀`
`tr_eval_dom` 📖	mathematical	—	`Part.Dom` `Turing.ListBlank` `Γ'` `Γ'.inhabited` `Turing.TM1.eval` `Λ'` `Λ'.inhabited` `tr` `trInit` `Turing.TM2.eval`	—	`StateTransition.tr_eval_dom` `tr_respects` `trCfg_init`
`tr_respects` 📖	mathematical	—	`StateTransition.Respects` `Turing.TM2.Cfg` `Turing.TM1.Cfg` `Γ'` `Λ'` `Γ'.inhabited` `Turing.TM2.step` `Turing.TM1.step` `tr` `TrCfg`	—	`tr_respects_aux` `Turing.TM2.stepAux.eq_def` `trNormal.eq_def` `Turing.TM1.stepAux.eq_def` `Relation.TransGen.head'`
`tr_respects_aux` 📖	mathematical	`Turing.ListBlank.map` `Turing.proj` `Turing.TM1.Cfg` `Γ'` `Λ'` `Γ'.inhabited` `TrCfg` `Turing.TM2.stepAux` `StateTransition.Reaches` `Turing.TM1.step` `tr` `Turing.TM1.stepAux` `trNormal` `Turing.Tape.mk'` `Turing.ListBlank` `Turing.ListBlank.hasEmptyc` `addBottom`	`Turing.TM1.Cfg` `Γ'` `Λ'` `Γ'.inhabited` `TrCfg` `Turing.TM2.stepAux` `stRun` `StateTransition.Reaches` `Turing.TM1.step` `tr` `Turing.TM1.stepAux` `trNormal` `Turing.Tape.mk'` `Turing.ListBlank` `Turing.ListBlank.hasEmptyc` `addBottom`	—	`step_run` `trNormal_run` `tr_respects_aux₁` `le_rfl` `tr_respects_aux₂` `StateTransition.Reaches₀.tail'` `Relation.TransGen.to_reflTransGen` `StateTransition.Reaches₀.trans` `StateTransition.Reaches₁.to₀` `Turing.TM1.stepAux.eq_5` `Option.isNone.eq_2` `le_of_eq` `stk_nth_val` `addBottom_nth_snd` `Turing.Tape.mk'_nth_nat` `Turing.Tape.move_right_n_head` `Turing.TM1.stepAux.eq_4` `tr.eq_2` `tr_respects_aux₃` `Relation.TransGen.head'` `tr.eq_3` `Turing.Tape.mk'_head` `addBottom_head_fst`
`tr_respects_aux₁` 📖	mathematical	`Turing.ListBlank.map` `Turing.proj`	`StateTransition.Reaches₀` `Turing.TM1.Cfg` `Γ'` `Λ'` `Γ'.inhabited` `Turing.TM1.step` `tr` `Λ'.go` `Turing.Tape.mk'` `Turing.ListBlank` `Turing.ListBlank.hasEmptyc` `addBottom` `Nat.iterate` `Turing.Tape` `Turing.Tape.move` `Turing.Dir.right`	—	`StateTransition.Reaches₀.refl` `StateTransition.Reaches₀.tail` `le_of_lt` `Function.iterate_succ_apply'` `Turing.Tape.move_right_n_head` `Turing.Tape.mk'_nth_nat` `addBottom_nth_snd` `stk_nth_val`
`tr_respects_aux₂` 📖	mathematical	`Turing.ListBlank.map` `Turing.proj`	`Turing.ListBlank` `Turing.ListBlank.map` `Turing.proj` `Function.update` `stWrite` `Turing.TM1.stepAux` `Γ'` `Λ'` `Γ'.inhabited` `trStAct` `Nat.iterate` `Turing.Tape` `Turing.Tape.move` `Turing.Dir.right` `Turing.Tape.mk'` `Turing.ListBlank.hasEmptyc` `addBottom` `stVar`	—	`Function.update_self` `Turing.Tape.write_move_right_n` `Turing.ListBlank.ext` `Turing.ListBlank.nth_map` `Turing.ListBlank.nth_modifyNth` `Turing.proj.eq_1` `Turing.PointedMap.mk_val` `List.getI_eq_getElem` `Turing.proj_map_nth` `lt_or_gt_of_ne` `List.getI_append` `List.getI_eq_default` `Function.update_of_ne` `Turing.Tape.move_right_n_head` `Turing.Tape.mk'_nth_nat` `addBottom_modifyNth` `Function.iterate_succ'` `Function.update_eq_self` `Turing.Tape.move_left_right` `Turing.Tape.move_right_left` `addBottom_nth_snd` `stk_nth_val` `Turing.Tape.move_left_mk'` `Turing.ListBlank.head_cons` `Turing.Tape.write_mk'` `addBottom_head_fst` `le_refl` `addBottom_nth_succ_fst` `List.head?.eq_2` `List.tail.eq_2`
`tr_respects_aux₃` 📖	mathematical	—	`StateTransition.Reaches₀` `Turing.TM1.Cfg` `Γ'` `Λ'` `Γ'.inhabited` `Turing.TM1.step` `tr` `Λ'.ret` `Nat.iterate` `Turing.Tape` `Turing.Tape.move` `Turing.Dir.right` `Turing.Tape.mk'` `Turing.ListBlank` `Turing.ListBlank.hasEmptyc` `addBottom`	—	`StateTransition.Reaches₀.refl` `StateTransition.Reaches₀.head` `tr.eq_3` `Turing.TM1.stepAux.eq_4` `Turing.Tape.move_right_n_head` `Turing.Tape.mk'_nth_nat` `addBottom_nth_succ_fst` `Turing.TM1.stepAux.eq_1` `Function.iterate_succ'` `Turing.Tape.move_right_left`
`tr_supports` 📖	mathematical	`Turing.TM2.Supports`	`Turing.TM1.Supports` `Γ'` `Λ'` `Λ'.inhabited` `tr` `trSupp`	—	`Finset.mem_biUnion` `Finset.mem_insert` `trStmts₁_run` `supports_run` `trNormal_run` `Turing.TM1.SupportsStmt.eq_def` `trStmts₁.eq_def` `Finset.mem_union_left` `Finset.mem_union_right` `Finset.mem_union` `trStmts₁.eq_5` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`

Turing.TM2to1.StAct

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

Turing.TM2to1.Γ'

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	—
`inhabited` 📖	CompOp	12 math math: `Turing.TM2to1.addBottom_nth_succ_fst`, `Turing.TM2to1.tr_respects_aux`, `Turing.TM2to1.tr_respects_aux₁`, `Turing.TM2to1.addBottom_modifyNth`, `Turing.TM2to1.tr_respects_aux₃`, `Turing.TM2to1.addBottom_head_fst`, `Turing.TM2to1.addBottom_map`, `Turing.TM2to1.tr_eval_dom`, `Turing.TM2to1.addBottom_nth_snd`, `Turing.TM2to1.tr_respects_aux₂`, `Turing.TM2to1.trCfg_init`, `Turing.TM2to1.tr_respects`

Turing.TM2to1.Λ'

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	3 math math: `Turing.TM2to1.tr_eval_dom`, `Turing.TM2to1.trCfg_init`, `Turing.TM2to1.tr_supports`

---

← Back to Index