Documentation Verification Report

PostTuringMachine

📁 Source: Mathlib/Computability/PostTuringMachine.lean

Statistics

Metric	Count
Definitions `FRespects`, `Reaches`, `Reaches₀`, `Reaches₁`, `Respects`, `Cfg`, `inhabited`, `map`, `q`, `Machine`, `inhabited`, `map`, `Reaches`, `Stmt`, `inhabited`, `map`, `Supports`, `eval`, `init`, `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`, `Λ'`, `eval`, `evalInduction`	59
Theorems `to₀`, `head`, `refl`, `single`, `tail`, `tail'`, `trans`, `to₀`, `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`, `eval_maximal`, `eval_maximal₁`, `frespects_eq`, `fun_respects`, `mem_eval`, `reaches_eval`, `reaches_total`, `reaches₀_eq`, `reaches₁_eq`, `reaches₁_fwd`, `tr_eval`, `tr_eval'`, `tr_eval_dom`, `tr_eval_rev`, `tr_reaches`, `tr_reaches_rev`, `tr_reaches₁`	52
Total	111

Turing

Definitions

Name	Category	Theorems
`FRespects` 📖	MathDef	2 math math: `frespects_eq`, `fun_respects`
`Reaches` 📖	MathDef	3 math math: `mem_eval`, `eval_maximal`, `reaches₁_fwd`
`Reaches₀` 📖	MathDef	7 math math: `TM2to1.tr_respects_aux₁`, `reaches₀_eq`, `TM2to1.tr_respects_aux₃`, `Reaches₀.refl`, `Reaches₁.to₀`, `Reaches.to₀`, `Reaches₀.single`
`Reaches₁` 📖	MathDef	15 math math: `PartrecToTM2.copy_ok`, `eval_maximal₁`, `PartrecToTM2.move_ok`, `PartrecToTM2.head_stack_ok`, `reaches₁_eq`, `PartrecToTM2.succ_ok`, `PartrecToTM2.clear_ok`, `PartrecToTM2.trNormal_respects`, `PartrecToTM2.pred_ok`, `PartrecToTM2.move₂_ok`, `PartrecToTM2.tr_ret_respects`, `PartrecToTM2.tr_init`, `Reaches₀.tail'`, `PartrecToTM2.unrev_ok`, `PartrecToTM2.head_main_ok`
`Respects` 📖	MathDef	7 math math: `TM0to1.tr_respects`, `PartrecToTM2.tr_respects`, `TM1to1.tr_respects`, `fun_respects`, `TM1to0.tr_respects`, `TM0.Machine.map_respects`, `TM2to1.tr_respects`
`eval` 📖	CompOp	9 math math: `tr_eval_dom`, `tr_eval'`, `ToPartrec.stepNormal_eval`, `reaches_eval`, `mem_eval`, `ToPartrec.stepRet_eval`, `ToPartrec.cont_eval_fix`, `PartrecToTM2.tr_eval`, `ToPartrec.Code.Ok.zero`
`evalInduction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_maximal` 📖	mathematical	`Part` `Part.instMembership` `eval`	`Reaches`	—	`mem_eval` `Relation.reflTransGen_iff_eq`
`eval_maximal₁` 📖	mathematical	`Part` `Part.instMembership` `eval`	`Reaches₁`	—	`mem_eval` `Relation.TransGen.head'_iff`
`frespects_eq` 📖	mathematical	—	`FRespects`	—	`reaches₁_eq`
`fun_respects` 📖	mathematical	—	`Respects` `FRespects`	—	—
`mem_eval` 📖	mathematical	—	`Part` `Part.instMembership` `eval` `Reaches`	—	`Part.mem_unique` `PFun.mem_fix_iff` `Part.mem_some_iff` `Relation.ReflTransGen.head` `Relation.ReflTransGen.head_induction_on` `Part.mem_some`
`reaches_eval` 📖	mathematical	`Reaches`	`eval`	—	`Part.ext` `mem_eval` `eval_maximal` `reaches_total` `Relation.ReflTransGen.trans`
`reaches_total` 📖	—	`Reaches`	—	—	`Relation.ReflTransGen.total_of_right_unique`
`reaches₀_eq` 📖	mathematical	—	`Reaches₀`	—	`reaches₁_eq`
`reaches₁_eq` 📖	mathematical	—	`Reaches₁`	—	`Relation.TransGen.head'_iff`
`reaches₁_fwd` 📖	mathematical	`Reaches₁`	`Reaches`	—	`Relation.TransGen.head'_iff`
`tr_eval` 📖	—	`Respects` `Part` `Part.instMembership` `eval`	—	—	`mem_eval` `tr_reaches`
`tr_eval'` 📖	mathematical	`Respects`	`eval` `Part` `Part.instMonad`	—	`Part.ext` `tr_eval_rev` `Part.mem_map_iff` `tr_eval`
`tr_eval_dom` 📖	mathematical	`Respects`	`Part.Dom` `eval`	—	`tr_eval_rev` `tr_eval`
`tr_eval_rev` 📖	—	`Respects` `Part` `Part.instMembership` `eval`	—	—	`mem_eval` `tr_reaches_rev` `Relation.reflTransGen_iff_eq` `Relation.TransGen.head'_iff`
`tr_reaches` 📖	—	`Respects` `Reaches`	—	—	`Relation.reflTransGen_iff_eq_or_transGen` `tr_reaches₁` `Relation.TransGen.to_reflTransGen`
`tr_reaches_rev` 📖	—	`Respects` `Reaches`	—	—	`Relation.ReflTransGen.cases_head` `Relation.TransGen.head'_iff`
`tr_reaches₁` 📖	—	`Respects` `Reaches₁`	—	—	—

