OAI/Computability/DegreeRigidity/Effective/CodingSplitSearch.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.TuringRigidity.CodingSplitSearch.Witnessline 8 - def
OAI.TuringRigidity.CodingSplitSearch.finiteTrialline 10 - theorem
OAI.TuringRigidity.CodingSplitSearch.finiteTrial_primrecline 16 - def
OAI.TuringRigidity.CodingSplitSearch.trialline 39 - theorem
OAI.TuringRigidity.CodingSplitSearch.trial_recursiveline 43 - theorem
OAI.TuringRigidity.CodingSplitSearch.trial_soundline 54 - theorem
OAI.TuringRigidity.CodingSplitSearch.trial_completeline 89 - theorem
OAI.TuringRigidity.CodingSplitSearch.splittingLocations_enumerableline 119