Documentation Verification Report

Halting

📁 Source: Mathlib/Computability/Halting.lean

Statistics

Metric	Count
Definitions `ComputablePred`, `Partrec'`, `REPred`	3
Theorems `computablePred`, `computable_iff`, `computable_iff_re_compl_re`, `computable_iff_re_compl_re'`, `decide`, `halting_problem`, `halting_problem_not_re`, `halting_problem_re`, `ite`, `not`, `of_eq`, `rice`, `rice₂`, `to_re`, `prim`, `bind`, `comp'`, `comp₁`, `cons`, `head`, `idv`, `map`, `nil`, `of_eq`, `of_part`, `of_prim`, `part_iff`, `part_iff₁`, `part_iff₂`, `rfindOpt`, `tail`, `to_part`, `vec_iff`, `merge'`, `cond`, `dom_re`, `merge`, `merge'`, `sumCasesOn`, `computablePred`, `of_eq`, `computablePred_iff_computable_decide`	42
Total	45

Computable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`computablePred` 📖	mathematical	`Computable` `Primcodable.bool`	`ComputablePred`	—	—

ComputablePred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`computable_iff` 📖	mathematical	—	`ComputablePred` `Computable` `Primcodable.bool`	—	`Bool.decide_iff`
`computable_iff_re_compl_re` 📖	mathematical	—	`ComputablePred` `REPred`	—	`to_re` `not` `Partrec.merge` `Partrec.map` `Computable.to₂` `Computable.const` `Partrec.of_eq` `Part.eq_some_iff`
`computable_iff_re_compl_re'` 📖	mathematical	—	`ComputablePred` `REPred`	—	`computable_iff_re_compl_re`
`decide` 📖	mathematical	`ComputablePred`	`Computable` `Primcodable.bool`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonDecidable`
`halting_problem` 📖	mathematical	—	`ComputablePred` `Nat.Partrec.Code` `Primcodable.ofDenumerable` `Nat.Partrec.Code.instDenumerable` `Part.Dom` `Nat.Partrec.Code.eval`	—	`rice` `Nat.Partrec.none`
`halting_problem_not_re` 📖	mathematical	—	`REPred` `Nat.Partrec.Code` `Primcodable.ofDenumerable` `Nat.Partrec.Code.instDenumerable` `Part.Dom` `Nat.Partrec.Code.eval`	—	`halting_problem` `computable_iff_re_compl_re'` `halting_problem_re`
`halting_problem_re` 📖	mathematical	—	`REPred` `Nat.Partrec.Code` `Primcodable.ofDenumerable` `Nat.Partrec.Code.instDenumerable` `Part.Dom` `Nat.Partrec.Code.eval`	—	`Partrec.dom_re` `Partrec₂.comp` `Nat.Partrec.Code.eval_part` `Computable.id` `Computable.const`
`ite` 📖	—	`Computable` `Primcodable.ofDenumerable` `Denumerable.nat` `ComputablePred`	—	—	`Computable.cond` `decide`
`not` 📖	—	`ComputablePred`	—	—	`Computable.computablePred` `Computable.of_eq` `Computable.comp` `Primrec.to_comp` `Primrec.not`
`of_eq` 📖	—	`ComputablePred`	—	—	—
`rice` 📖	—	`ComputablePred` `Nat.Partrec.Code` `Primcodable.ofDenumerable` `Nat.Partrec.Code.instDenumerable` `PFun` `Set` `Set.instMembership` `Nat.Partrec.Code.eval`	—	—	`Nat.Partrec.Code.fixed_point₂` `Partrec.to₂` `Partrec.cond` `Computable.comp` `Computable.fst` `Partrec.comp` `Partrec.nat_iff` `Computable.snd`
`rice₂` 📖	mathematical	`Nat.Partrec.Code` `Set` `Set.instMembership`	`ComputablePred` `Primcodable.ofDenumerable` `Nat.Partrec.Code.instDenumerable` `Set.instEmptyCollection` `Set.univ`	—	`Set.mem_image_of_mem` `Set.eq_univ_of_forall` `Set.nonempty_iff_ne_empty` `rice` `of_eq` `Partrec.nat_iff` `Partrec₂.comp` `Nat.Partrec.Code.eval_part` `Computable.const` `Computable.id`
`to_re` 📖	mathematical	`ComputablePred`	`REPred`	—	`computable_iff` `Partrec.of_eq` `Partrec.cond` `Decidable.Partrec.const'` `Partrec.none` `Part.ext` `instIsEmptyFalse`

Nat

Definitions

Name	Category	Theorems
`Partrec'` 📖	CompData	6 math math: `Partrec'.of_part`, `Partrec'.of_prim`, `Partrec'.part_iff`, `Partrec'.part_iff₂`, `Partrec'.head`, `Partrec'.part_iff₁`

