Documentation Verification Report

TMConfig

📁 Source: Mathlib/Computability/TMConfig.lean

Statistics

Metric	Count
Definitions `Cfg`, `then`, `Code`, `Ok`, `eval`, `head`, `id`, `nil`, `prec`, `pred`, `rfind`, `zero`, `eval`, `then`, `instDecidableEqCode`, `decEq`, `instInhabitedCfg`, `default`, `instInhabitedCode`, `default`, `instInhabitedCont`, `default`, `step`, `stepNormal`, `stepRet`	25
Theorems `zero`, `case_eval`, `comp_eval`, `cons_eval`, `exists_code`, `comp`, `fix_eval`, `head_eval`, `id_eval`, `nil_eval`, `pred_eval`, `succ_eval`, `tail_eval`, `zero'_eval`, `zero_eval`, `then_eval`, `code_is_ok`, `cont_eval_fix`, `is_ret`, `stepNormal_eval`, `stepNormal_then`, `stepRet_eval`, `stepRet_then`	23
Total	48

Turing.ToPartrec

Definitions

Name	Category	Theorems
`Cfg` 📖	CompData	5 math math: `stepNormal_eval`, `Turing.PartrecToTM2.tr_respects`, `stepRet_eval`, `cont_eval_fix`, `Code.Ok.zero`
`Code` 📖	CompData	—
`instDecidableEqCode` 📖	CompOp	—
`instInhabitedCfg` 📖	CompOp	—
`instInhabitedCode` 📖	CompOp	—
`instInhabitedCont` 📖	CompOp	—
`step` 📖	CompOp	5 math math: `stepNormal_eval`, `Turing.PartrecToTM2.tr_respects`, `stepRet_eval`, `cont_eval_fix`, `Code.Ok.zero`
`stepNormal` 📖	CompOp	7 math math: `stepNormal_eval`, `cont_eval_fix`, `stepNormal.is_ret`, `stepNormal_then`, `Code.Ok.zero`, `Turing.PartrecToTM2.trNormal_respects`, `Turing.PartrecToTM2.tr_init`
`stepRet` 📖	CompOp	3 math math: `stepRet_then`, `stepRet_eval`, `Turing.PartrecToTM2.tr_ret_respects`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`code_is_ok` 📖	mathematical	—	`Code.Ok`	—	`stepNormal.eq_1` `Part.instLawfulMonad` `stepNormal.eq_2` `stepNormal.eq_3` `stepNormal.eq_4` `Code.eval.eq_4` `Turing.reaches_eval` `Relation.ReflTransGen.single` `stepRet.eq_2` `stepNormal.eq_5` `Code.eval.eq_5` `stepRet.eq_4` `stepNormal.eq_6` `stepNormal.eq_7` `cont_eval_fix`
`cont_eval_fix` 📖	mathematical	`Code.Ok`	`Turing.eval` `Cfg` `step` `stepNormal` `Cont.fix` `Part` `Part.instMonad` `Code.eval` `Code.fix` `Cfg.ret`	—	`Part.ext` `Turing.mem_eval` `Part.mem_bind_iff` `Part.bind_eq_bind` `Part.mem_unique` `Turing.reaches_eval` `Relation.ReflTransGen.single` `Part.mem_some` `stepNormal.is_ret` `stepNormal_then` `Cfg.then.eq_1` `stepRet.eq_5` `Cfg.then.eq_2` `Cont.then.eq_1` `stepRet_then` `PFun.mem_fix_iff` `Part.eq_some_iff` `Part.map_some` `Part.mem_some_iff` `Part.mem_map_iff`
`stepNormal_eval` 📖	mathematical	—	`Turing.eval` `Cfg` `step` `stepNormal` `Cont.halt` `Part` `Part.instMonad` `Cfg.halt` `Code.eval`	—	`Code.Ok.zero` `code_is_ok`
`stepNormal_then` 📖	mathematical	—	`stepNormal` `Cont.then` `Cfg.then`	—	`Cont.then.eq_2` `Cont.then.eq_4` `Cont.then.eq_5`
`stepRet_eval` 📖	mathematical	—	`Turing.eval` `Cfg` `step` `stepRet` `Part` `Part.instMonad` `Cfg.halt` `Cont.eval`	—	`Part.instLawfulMonad` `Part.eq_some_iff` `Turing.mem_eval` `Cont.eval.eq_2` `stepRet.eq_2` `code_is_ok` `Turing.reaches_eval` `Relation.ReflTransGen.single` `stepRet.eq_3` `Cont.eval.eq_3` `Cont.eval.eq_4` `stepRet.eq_4` `Cont.eval.eq_5` `stepRet.eq_5` `cont_eval_fix`
`stepRet_then` 📖	mathematical	—	`stepRet` `Cont.then` `Cfg.then`	—	`stepNormal_then`

Turing.ToPartrec.Cfg

Definitions

Name	Category	Theorems
`then` 📖	CompOp	2 math math: `Turing.ToPartrec.stepRet_then`, `Turing.ToPartrec.stepNormal_then`

Turing.ToPartrec.Code

Definitions

