Documentation Verification Report

PostTuringMachine

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

Statistics

Metric	Count
Definitions `Cfg`, `inhabited`, `map`, `q`, `Machine`, `map`, `Reaches`, `Stmt`, `inhabited`, `map`, `Supports`, `eval`, `init`, `instInhabitedMachine`, `step`, `instInhabitedΛ'`, `tr`, `trCfg`, `Λ'`, `Cfg`, `inhabited`, `l`, `var`, `Stmt`, `inhabited`, `Supports`, `SupportsStmt`, `eval`, `init`, `step`, `stepAux`, `stmts`, `stmts₁`, `instInhabitedΛ'`, `tr`, `trAux`, `trCfg`, `trStmts`, `Λ'`, `instInhabitedΛ'`, `move`, `read`, `readAux`, `tr`, `trCfg`, `trNormal`, `trSupp`, `trTape`, `trTape'`, `write`, `writes`, `Λ'`	52
Theorems `map_respects`, `map_step`, `map_init`, `step_supports`, `univ_supports`, `tr_respects`, `step_supports`, `stmts_supportsStmt`, `stmts_trans`, `stmts₁_self`, `stmts₁_supportsStmt_mono`, `stmts₁_trans`, `tr_eval`, `tr_respects`, `tr_supports`, `exists_enc_dec`, `stepAux_move`, `stepAux_read`, `stepAux_write`, `supportsStmt_move`, `supportsStmt_read`, `supportsStmt_write`, `trTape'_move_left`, `trTape'_move_right`, `trTape_mk'`, `tr_respects`, `tr_supports`	27
Total	79

Turing.TM0

Definitions

Name	Category	Theorems
`Cfg` 📖	CompData	4 math math: `Turing.TM0to1.tr_respects`, `Machine.map_step`, `Turing.TM1to0.tr_respects`, `Machine.map_respects`
`Machine` 📖	CompOp	—
`Reaches` 📖	MathDef	—
`Stmt` 📖	CompData	—
`Supports` 📖	MathDef	2 math math: `univ_supports`, `Turing.TM1to0.tr_supports`
`eval` 📖	CompOp	1 math math: `Turing.TM1to0.tr_eval`
`init` 📖	CompOp	1 math math: `map_init`
`instInhabitedMachine` 📖	CompOp	—
`step` 📖	CompOp	4 math math: `Turing.TM0to1.tr_respects`, `Machine.map_step`, `Turing.TM1to0.tr_respects`, `Machine.map_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_init` 📖	mathematical	—	`Cfg.map` `Turing.PointedMap.f` `init`	—	`Turing.PointedMap.map_pt` `Turing.Tape.map_mk₁`
`step_supports` 📖	mathematical	`Supports` `Cfg` `step` `Set` `Set.instMembership` `Cfg.q`	`Set` `Set.instMembership` `Cfg.q`	—	—
`univ_supports` 📖	mathematical	—	`Supports` `Set.univ`	—	`Set.mem_univ`

Turing.TM0.Cfg

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `Turing.TM0.map_init`, `Turing.TM0.Machine.map_step`, `Turing.TM0.Machine.map_respects`
`q` 📖	CompOp	2 math math: `Turing.TM0.step_supports`, `Turing.TM0.Machine.map_respects`

Turing.TM0.Machine

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `map_step`, `map_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_respects` 📖	mathematical	`Turing.TM0.Supports` `Turing.PointedMap.f`	`StateTransition.Respects` `Turing.TM0.Cfg` `Turing.TM0.step` `map` `Turing.PointedMap.f` `Set` `Set.instMembership` `Turing.TM0.Cfg.q` `Turing.TM0.Cfg.map`	—	`map_step` `Turing.TM0.step_supports`
`map_step` 📖	mathematical	`Turing.PointedMap.f` `Set` `Set.instMembership` `Turing.TM0.Cfg.q`	`Turing.TM0.Cfg` `Turing.TM0.Cfg.map` `Turing.TM0.step` `map`	—	`Turing.Tape.map_fst` `Turing.Tape.map_move` `Turing.Tape.map_write`

Turing.TM0.Stmt

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`map` 📖	CompOp	—

Turing.TM0to1

Definitions

Name	Category	Theorems
`instInhabitedΛ'` 📖	CompOp	—
`tr` 📖	CompOp	1 math math: `tr_respects`
`trCfg` 📖	CompOp	1 math math: `tr_respects`
`Λ'` 📖	CompData	1 math math: `tr_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tr_respects` 📖	mathematical	—	`StateTransition.Respects` `Turing.TM0.Cfg` `Turing.TM1.Cfg` `Λ'` `Turing.TM0.step` `Turing.TM1.step` `tr` `trCfg`	—	`StateTransition.fun_respects` `Relation.TransGen.head` `Relation.TransGen.head'` `Relation.ReflTransGen.single`

Turing.TM1

Definitions

