OAI/Computability/Scheduling/ScheduleBounds.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeBoundedFunction line 10
  2. theorem OAI.ThreeMachine.StackCompiler.Poly.volumePredecessors line 18
  3. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeRank line 26
  4. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeReverseRank line 32
  5. theorem OAI.ThreeMachine.StackCompiler.fullSolve_small line 44
  6. theorem OAI.ThreeMachine.StackCompiler.scheduleMatrix_bound line 48
  7. theorem OAI.ThreeMachine.StackCompiler.bestMatrix_bound line 55
  8. theorem OAI.ThreeMachine.StackCompiler.answerMatrix_length line 73
  9. theorem OAI.ThreeMachine.StackCompiler.answerMatrix_bound line 85
  10. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSchedule line 109
  11. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeBest line 116
  12. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_triple_le line 133
  13. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_cardinalMap line 141
  14. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_cardinalValue line 143
  15. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_makeUniverse line 145
  16. def OAI.ThreeMachine.StackCompiler.Uniform.restrictCell line 148
  17. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_restrictTime line 151
  18. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_recode_input line 153
  19. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_scheduleMatrix line 159
  20. theorem OAI.ThreeMachine.StackCompiler.Costs.restrictCell line 170
  21. theorem OAI.ThreeMachine.StackCompiler.Costs.restrictTime line 185
  22. theorem OAI.ThreeMachine.StackCompiler.Costs.restrictTimeBound line 198
  23. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeRestricted line 213
  24. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFullSolve line 225
  25. abbrev OAI.ThreeMachine.StackCompiler.Uniform.PredecessorInput line 235
  26. def OAI.ThreeMachine.StackCompiler.Uniform.predecessorCell line 236
  27. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_predecessorCount line 238
  28. abbrev OAI.ThreeMachine.StackCompiler.Uniform.PredecessorsInput line 241
  29. def OAI.ThreeMachine.StackCompiler.Uniform.predecessorsBody line 242
  30. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_predecessors line 245
  31. theorem OAI.ThreeMachine.StackCompiler.Costs.predecessorCell line 249
  32. theorem OAI.ThreeMachine.StackCompiler.Costs.predecessorCount line 251
  33. theorem OAI.ThreeMachine.StackCompiler.Costs.predecessorsBody line 254
  34. theorem OAI.ThreeMachine.StackCompiler.Costs.predecessors line 256
  35. abbrev OAI.ThreeMachine.StackCompiler.Uniform.RankCellInput line 268
  36. def OAI.ThreeMachine.StackCompiler.Uniform.rankCellA line 269
  37. def OAI.ThreeMachine.StackCompiler.Uniform.rankCellB line 271
  38. def OAI.ThreeMachine.StackCompiler.Uniform.rankCellLT line 273
  39. def OAI.ThreeMachine.StackCompiler.Uniform.rankCellEQ line 274
  40. def OAI.ThreeMachine.StackCompiler.Uniform.rankCellFinLT line 275
  41. def OAI.ThreeMachine.StackCompiler.Uniform.rankCell line 277
  42. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_rankFromCounts line 278
  43. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_natLT_le line 288
  44. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_finVal line 297