OAI/Computability/Scheduling/OptimumCosts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThreeMachine.StackCompiler.Uniform.BestState line 9
  2. def OAI.ThreeMachine.StackCompiler.Uniform.bestNext line 10
  3. def OAI.ThreeMachine.StackCompiler.Uniform.bestAttempt line 12
  4. def OAI.ThreeMachine.StackCompiler.Uniform.bestRetain line 16
  5. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_bestMatrixStep line 21
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.bestNext line 30
  7. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_attach_le line 42
  8. theorem OAI.ThreeMachine.StackCompiler.Poly.compTimeSame line 72
  9. theorem OAI.ThreeMachine.StackCompiler.Poly.pairTimeSame line 82
  10. theorem OAI.ThreeMachine.StackCompiler.Costs.bestAttempt line 102
  11. theorem OAI.ThreeMachine.StackCompiler.Costs.bestRetain line 131
  12. theorem OAI.ThreeMachine.StackCompiler.Costs.bestMatrixStep line 150
  13. abbrev OAI.ThreeMachine.StackCompiler.Poly.StrictIterPool line 169
  14. theorem OAI.ThreeMachine.StackCompiler.Poly.iterateTimeStrict line 170
  15. theorem OAI.ThreeMachine.StackCompiler.Costs.bestMatrix line 192