OAI/Computability/DegreeRigidity/Effective/UniformSplit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.UniformSplit.base line 10
  2. def OAI.TuringRigidity.UniformSplit.program line 11
  3. def OAI.TuringRigidity.UniformSplit.start line 12
  4. def OAI.TuringRigidity.UniformSplit.SplitCert line 14
  5. theorem OAI.TuringRigidity.UniformSplit.splitCert_sigma line 21
  6. def OAI.TuringRigidity.UniformSplit.PointCert line 34
  7. theorem OAI.TuringRigidity.UniformSplit.pointCert_sigma line 42
  8. def OAI.TuringRigidity.UniformSplit.ConvergesAbove line 62
  9. theorem OAI.TuringRigidity.UniformSplit.convergesAbove_sigma line 68
  10. def OAI.TuringRigidity.UniformSplit.DivCert line 79
  11. theorem OAI.TuringRigidity.UniformSplit.divCert_recursive line 82
  12. def OAI.TuringRigidity.UniformSplit.Accept line 90
  13. theorem OAI.TuringRigidity.UniformSplit.accept_recursive line 98
  14. theorem OAI.TuringRigidity.UniformSplit.accept_total line 111
  15. def OAI.TuringRigidity.UniformSplit.step line 139
  16. theorem OAI.TuringRigidity.UniformSplit.step_recursive line 141
  17. theorem OAI.TuringRigidity.UniformSplit.step_spec line 145