OAI/Computability/DegreeRigidity/Effective/RecursiveInfiniteSubset.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RecursiveInfiniteSubset.Unbounded line 8
  2. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.accepted_exists line 10
  3. def OAI.TuringRigidity.RecursiveInfiniteSubset.index line 15
  4. def OAI.TuringRigidity.RecursiveInfiniteSubset.above line 18
  5. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.above_spec line 21
  6. def OAI.TuringRigidity.RecursiveInfiniteSubset.flag line 30
  7. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.flag_primrec line 34
  8. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.index_recursive line 40
  9. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.above_recursive line 56
  10. def OAI.TuringRigidity.RecursiveInfiniteSubset.growing line 64
  11. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.growing_strictMono line 68
  12. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.growing_mem line 73
  13. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.growing_recursive line 77
  14. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.recursive_range line 99
  15. theorem OAI.TuringRigidity.RecursiveInfiniteSubset.infinite_recursive_subset line 129