OAI/Computability/Scheduling/SchedulingCosts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Costs.layerStep line 9
  2. theorem OAI.ThreeMachine.StackCompiler.Costs.layers line 44
  3. def OAI.ThreeMachine.StackCompiler.Uniform.fullLayers line 94
  4. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_fullSolveK line 100
  5. theorem OAI.ThreeMachine.StackCompiler.Costs.fullLayers line 106
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.fullSolveK line 122
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.fullSolve line 138
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.paddedSolve line 145
  9. def OAI.ThreeMachine.StackCompiler.Uniform.scheduleRestriction line 158
  10. def OAI.ThreeMachine.StackCompiler.Uniform.scheduleCandidate line 162
  11. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_scheduleMatrixFixed line 166
  12. theorem OAI.ThreeMachine.StackCompiler.Costs.scheduleRestriction line 174
  13. abbrev OAI.ThreeMachine.StackCompiler.Costs.ScheduleInput line 187
  14. theorem OAI.ThreeMachine.StackCompiler.Costs.candidateVolume line 188
  15. theorem OAI.ThreeMachine.StackCompiler.Costs.scheduleCandidate line 202
  16. theorem OAI.ThreeMachine.StackCompiler.Costs.scheduleMatrixFixed line 230
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.scheduleMatrix line 242