OAI/Computability/BinPacking/Computation/GraphIterationBounds.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.extraTapes line 11
  2. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.frame line 16
  3. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.trace_trans line 23
  4. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.start_eq line 27
  5. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.finish_eq line 40
  6. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.drainTrace line 50
  7. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.clockCopyTrace line 67
  8. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.archiveCopyTrace line 88
  9. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.reverseTrace line 110
  10. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.finishTrace line 135
  11. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterFinish.finishInTime line 150
  12. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.rawOutput line 165
  13. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.rawInTime line 168
  14. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.count line 192
  15. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.output line 194
  16. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.rowsBits line 197
  17. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 200
  18. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 204
  19. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 210
  20. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.inputBits line 230
  21. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.countedBits line 232
  22. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.words line 234
  23. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.count line 237
  24. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.lengthPolynomial line 239
  25. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.inputBits_le_countedBits line 242
  26. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.size_le_inputBits line 246
  27. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.count_le line 251
  28. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.intermediate_size line 255
  29. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.intermediate_bits line 263
  30. def OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial line 279
  31. theorem OAI.BinPackingGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial_eval line 283