OAI/Computability/DegreeRigidity/Effective/StageScan.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TuringRigidity.StageComputability.f line 10
  2. abbrev OAI.TuringRigidity.StageComputability.r line 11
  3. def OAI.TuringRigidity.StageComputability.levelCode line 13
  4. theorem OAI.TuringRigidity.StageComputability.levelCode_primrec line 15
  5. theorem OAI.TuringRigidity.StageComputability.levelCode_eq line 19
  6. theorem OAI.TuringRigidity.StageComputability.condition_levelCode line 21
  7. def OAI.TuringRigidity.StageComputability.candidate line 24
  8. theorem OAI.TuringRigidity.StageComputability.candidate_recursive line 28
  9. theorem OAI.TuringRigidity.StageComputability.candidate_eq line 35
  10. def OAI.TuringRigidity.StageComputability.scanStep line 39
  11. theorem OAI.TuringRigidity.StageComputability.scanStep_recursive line 47
  12. def OAI.TuringRigidity.StageComputability.scan line 65
  13. theorem OAI.TuringRigidity.StageComputability.scan_recursive line 67
  14. theorem OAI.TuringRigidity.StageComputability.source_scan_succ line 72
  15. theorem OAI.TuringRigidity.StageComputability.scan_eq line 88