Turing.Reaches

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to₀` 📖	mathematical	`Turing.Reaches`	`Turing.Reaches₀`	—	`Relation.TransGen.trans_right`

Turing.Reaches₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`head` 📖	—	`Turing.Reaches₀`	—	—	`trans` `single`
`refl` 📖	mathematical	—	`Turing.Reaches₀`	—	—
`single` 📖	mathematical	—	`Turing.Reaches₀`	—	`Relation.TransGen.head`
`tail` 📖	—	`Turing.Reaches₀`	—	—	`trans` `single`
`tail'` 📖	mathematical	`Turing.Reaches₀`	`Turing.Reaches₁`	—	—
`trans` 📖	—	`Turing.Reaches₀`	—	—	—

Turing.Reaches₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to₀` 📖	mathematical	`Turing.Reaches₁`	`Turing.Reaches₀`	—	—

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`
`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` 📖	—	`Supports` `Cfg` `step` `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	1 math math: `Turing.TM0.Machine.map_respects`

Turing.TM0.Machine

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`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`	`Turing.Respects` `Turing.TM0.Cfg` `Turing.TM0.step` `map` `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	—	`Turing.Respects` `Turing.TM0.Cfg` `Turing.TM1.Cfg` `Λ'` `Turing.TM0.step` `Turing.TM1.step` `tr` `trCfg`	—	`Turing.fun_respects` `Relation.TransGen.head` `Relation.TransGen.head'` `Relation.ReflTransGen.single`

Turing.TM1

Definitions

Name	Category	Theorems
`Cfg` 📖	CompData	6 math math: `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	1 math math: `stmts₁_self`
`Supports` 📖	MathDef	1 math math: `Turing.TM2to1.tr_supports`
`SupportsStmt` 📖	MathDef	3 math math: `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	6 math math: `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	4 math math: `Turing.TM1to1.stepAux_write`, `Turing.TM1to1.stepAux_read`, `Turing.TM1to1.stepAux_move`, `Turing.TM2to1.tr_respects_aux₂`
`stmts` 📖	CompOp	—
`stmts₁` 📖	CompOp	1 math math: `stmts₁_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`step_supports` 📖	—	`Supports` `Cfg` `step` `Finset` `Finset.instMembership` `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` `Finset.instMembership` `stmts`	`SupportsStmt`	—	`stmts₁_supportsStmt_mono`
`stmts_trans` 📖	—	`Stmt` `Finset` `Finset.instMembership` `stmts₁` `stmts`	—	—	`stmts₁_trans`
`stmts₁_self` 📖	mathematical	—	`Stmt` `Finset` `Finset.instMembership` `stmts₁`	—	—
`stmts₁_supportsStmt_mono` 📖	—	`Stmt` `Finset` `Finset.instMembership` `stmts₁` `SupportsStmt`	—	—	—
`stmts₁_trans` 📖	mathematical	`Stmt` `Finset` `Finset.instMembership` `stmts₁`	`Finset.instHasSubset`	—	`stmts₁.eq_def`

Turing.TM1.Cfg

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`l` 📖	CompOp	—
`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`	—	`Turing.tr_eval'` `tr_respects` `Part.map_eq_map` `Part.map_map` `Turing.TM1.eval.eq_1`
`tr_respects` 📖	mathematical	—	`Turing.Respects` `Turing.TM1.Cfg` `Turing.TM0.Cfg` `Λ'` `Turing.TM1.step` `Turing.TM0.step` `instInhabitedΛ'` `tr` `trCfg`	—	`Turing.fun_respects` `Relation.TransGen.head` `Turing.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	7 math math: `stepAux_write`, `stepAux_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` `Λ'`	`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`	`Turing.Respects` `Turing.TM1.Cfg` `Λ'` `Turing.TM1.step` `tr` `trCfg`	—	`Turing.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`	`Λ'` `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