Nat.Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`merge'` 📖	mathematical	—	`Part` `Part.instMembership` `Part.Dom`	—	`Code.exists_code` `Partrec.nat_iff` `Partrec.rfindOpt` `Computable₂.comp` `Primrec₂.to_comp` `Primrec.option_orElse` `Computable.comp` `Primrec.to_comp` `Code.primrec_evaln` `Computable.pair` `Computable.snd` `Computable.const` `Computable.fst` `Nat.rfindOpt_spec` `Code.evaln_sound` `Exists.fst` `Nat.rfindOpt_dom`

Nat.Partrec'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind` 📖	mathematical	`Nat.Partrec'`	`Part.bind` `List.Vector.cons`	—	`of_eq` `Vector.mOfFn_part_some` `List.Vector.ofFn_get` `Part.bind_some` `Part.bind_assoc`
`comp'` 📖	—	`Nat.Partrec'` `Vec`	—	—	`of_eq` `Vector.mOfFn_part_some` `List.Vector.ofFn_get` `Part.bind_some`
`comp₁` 📖	—	`Nat.Partrec'` `List.Vector.head` `PFun.lift` `List.Vector`	—	—	`List.Vector.head_cons` `comp'` `cons` `nil`
`cons` 📖	mathematical	`Nat.Partrec'` `PFun.lift` `List.Vector` `Vec`	`List.Vector.cons`	—	`List.Vector.get_zero` `List.Vector.head_cons` `List.Vector.get_cons_succ`
`head` 📖	mathematical	—	`Nat.Partrec'` `PFun.lift` `List.Vector` `List.Vector.head`	—	`Nat.Primrec'.head`
`idv` 📖	mathematical	—	`Vec` `List.Vector`	—	`Vec.prim` `Nat.Primrec'.idv`
`map` 📖	mathematical	`Nat.Partrec'` `PFun.lift` `List.Vector`	`Part.map` `List.Vector.cons`	—	`Part.bind_some_eq_map` `bind`
`nil` 📖	mathematical	—	`Vec` `List.Vector.nil`	—	—
`of_eq` 📖	—	`Nat.Partrec'`	—	—	—
`of_part` 📖	mathematical	`Part.bind` `List.Vector` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Primcodable.vector` `Primcodable.ofDenumerable` `Denumerable.nat` `Part.map` `Encodable.encode`	`Nat.Partrec'`	—	`Nat.Partrec.Code.exists_code` `Nat.Partrec.Code.eval_eq_rfindOpt` `List.Vector.head_cons` `List.Vector.tail_cons` `Denumerable.ofNat_encode` `rfindOpt` `of_prim` `Primrec.encode_iff` `Primrec.comp` `Nat.Partrec.Code.primrec_evaln` `Primrec.pair` `Primrec.vector_head` `Primrec.const` `Primrec.vector_tail` `of_eq` `comp₁` `Nat.Primrec'.encode` `Encodable.encodek` `Part.map_id'` `Part.bind_some`
`of_prim` 📖	mathematical	`Encodable.encode` `Option.encodable` `Primcodable.toEncodable` `Primcodable.ofDenumerable` `Denumerable.nat` `List.Vector` `Encodable.decode` `Primcodable.vector`	`Nat.Partrec'` `PFun.lift`	—	`Nat.Primrec'.of_prim`
`part_iff` 📖	mathematical	—	`Nat.Partrec'` `Part.bind` `List.Vector` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Primcodable.vector` `Primcodable.ofDenumerable` `Denumerable.nat` `Part.map` `Encodable.encode`	—	`to_part` `of_part`
`part_iff₁` 📖	mathematical	—	`Nat.Partrec'` `List.Vector.head` `Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Primcodable.ofDenumerable` `Denumerable.nat` `Part.map` `Encodable.encode`	—	`part_iff` `Partrec.of_eq` `Partrec.comp` `Primrec.to_comp` `Primrec.vector_ofFn` `Primrec.id` `List.Vector.head_ofFn` `Computable.vector_head`
`part_iff₂` 📖	mathematical	—	`Nat.Partrec'` `List.Vector.head` `List.Vector.tail` `Partrec₂` `Primcodable.ofDenumerable` `Denumerable.nat`	—	`part_iff` `Partrec.of_eq` `Partrec.comp` `Computable₂.comp` `Computable.vector_cons` `Computable.fst` `Computable.snd` `Computable.const` `List.Vector.head_cons` `List.Vector.tail_cons` `Partrec₂.comp` `Computable.vector_head` `Computable.comp` `Computable.vector_tail`
`rfindOpt` 📖	mathematical	`Nat.Partrec'` `PFun.lift` `List.Vector`	`Nat.rfindOpt` `Denumerable.ofNat` `Denumerable.option` `Denumerable.nat` `List.Vector.cons`	—	`of_eq` `bind` `comp₁` `of_prim` `Primrec₂.comp` `Primrec.nat_sub` `Primrec.const` `Primrec.vector_head` `Nat.Primrec'.pred` `Part.ext` `Nat.instCanonicallyOrderedAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.rfind_spec`
`tail` 📖	mathematical	`Nat.Partrec'`	`List.Vector.tail`	—	`of_eq` `Vector.mOfFn_part_some` `Part.bind_some` `List.Vector.ofFn_get` `List.Vector.get_tail_succ`
`to_part` 📖	mathematical	`Nat.Partrec'`	`Part.bind` `List.Vector` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Primcodable.vector` `Primcodable.ofDenumerable` `Denumerable.nat` `Part.map` `Encodable.encode`	—	`Primrec.to_comp` `Nat.Primrec'.to_prim` `Partrec.bind` `Partrec.vector_mOfFn` `Partrec.comp` `Computable.snd` `Computable₂.comp` `Computable.vector_cons` `Computable.fst` `Computable₂.partrec₂` `Computable.to₂` `Computable.comp` `Primrec₂.comp` `PrimrecRel.decide` `Primrec.eq` `Primrec.id` `Primrec.const` `Partrec.rfind`
`vec_iff` 📖	mathematical	—	`Vec` `Computable` `List.Vector` `Primcodable.vector` `Primcodable.ofDenumerable` `Denumerable.nat`	—	`List.Vector.ofFn_get` `Computable.vector_ofFn` `to_part` `of_part` `Computable₂.comp` `Computable.vector_get` `Computable.const`

