TuringDegree

📁 Source: Mathlib/Computability/TuringDegree.lean

Statistics

Metric	Count
Definitions «term_≡ᵀ_», «term_≤ᵀ_», TuringDegree, instPartialOrder, TuringEquivalent, TuringReducible	6
Theorems turingReducible, equivalence, refl, trans, partrec_of_zero, refl, rfl, trans, instIsPreorderPFunNatTuringReducible, partrec_iff_forall_turingReducible	10
Total	16

Computability

Definitions

Name	Category	Theorems
«term_≡ᵀ_» 📖	CompOp	—
«term_≤ᵀ_» 📖	CompOp	—

Nat.Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
turingReducible 📖	mathematical	—	TuringReducible	—	—

TuringDegree

Definitions

Name	Category	Theorems
instPartialOrder 📖	CompOp	—

TuringEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence 📖	mathematical	—	PFun TuringEquivalent	—	instIsPreorderPFunNatTuringReducible
refl 📖	mathematical	—	TuringEquivalent	—	equivalence
trans 📖	mathematical	TuringEquivalent	TuringEquivalent	—	equivalence

TuringReducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partrec_of_zero 📖	—	TuringReducible Part.some	—	—	Set.mem_singleton_iff
refl 📖	mathematical	—	TuringReducible	—	—
rfl 📖	mathematical	—	TuringReducible	—	refl
trans 📖	mathematical	TuringReducible	TuringReducible	—	Set.mem_singleton_iff

(root)

Definitions

Name	Category	Theorems
TuringDegree 📖	CompOp	—
TuringEquivalent 📖	MathDef	4 math math: TuringEquivalent.symm, TuringEquivalent.refl, TuringEquivalent.equivalence, TuringEquivalent.trans
TuringReducible 📖	MathDef	6 math math: instIsPreorderPFunNatTuringReducible, TuringReducible.refl, TuringReducible.trans, TuringReducible.rfl, partrec_iff_forall_turingReducible, Nat.Partrec.turingReducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsPreorderPFunNatTuringReducible 📖	mathematical	—	IsPreorder PFun TuringReducible	—	TuringReducible.rfl TuringReducible.trans
partrec_iff_forall_turingReducible 📖	mathematical	—	TuringReducible	—	Nat.Partrec.turingReducible TuringReducible.partrec_of_zero

---

← Back to Index