Name	Category	Theorems
`Cfg` 📖	CompData	7 math math: `Turing.TM2to1.tr_respects_aux`, `Turing.TM2to1.tr_respects_aux₁`, `Turing.TM2to1.tr_respects_aux₃`, `Turing.TM0to1.tr_respects`, `Turing.TM1to1.tr_respects`, `Turing.TM1to0.tr_respects`, `Turing.TM2to1.tr_respects`
`Stmt` 📖	CompData	3 math math: `stmts₁_trans`, `stmts₁_self`, `stmts_trans`
`Supports` 📖	MathDef	2 math math: `Turing.TM1to1.tr_supports`, `Turing.TM2to1.tr_supports`
`SupportsStmt` 📖	MathDef	5 math math: `Turing.TM1to1.supportsStmt_read`, `stmts₁_supportsStmt_mono`, `Turing.TM1to1.supportsStmt_write`, `Turing.TM1to1.supportsStmt_move`, `stmts_supportsStmt`
`eval` 📖	CompOp	2 math math: `Turing.TM1to0.tr_eval`, `Turing.TM2to1.tr_eval_dom`
`init` 📖	CompOp	1 math math: `Turing.TM2to1.trCfg_init`
`step` 📖	CompOp	7 math math: `Turing.TM2to1.tr_respects_aux`, `Turing.TM2to1.tr_respects_aux₁`, `Turing.TM2to1.tr_respects_aux₃`, `Turing.TM0to1.tr_respects`, `Turing.TM1to1.tr_respects`, `Turing.TM1to0.tr_respects`, `Turing.TM2to1.tr_respects`
`stepAux` 📖	CompOp	5 math math: `Turing.TM2to1.tr_respects_aux`, `Turing.TM1to1.stepAux_write`, `Turing.TM1to1.stepAux_read`, `Turing.TM1to1.stepAux_move`, `Turing.TM2to1.tr_respects_aux₂`
`stmts` 📖	CompOp	1 math math: `stmts_trans`
`stmts₁` 📖	CompOp	2 math math: `stmts₁_trans`, `stmts₁_self`

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`

Turing.TM1.Cfg

Definitions

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

Turing.TM1.Stmt

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

Turing.TM1to0

Definitions

Name	Category	Theorems
`instInhabitedΛ'` 📖	CompOp	3 math math: `tr_eval`, `tr_supports`, `tr_respects`
`tr` 📖	CompOp	3 math math: `tr_eval`, `tr_supports`, `tr_respects`
`trAux` 📖	CompOp	—
`trCfg` 📖	CompOp	1 math math: `tr_respects`
`trStmts` 📖	CompOp	1 math math: `tr_supports`
`Λ'` 📖	CompOp	3 math math: `tr_eval`, `tr_supports`, `tr_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tr_eval` 📖	mathematical	—	`Turing.TM0.eval` `Λ'` `instInhabitedΛ'` `tr` `Turing.TM1.eval`	—	`StateTransition.tr_eval'` `tr_respects` `Part.map_eq_map` `Part.map_map` `Turing.TM1.eval.eq_1`
`tr_respects` 📖	mathematical	—	`StateTransition.Respects` `Turing.TM1.Cfg` `Turing.TM0.Cfg` `Λ'` `Turing.TM1.step` `Turing.TM0.step` `instInhabitedΛ'` `tr` `trCfg`	—	`StateTransition.fun_respects` `Relation.TransGen.head` `StateTransition.reaches₁_eq` `Turing.TM1.stepAux.eq_def` `Turing.Tape.write_self`
`tr_supports` 📖	mathematical	`Turing.TM1.Supports`	`Turing.TM0.Supports` `Λ'` `instInhabitedΛ'` `tr` `SetLike.coe` `Finset` `Finset.instSetLike` `trStmts`	—	`Finset.mem_product` `Turing.TM1.stmts₁_self` `Finset.mem_univ` `Multiset.mem_cons_self` `Turing.TM1.stmts_supportsStmt` `Turing.TM1.stmts_trans` `Turing.TM1.stmts₁.eq_def` `Finset.mem_insert_of_mem` `Finset.mem_union_right` `trAux.eq_4` `Finset.mem_union_left` `Finset.some_mem_insertNone` `Finset.mem_biUnion`

Turing.TM1to1

Definitions

