OAI/Computability/BinPacking/Computation/MachineOverlayRows.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.State line 14
  2. inductive OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.Label line 16
  3. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.bodyIndex line 22
  4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.bodyIndex_injective line 24
  5. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.trueBits line 28
  6. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.instruction line 30
  7. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowBits line 45
  8. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowSteps line 48
  9. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.resultTapes line 52
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.joinTrace line 57
  11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowTrace line 61
  12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowBits_eq_expanderRow line 203
  13. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.machine line 216
  14. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.VertexLabel line 227
  15. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexInstruction line 229
  16. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.streamFrame line 239
  17. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.streamOutput line 244
  18. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexSteps line 247
  19. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.valueBound line 252
  20. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowSizeBound line 253
  21. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowCostBound line 254
  22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.value_le line 257
  23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowBits_length line 265
  24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowBits_length_le line 271
  25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.rowSteps_le line 278
  26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le_capacity line 288
  27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le line 313
  28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.streamFrame_afterRow line 320
  29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexSuffixTrace line 336
  30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexTrace line 410
  31. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexInTime line 426
  32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.encodeWords_flatMap line 448
  33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.streamOutput_expanderRows line 454
  34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.expanderValues_bounded line 466
  35. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayRows.vertexMachine line 471