OAI/Computability/DegreeRigidity/Effective/LocalScan.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TuringRigidity.LocalComputability.f line 11
2. abbrev OAI.TuringRigidity.LocalComputability.r line 12
3. def OAI.TuringRigidity.LocalComputability.levelCode line 14
4. theorem OAI.TuringRigidity.LocalComputability.levelCode_primrec line 16
5. theorem OAI.TuringRigidity.LocalComputability.levelCode_eq line 20
6. theorem OAI.TuringRigidity.LocalComputability.condition_levelCode line 22
7. def OAI.TuringRigidity.LocalComputability.candidate line 25
8. theorem OAI.TuringRigidity.LocalComputability.candidate_recursive line 29
9. theorem OAI.TuringRigidity.LocalComputability.candidate_eq line 36
10. def OAI.TuringRigidity.LocalComputability.scanStep line 40
11. theorem OAI.TuringRigidity.LocalComputability.scanStep_recursive line 48
12. def OAI.TuringRigidity.LocalComputability.scan line 66
13. theorem OAI.TuringRigidity.LocalComputability.scan_recursive line 68
14. theorem OAI.TuringRigidity.LocalComputability.source_scan_succ line 73
15. theorem OAI.TuringRigidity.LocalComputability.scan_eq line 89