OAI/Computability/MeanPayoff/CountedRecursion.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.SolveBox.repeatedCounted line 9
  2. abbrev OAI.MeanPayoff.CountedAlgorithm.LowerSolver line 15
  3. def OAI.MeanPayoff.CountedAlgorithm.centerUpdate line 19
  4. def OAI.MeanPayoff.CountedAlgorithm.centerSteps line 27
  5. def OAI.MeanPayoff.CountedAlgorithm.orientationTail line 36
  6. def OAI.MeanPayoff.CountedAlgorithm.orient line 50
  7. def OAI.MeanPayoff.CountedAlgorithm.orientPlus line 62
  8. def OAI.MeanPayoff.CountedAlgorithm.tighten line 66
  9. def OAI.MeanPayoff.CountedAlgorithm.finishChoice line 96
  10. def OAI.MeanPayoff.CountedAlgorithm.solveWidth line 113
  11. def OAI.MeanPayoff.CountedAlgorithm.solve line 135
  12. theorem OAI.MeanPayoff.SolveBox.erase_repeated line 144
  13. theorem OAI.MeanPayoff.SolveBox.bounded_repeated line 149
  14. def OAI.MeanPayoff.CountedAlgorithm.eraseLower line 156
  15. abbrev OAI.MeanPayoff.CountedAlgorithm.LowerBound line 159
  16. theorem OAI.MeanPayoff.CountedAlgorithm.erase_centerUpdate line 162
  17. theorem OAI.MeanPayoff.CountedAlgorithm.erase_centerSteps line 169
  18. theorem OAI.MeanPayoff.CountedAlgorithm.erase_orientationTail line 179
  19. theorem OAI.MeanPayoff.CountedAlgorithm.erase_orient line 188
  20. theorem OAI.MeanPayoff.CountedAlgorithm.erase_orientPlus line 203
  21. theorem OAI.MeanPayoff.CountedAlgorithm.erase_tighten line 208
  22. theorem OAI.MeanPayoff.CountedAlgorithm.erase_finishChoice line 239
  23. theorem OAI.MeanPayoff.CountedAlgorithm.erase_solveWidth line 249
  24. theorem OAI.MeanPayoff.CountedAlgorithm.erase_solve line 272