Nat.Partrec'.Vec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prim` 📖	mathematical	`Nat.Primrec'.Vec`	`Nat.Partrec'.Vec`	—	—

Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cond` 📖	—	`Computable` `Primcodable.bool` `Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Part.map` `Encodable.encode`	—	—	`Nat.Partrec.Code.exists_code` `of_eq` `bind` `Partrec₂.comp` `Nat.Partrec.Code.eval_part` `Computable.cond` `Computable.const` `Computable.encode` `to₂` `Computable.ofOption` `Computable.comp` `Computable.decode` `Computable.snd` `Encodable.encodek` `Part.bind_some` `Part.bind_map` `Part.bind_some_right`
`dom_re` 📖	mathematical	`Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Part.map` `Encodable.encode`	`REPred` `Part.Dom`	—	`of_eq` `map` `Computable.to₂` `Computable.const` `Part.ext`
`merge` 📖	mathematical	`Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Part.map` `Encodable.encode`	`Part` `Part.instMembership`	—	`merge'` `Exists.fst` `Part.mem_unique`
`merge'` 📖	mathematical	`Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Part.map` `Encodable.encode`	`Part` `Part.instMembership` `Part.Dom`	—	`Nat.Partrec.merge'` `bind_decode₂_iff` `bind` `comp` `nat_iff` `Computable.encode` `to₂` `Computable.ofOption` `Computable.decode` `Computable.snd` `Encodable.decode₂_encode` `Part.bind_some` `Encodable.encodek` `Exists.fst` `Part.bind_dom` `Encodable.encodek₂`
`sumCasesOn` 📖	mathematical	`Computable` `Primcodable.sum` `Partrec₂`	`Part.bind` `Part.ofOption` `Encodable.decode` `Primcodable.toEncodable` `Part.map` `Encodable.encode`	—	`option_some_iff` `of_eq` `cond` `Computable.sumCasesOn` `Computable.to₂` `Computable.const` `sumCasesOn_left` `to₂` `sumCasesOn_right`

PrimrecPred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`computablePred` 📖	mathematical	`PrimrecPred`	`ComputablePred`	—	`Computable.computablePred` `Primrec.to_comp`

REPred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_eq` 📖	—	`REPred`	—	—	—

(root)

Definitions

Name	Category	Theorems
`ComputablePred` 📖	MathDef	8 math math: `computablePred_iff_computable_decide`, `ComputablePred.computable_iff_re_compl_re'`, `ComputablePred.rice₂`, `PrimrecPred.computablePred`, `ComputablePred.computable_iff_re_compl_re`, `ComputablePred.halting_problem`, `Computable.computablePred`, `ComputablePred.computable_iff`
`REPred` 📖	MathDef	6 math math: `ComputablePred.computable_iff_re_compl_re'`, `ComputablePred.computable_iff_re_compl_re`, `ComputablePred.halting_problem_not_re`, `Partrec.dom_re`, `ComputablePred.halting_problem_re`, `ComputablePred.to_re`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`computablePred_iff_computable_decide` 📖	mathematical	—	`ComputablePred` `Computable` `Primcodable.bool`	—	`ComputablePred.decide` `Computable.computablePred`

---

← Back to Index