Name	Category	Theorems
`instInhabitedΛ'` 📖	CompOp	1 math math: `tr_supports`
`move` 📖	CompOp	2 math math: `supportsStmt_move`, `stepAux_move`
`read` 📖	CompOp	2 math math: `stepAux_read`, `supportsStmt_read`
`readAux` 📖	CompOp	—
`tr` 📖	CompOp	2 math math: `tr_respects`, `tr_supports`
`trCfg` 📖	CompOp	1 math math: `tr_respects`
`trNormal` 📖	CompOp	—
`trSupp` 📖	CompOp	1 math math: `tr_supports`
`trTape` 📖	CompOp	1 math math: `trTape_mk'`
`trTape'` 📖	CompOp	5 math math: `trTape_mk'`, `stepAux_write`, `stepAux_read`, `trTape'_move_left`, `trTape'_move_right`
`write` 📖	CompOp	2 math math: `stepAux_write`, `supportsStmt_write`
`writes` 📖	CompOp	—
`Λ'` 📖	CompData	8 math math: `stepAux_write`, `stepAux_read`, `supportsStmt_read`, `tr_respects`, `supportsStmt_write`, `supportsStmt_move`, `stepAux_move`, `tr_supports`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_enc_dec` 📖	mathematical	—	`List.Vector.replicate`	—	`Finite.exists_equiv_fin` `Bool.of_decide_true` `Bool.decide_true` `Function.Embedding.setValue_eq` `Function.leftInverse_invFun` `Function.Embedding.inj'`
`stepAux_move` 📖	mathematical	—	`Turing.TM1.stepAux` `Λ'` `move` `Nat.iterate` `Turing.Tape` `Turing.Tape.move`	—	`Function.iterate_succ'` `Function.iterate_succ`
`stepAux_read` 📖	mathematical	`List.Vector.replicate`	`Turing.TM1.stepAux` `Λ'` `read` `trTape'` `Turing.ListBlank.head`	—	`Turing.ListBlank.exists_cons` `Turing.ListBlank.cons_flatMap` `Turing.ListBlank.head_cons` `Turing.ListBlank.flatMap.congr_simp` `Turing.ListBlank.tail_cons` `Turing.Tape.move_right_mk'` `Turing.ListBlank.append.eq_2` `read.eq_1` `stepAux_move` `trTape'_move_left` `trTape'.congr_simp` `Turing.ListBlank.cons_head_tail`
`stepAux_write` 📖	mathematical	`List.Vector.replicate`	`Turing.TM1.stepAux` `Λ'` `write` `List.Vector.toList` `trTape'` `Turing.ListBlank.cons`	—	`Turing.ListBlank.cons_flatMap` `Turing.Tape.write_mk'` `Turing.ListBlank.tail_cons` `Turing.Tape.move_right_mk'` `Turing.ListBlank.head_cons`
`supportsStmt_move` 📖	mathematical	—	`Turing.TM1.SupportsStmt` `Λ'` `move`	—	—
`supportsStmt_read` 📖	mathematical	`Turing.TM1.SupportsStmt` `Λ'`	`Turing.TM1.SupportsStmt` `Λ'` `read`	—	`supportsStmt_move`
`supportsStmt_write` 📖	mathematical	—	`Turing.TM1.SupportsStmt` `Λ'` `write`	—	—
`trTape'_move_left` 📖	mathematical	`List.Vector.replicate`	`Nat.iterate` `Turing.Tape` `Turing.Tape.move` `Turing.Dir.left` `trTape'` `Turing.ListBlank.tail` `Turing.ListBlank.cons` `Turing.ListBlank.head`	—	`Turing.ListBlank.exists_cons` `Turing.ListBlank.cons_flatMap` `Turing.ListBlank.flatMap.congr_simp` `Turing.ListBlank.tail_cons` `Turing.ListBlank.head_cons` `Turing.Tape.move_left_mk'` `List.Vector.toList_length`
`trTape'_move_right` 📖	mathematical	`List.Vector.replicate`	`Nat.iterate` `Turing.Tape` `Turing.Tape.move` `Turing.Dir.right` `trTape'` `Turing.ListBlank.cons` `Turing.ListBlank.head` `Turing.ListBlank.tail`	—	`Function.iterate_succ_apply` `Function.iterate_succ_apply'` `Turing.Tape.move_left_right` `trTape'_move_left` `trTape'.congr_simp` `Turing.ListBlank.tail_cons` `Turing.ListBlank.head_cons` `Turing.ListBlank.cons_head_tail`
`trTape_mk'` 📖	mathematical	`List.Vector.replicate`	`trTape` `Turing.Tape.mk'` `trTape'`	—	`trTape'.congr_simp` `Turing.Tape.mk'_right₀`
`tr_respects` 📖	mathematical	`List.Vector.replicate`	`StateTransition.Respects` `Turing.TM1.Cfg` `Λ'` `Turing.TM1.step` `tr` `trCfg`	—	`StateTransition.fun_respects` `Turing.Tape.exists_mk'` `stepAux_move` `trTape'_move_left` `trCfg.congr_simp` `Turing.Tape.move_left_mk'` `trTape'_move_right` `stepAux_read` `Relation.ReflTransGen.head` `Turing.ListBlank.exists_cons` `tr.eq_2` `Turing.Tape.mk'_head` `stepAux_write` `Turing.ListBlank.head_cons` `trTape'.congr_simp` `Turing.ListBlank.tail_cons` `Turing.Tape.write_mk'` `trTape_mk'` `Relation.TransGen.head'`
`tr_supports` 📖	mathematical	`Turing.TM1.Supports`	`Turing.TM1.Supports` `Λ'` `instInhabitedΛ'` `tr` `trSupp`	—	`Finset.mem_biUnion` `Finset.mem_insert_self` `writes.eq_def` `supportsStmt_move` `supportsStmt_read` `supportsStmt_write` `Finset.mem_insert_of_mem` `Finset.mem_insert`

---

← Back to Index