OAI/Computability/DegreeRigidity/CohenForcing/CohenHalting.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.CohenHalting.table line 8
  2. theorem OAI.TuringRigidity.CohenHalting.table_primrec line 9
  3. def OAI.TuringRigidity.CohenHalting.Agrees line 11
  4. theorem OAI.TuringRigidity.CohenHalting.agrees_recursive line 15
  5. def OAI.TuringRigidity.CohenHalting.Certificate line 49
  6. theorem OAI.TuringRigidity.CohenHalting.certificate_recursive line 56
  7. def OAI.TuringRigidity.CohenHalting.OpenHalts line 67
  8. theorem OAI.TuringRigidity.CohenHalting.openHalts_sigma line 69
  9. def OAI.TuringRigidity.CohenHalting.Prefix line 72
  10. def OAI.TuringRigidity.CohenHalting.initial line 74
  11. theorem OAI.TuringRigidity.CohenHalting.initial_length line 76
  12. theorem OAI.TuringRigidity.CohenHalting.initial_getD line 78
  13. theorem OAI.TuringRigidity.CohenHalting.initial_prefix line 81
  14. theorem OAI.TuringRigidity.CohenHalting.prefix_initial line 85
  15. theorem OAI.TuringRigidity.CohenHalting.initial_mono line 92
  16. theorem OAI.TuringRigidity.CohenHalting.agrees_table line 95
  17. theorem OAI.TuringRigidity.CohenHalting.openHalts_sound line 109
  18. theorem OAI.TuringRigidity.CohenHalting.openHalts_complete line 118
  19. theorem OAI.TuringRigidity.CohenHalting.openHalts_mono line 139