OAI/Computability/DegreeRigidity/Effective/GuardedScan.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

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