OAI/Computability/BinPacking/Machines/PackingCountMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.PackingCountMachine.Parameters line 11
  2. def OAI.BinPackingGap.PackingCountMachine.R line 17
  3. theorem OAI.BinPackingGap.PackingCountMachine.R_affine line 19
  4. def OAI.BinPackingGap.PackingCountMachine.B line 24
  5. theorem OAI.BinPackingGap.PackingCountMachine.B_accumulate line 26
  6. inductive OAI.BinPackingGap.PackingCountMachine.Phase line 31
  7. instance OAI.BinPackingGap.PackingCountMachine.(instance at line 38) line 38
  8. inductive OAI.BinPackingGap.PackingCountMachine.Label line 42
  9. abbrev OAI.BinPackingGap.PackingCountMachine.State line 47
  10. def OAI.BinPackingGap.PackingCountMachine.clean line 49
  11. def OAI.BinPackingGap.PackingCountMachine.affineIndices line 51
  12. def OAI.BinPackingGap.PackingCountMachine.productIndices line 57
  13. def OAI.BinPackingGap.PackingCountMachine.affineSlots line 61
  14. def OAI.BinPackingGap.PackingCountMachine.productSlots line 64
  15. def OAI.BinPackingGap.PackingCountMachine.coefficient line 66
  16. def OAI.BinPackingGap.PackingCountMachine.offset line 72
  17. def OAI.BinPackingGap.PackingCountMachine.phaseExit line 76
  18. def OAI.BinPackingGap.PackingCountMachine.instruction line 82
  19. def OAI.BinPackingGap.PackingCountMachine.resultTapes line 90
  20. theorem OAI.BinPackingGap.PackingCountMachine.resultTapes_other line 100
  21. def OAI.BinPackingGap.PackingCountMachine.steps line 106
  22. theorem OAI.BinPackingGap.PackingCountMachine.steps_eq line 110
  23. def OAI.BinPackingGap.PackingCountMachine.timePolynomial line 115
  24. theorem OAI.BinPackingGap.PackingCountMachine.steps_le_timePolynomial line 119
  25. theorem OAI.BinPackingGap.PackingCountMachine.graph_steps_le_timePolynomial line 138
  26. theorem OAI.BinPackingGap.PackingCountMachine.joinTrace line 143
  27. theorem OAI.BinPackingGap.PackingCountMachine.countTrace line 147
  28. def OAI.BinPackingGap.PackingCountMachine.countInTime line 250
  29. def OAI.BinPackingGap.PackingCountMachine.graphCountInTime line 267