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 📖	—	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 📖	—	TuringReducible	—	—	Set.mem_singleton_iff

(root)

Definitions

Name	Category	Theorems
TuringDegree 📖	CompOp	—
TuringEquivalent 📖	MathDef	2 math math: TuringEquivalent.refl, TuringEquivalent.equivalence
TuringReducible 📖	MathDef	5 math math: instIsPreorderPFunNatTuringReducible, TuringReducible.refl, 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