Name	Category	Theorems
`Ok` 📖	MathDef	1 math math: `Turing.ToPartrec.code_is_ok`
`eval` 📖	CompOp	17 math math: `comp_eval`, `nil_eval`, `pred_eval`, `head_eval`, `Turing.ToPartrec.stepNormal_eval`, `zero'_eval`, `tail_eval`, `id_eval`, `cons_eval`, `Turing.ToPartrec.cont_eval_fix`, `exists_code`, `succ_eval`, `Turing.PartrecToTM2.tr_eval`, `Ok.zero`, `fix_eval`, `zero_eval`, `case_eval`
`head` 📖	CompOp	1 math math: `head_eval`
`id` 📖	CompOp	1 math math: `id_eval`
`nil` 📖	CompOp	1 math math: `nil_eval`
`prec` 📖	CompOp	—
`pred` 📖	CompOp	1 math math: `pred_eval`
`rfind` 📖	CompOp	—
`zero` 📖	CompOp	1 math math: `zero_eval`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`case_eval` 📖	mathematical	—	`eval` `case` `Part` `List.headI`	—	—
`comp_eval` 📖	mathematical	—	`eval` `comp` `Part` `Part.instMonad`	—	—
`cons_eval` 📖	mathematical	—	`eval` `cons` `Part` `Part.instMonad` `List.headI`	—	—
`exists_code` 📖	mathematical	`Nat.Partrec'`	`eval` `Part` `Part.instMonad` `List.instAlternativeMonad_mathlib`	—	`head_eval` `List.Vector.get_zero` `comp_eval` `tail_eval` `Part.bind_some` `List.Vector.tail_val` `List.Vector.get_tail_succ` `Vector.mOfFn_part_some` `exists_code.comp` `List.Vector.cons_head_tail` `Part.map_some` `List.Vector.cons_val` `List.Vector.tail_cons` `List.Vector.head_cons` `cons_eval` `case_eval` `id_eval` `zero'_eval` `fix_eval` `succ_eval` `pred_eval` `Part.bind_assoc` `nil_eval` `PFun.mem_fix_iff` `Part.eq_some_iff` `Part.mem_some_iff` `add_right_comm` `zero_add` `Nat.instCanonicallyOrderedAdd` `Part.ext` `Part.map_bind`
`fix_eval` 📖	mathematical	—	`eval` `fix` `PFun.fix` `Part.map` `List.headI`	—	—
`head_eval` 📖	mathematical	—	`eval` `head` `Part` `Part.instMonad` `List.headI`	—	`cons_eval` `id_eval` `nil_eval` `Part.bind_some`
`id_eval` 📖	mathematical	—	`eval` `id` `Part` `Part.instMonad`	—	`comp_eval` `zero'_eval` `tail_eval` `Part.bind_some`
`nil_eval` 📖	mathematical	—	`eval` `nil` `Part` `Part.instMonad`	—	`comp_eval` `succ_eval` `tail_eval` `Part.bind_some`
`pred_eval` 📖	mathematical	—	`eval` `pred` `Part` `Part.instMonad` `List.headI`	—	`case_eval` `zero_eval` `head_eval` `Nat.instCanonicallyOrderedAdd` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`succ_eval` 📖	mathematical	—	`eval` `succ` `Part` `Part.instMonad` `List.headI`	—	—
`tail_eval` 📖	mathematical	—	`eval` `tail` `Part` `Part.instMonad`	—	—
`zero'_eval` 📖	mathematical	—	`eval` `zero'` `Part` `Part.instMonad`	—	—
`zero_eval` 📖	mathematical	—	`eval` `zero` `Part` `Part.instMonad`	—	`cons_eval` `zero'_eval` `nil_eval` `Part.bind_some`

Turing.ToPartrec.Code.Ok

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero` 📖	mathematical	`Turing.ToPartrec.Code.Ok`	`Turing.eval` `Turing.ToPartrec.Cfg` `Turing.ToPartrec.step` `Turing.ToPartrec.stepNormal` `Turing.ToPartrec.Cont.halt` `Part` `Part.instMonad` `Turing.ToPartrec.Cfg.halt` `Turing.ToPartrec.Code.eval`	—	`Part.instLawfulMonad` `Part.eq_some_iff` `Turing.mem_eval` `Relation.ReflTransGen.single`

Turing.ToPartrec.Code.exists_code

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`Turing.ToPartrec.Code.eval` `Part` `Part.instMonad` `List.instAlternativeMonad_mathlib`	`List.Vector` `List.Vector.mOfFn`	—	`Turing.ToPartrec.Code.nil_eval` `Turing.ToPartrec.Code.cons_eval` `Part.instLawfulMonad` `Turing.ToPartrec.Code.comp_eval`

Turing.ToPartrec.Cont

Definitions

Name	Category	Theorems
`eval` 📖	CompOp	2 math math: `then_eval`, `Turing.ToPartrec.stepRet_eval`
`then` 📖	CompOp	3 math math: `Turing.ToPartrec.stepRet_then`, `then_eval`, `Turing.ToPartrec.stepNormal_then`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`then_eval` 📖	mathematical	—	`eval` `then` `Part` `Part.instMonad`	—	`Part.instLawfulMonad`

Turing.ToPartrec.instDecidableEqCode

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Turing.ToPartrec.instInhabitedCfg

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.ToPartrec.instInhabitedCode

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.ToPartrec.instInhabitedCont

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.ToPartrec.stepNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_ret` 📖	mathematical	—	`Turing.ToPartrec.stepNormal` `Turing.ToPartrec.Cfg.ret`	—	`eq_6`

---

← Back to Index