OAI/Computability/DegreeRigidity/Effective/UniformPair.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.UniformPair.request line 11
  2. theorem OAI.TuringRigidity.UniformPair.request_primrec line 13
  3. def OAI.TuringRigidity.UniformPair.IsCoding line 20
  4. theorem OAI.TuringRigidity.UniformPair.coding_recursive line 23
  5. def OAI.TuringRigidity.UniformPair.outcome line 38
  6. theorem OAI.TuringRigidity.UniformPair.outcome_recursive line 44
  7. def OAI.TuringRigidity.UniformPair.retag line 60
  8. theorem OAI.TuringRigidity.UniformPair.retag_primrec line 63
  9. def OAI.TuringRigidity.UniformPair.update line 67
  10. def OAI.TuringRigidity.UniformPair.next line 69
  11. theorem OAI.TuringRigidity.UniformPair.next_recursive line 71
  12. theorem OAI.TuringRigidity.UniformPair.next_extends line 80
  13. theorem OAI.TuringRigidity.UniformPair.split_coding_or_divergence line 88
  14. theorem OAI.TuringRigidity.UniformPair.next_spec line 113
  15. theorem OAI.TuringRigidity.UniformPair.disagreement_mono line 190
  16. theorem OAI.TuringRigidity.UniformPair.pair_exists line 196