OAI/Computability/Scheduling/RankCosts.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Costs.rankCellLT line 10
  2. theorem OAI.ThreeMachine.StackCompiler.Costs.rankCellEQ line 12
  3. theorem OAI.ThreeMachine.StackCompiler.Costs.rankCellFinLT line 14
  4. theorem OAI.ThreeMachine.StackCompiler.Costs.rankCell line 18
  5. theorem OAI.ThreeMachine.StackCompiler.Costs.rankFromCounts line 30
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.rank line 37
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.reverseRank line 46
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.ranks line 50
  9. abbrev OAI.ThreeMachine.StackCompiler.Uniform.ThresholdInput line 64
  10. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdA line 65
  11. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdB line 67
  12. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdP line 68
  13. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdF line 73
  14. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdN line 76
  15. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_thresholdSets line 78
  16. theorem OAI.ThreeMachine.StackCompiler.Costs.thresholdP line 84
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.thresholdF line 89
  18. theorem OAI.ThreeMachine.StackCompiler.Costs.thresholdSets line 97
  19. def OAI.ThreeMachine.StackCompiler.Uniform.triplesE line 112
  20. def OAI.ThreeMachine.StackCompiler.Uniform.triplesA line 113
  21. def OAI.ThreeMachine.StackCompiler.Uniform.triplesP line 114
  22. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_triples line 116
  23. def OAI.ThreeMachine.StackCompiler.Uniform.conesF line 119
  24. def OAI.ThreeMachine.StackCompiler.Uniform.conesOne line 121
  25. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_cones_cons line 123
  26. theorem OAI.ThreeMachine.StackCompiler.Costs.matrixGetFrame line 130
  27. theorem OAI.ThreeMachine.StackCompiler.Costs.conePred line 135
  28. theorem OAI.ThreeMachine.StackCompiler.Costs.cone line 140
  29. theorem OAI.ThreeMachine.StackCompiler.Costs.triplesE line 147
  30. theorem OAI.ThreeMachine.StackCompiler.Costs.triplesA line 149
  31. theorem OAI.ThreeMachine.StackCompiler.Costs.triplesP line 151
  32. theorem OAI.ThreeMachine.StackCompiler.Costs.triples line 153
  33. theorem OAI.ThreeMachine.StackCompiler.Costs.conesF line 156
  34. theorem OAI.ThreeMachine.StackCompiler.Costs.conesOne line 159
  35. theorem OAI.ThreeMachine.StackCompiler.Costs.cones line 165