OAI/Computability/DegreeRigidity/Representation/CategoryMachine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.CategorySearch.rationalBit line 9
  2. theorem OAI.TuringRigidity.CategorySearch.rationalBit_primrec line 11
  3. theorem OAI.TuringRigidity.CategorySearch.rationalBit_eq line 15
  4. def OAI.TuringRigidity.CategorySearch.sample line 19
  5. def OAI.TuringRigidity.CategorySearch.finiteOracle line 21
  6. theorem OAI.TuringRigidity.CategorySearch.partialJoin_oracle line 25
  7. def OAI.TuringRigidity.CategorySearch.Avalue line 30
  8. theorem OAI.TuringRigidity.CategorySearch.finiteOracle_approximates line 32
  9. def OAI.TuringRigidity.CategorySearch.inside line 47
  10. instance OAI.TuringRigidity.CategorySearch.(instance at line 50) line 50
  11. theorem OAI.TuringRigidity.CategorySearch.inside_primrec line 52
  12. theorem OAI.TuringRigidity.CategorySearch.inside_iff line 58
  13. def OAI.TuringRigidity.CategorySearch.finiteRun line 62
  14. theorem OAI.TuringRigidity.CategorySearch.finiteRun_partrec line 68
  15. theorem OAI.TuringRigidity.CategorySearch.finiteRun_code line 95