OAI/Computability/DegreeRigidity/Representation/GenericCoding.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.GenericCoding.count line 11
  2. def OAI.TuringRigidity.GenericCoding.code line 13
  3. theorem OAI.TuringRigidity.GenericCoding.count_le line 16
  4. theorem OAI.TuringRigidity.GenericCoding.count_mono line 24
  5. def OAI.TuringRigidity.GenericCoding.InfiniteOdd line 30
  6. theorem OAI.TuringRigidity.GenericCoding.infiniteOdd_iff line 32
  7. theorem OAI.TuringRigidity.GenericCoding.count_unbounded line 43
  8. theorem OAI.TuringRigidity.GenericCoding.exists_insertion line 56
  9. theorem OAI.TuringRigidity.GenericCoding.count_recursive line 73
  10. theorem OAI.TuringRigidity.GenericCoding.code_recursive line 79
  11. theorem OAI.TuringRigidity.GenericCoding.code_reduces line 98
  12. def OAI.TuringRigidity.GenericCoding.recoverDecision line 103
  13. theorem OAI.TuringRigidity.GenericCoding.recoverDecision_primrec line 106
  14. def OAI.TuringRigidity.GenericCoding.recoverTrial line 111
  15. theorem OAI.TuringRigidity.GenericCoding.recoverTrial_recursive line 114
  16. theorem OAI.TuringRigidity.GenericCoding.recoverTrial_sound line 132
  17. theorem OAI.TuringRigidity.GenericCoding.recoverTrial_complete line 142
  18. theorem OAI.TuringRigidity.GenericCoding.set_reduces_code_join line 147
  19. theorem OAI.TuringRigidity.GenericCoding.join_degree_eq line 153
  20. theorem OAI.TuringRigidity.GenericCoding.source_join_degree_eq line 159
  21. theorem OAI.TuringRigidity.GenericCoding.forward_single_program line 163
  22. theorem OAI.TuringRigidity.GenericCoding.inverse_single_program line 168