OAI/Computability/BinPacking/Machines/GraphPackingJobEdge.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.GraphPackingProgram.endpointResultValues line 15
  2. def OAI.BinPackingGap.GraphPackingProgram.endpointResultTapes line 22
  3. theorem OAI.BinPackingGap.GraphPackingProgram.endpoint_frame_extra line 28
  4. theorem OAI.BinPackingGap.GraphPackingProgram.endpoint_extra_outside line 35
  5. theorem OAI.BinPackingGap.GraphPackingProgram.endpoint_exec line 39
  6. def OAI.BinPackingGap.GraphPackingProgram.endpointTimePolynomial line 127
  7. theorem OAI.BinPackingGap.GraphPackingProgram.endpoint_exec_polynomial line 130
  8. theorem OAI.BinPackingGap.GraphPackingProgram.endpoint_layout_exec line 154
  9. def OAI.BinPackingGap.GraphPackingJobs.repeatPhases line 207
  10. def OAI.BinPackingGap.GraphPackingJobs.repeatSetPolynomial line 217
  11. def OAI.BinPackingGap.GraphPackingJobs.repeatLoopPolynomial line 221
  12. def OAI.BinPackingGap.GraphPackingJobs.repeatWidthPolynomial line 226
  13. def OAI.BinPackingGap.GraphPackingJobs.repeatTimePolynomial line 230
  14. theorem OAI.BinPackingGap.GraphPackingJobs.repeatTimePolynomial_eval line 233
  15. theorem OAI.BinPackingGap.GraphPackingJobs.repeat_tally_bound line 240
  16. theorem OAI.BinPackingGap.GraphPackingJobs.repeat_exec line 250
  17. def OAI.BinPackingGap.GraphPackingJobs.prefixPhases line 368
  18. def OAI.BinPackingGap.GraphPackingJobs.prefixTimePolynomial line 373
  19. theorem OAI.BinPackingGap.GraphPackingJobs.prefixTimePolynomial_eval line 376
  20. theorem OAI.BinPackingGap.GraphPackingJobs.prepared_endpoint_registers line 381
  21. theorem OAI.BinPackingGap.GraphPackingJobs.right_after_left_registers line 388
  22. theorem OAI.BinPackingGap.GraphPackingJobs.endpoint_measure_le line 396
  23. theorem OAI.BinPackingGap.GraphPackingJobs.prefix_exec line 404
  24. def OAI.BinPackingGap.GraphPackingJobs.resultBase line 506
  25. theorem OAI.BinPackingGap.GraphPackingJobs.resultBase_endpoints line 510
  26. theorem OAI.BinPackingGap.GraphPackingJobs.resultBase_other line 514
  27. theorem OAI.BinPackingGap.GraphPackingJobs.resultBase_append line 519
  28. theorem OAI.BinPackingGap.GraphPackingJobs.resultBase_counter line 532
  29. theorem OAI.BinPackingGap.GraphPackingJobs.resultBase_nil line 550
  30. def OAI.BinPackingGap.GraphPackingJobs.edgeTimePolynomial line 556
  31. theorem OAI.BinPackingGap.GraphPackingJobs.edge_exec line 559