OAI/Computability/DegreeRigidity/Effective/EffectiveWitness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.EffectiveWitness.least line 8
2. theorem OAI.TuringRigidity.EffectiveWitness.least_spec line 13
3. theorem OAI.TuringRigidity.EffectiveWitness.least_recursive line 18
4. def OAI.TuringRigidity.EffectiveWitness.Accept line 32
5. theorem OAI.TuringRigidity.EffectiveWitness.accept_total line 36
6. theorem OAI.TuringRigidity.EffectiveWitness.accept_recursive line 43
7. def OAI.TuringRigidity.EffectiveWitness.witness line 59
8. theorem OAI.TuringRigidity.EffectiveWitness.witness_recursive line 62
9. theorem OAI.TuringRigidity.EffectiveWitness.witness_spec line 66
10. theorem OAI.TuringRigidity.EffectiveWitness.sigma1_choice line 71