OAI/Computability/MeanPayoff/PolynomialCosts.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.PolynomialCost line 10
  2. theorem OAI.MeanPayoff.TreeDevice.LinearCost.polynomial line 13
  3. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.compose line 20
  4. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.pairMap line 46
  5. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.fanout line 72
  6. theorem OAI.MeanPayoff.TreeDevice.Fold.time_le line 81
  7. theorem OAI.MeanPayoff.TreeDevice.Fold.polynomial line 106
  8. theorem OAI.MeanPayoff.TreeDevice.LinearCost.recode line 138
  9. theorem OAI.MeanPayoff.TreeDevice.LinearCost.pairSwap line 147
  10. theorem OAI.MeanPayoff.TreeDevice.LinearCost.nilPrefix line 150
  11. theorem OAI.MeanPayoff.TreeDevice.LinearCost.nilSuffix line 156
  12. theorem OAI.MeanPayoff.TreeDevice.LinearCost.cons line 159
  13. theorem OAI.MeanPayoff.TreeDevice.LinearCost.consAcc line 162
  14. theorem OAI.MeanPayoff.TreeDevice.Forest.literal_limit line 167
  15. theorem OAI.MeanPayoff.TreeDevice.LinearCost.constant line 180
  16. theorem OAI.MeanPayoff.TreeDevice.LinearCost.branch line 189
  17. theorem OAI.MeanPayoff.TreeDevice.LinearCost.not line 194
  18. theorem OAI.MeanPayoff.TreeDevice.LinearCost.tail line 197
  19. theorem OAI.MeanPayoff.TreeDevice.LinearCost.head line 208
  20. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.reverse line 226
  21. theorem OAI.MeanPayoff.TreeDevice.«Sort».carry_linear line 235
  22. theorem OAI.MeanPayoff.TreeDevice.«Sort».carry_size line 242
  23. theorem OAI.MeanPayoff.TreeDevice.«Sort».initial_linear line 249
  24. theorem OAI.MeanPayoff.TreeDevice.«Sort».insert_polynomial line 252
  25. theorem OAI.MeanPayoff.TreeDevice.«Sort».sort_polynomial line 257
  26. theorem OAI.MeanPayoff.TreeDevice.element_size_le line 270
  27. theorem OAI.MeanPayoff.TreeDevice.list_length_le_size line 280
  28. theorem OAI.MeanPayoff.TreeDevice.PolynomialCost.map line 285
  29. theorem OAI.MeanPayoff.TreeDevice.Median.halfStep_linear line 320
  30. theorem OAI.MeanPayoff.TreeDevice.Median.halfStep_size line 326
  31. theorem OAI.MeanPayoff.TreeDevice.Median.count_polynomial line 333
  32. theorem OAI.MeanPayoff.TreeDevice.Median.drop_polynomial line 341
  33. theorem OAI.MeanPayoff.TreeDevice.Median.polynomial line 347