OAI/Computability/Scheduling/StateCosts.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_setFilter line 11
  2. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_setEmpty line 15
  3. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_vectorMap line 17
  4. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_vectorMapAny line 21
  5. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_andD_le line 28
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.matrixGet line 44
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.finEq line 46
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.setMem line 58
  9. theorem OAI.ThreeMachine.StackCompiler.Costs.setSubset line 60
  10. theorem OAI.ThreeMachine.StackCompiler.Costs.setEq line 62
  11. theorem OAI.ThreeMachine.StackCompiler.Costs.setInter line 64
  12. theorem OAI.ThreeMachine.StackCompiler.Costs.setDiff line 66
  13. theorem OAI.ThreeMachine.StackCompiler.Costs.setDisjoint line 68
  14. def OAI.ThreeMachine.StackCompiler.Uniform.noEdgeTest line 73
  15. def OAI.ThreeMachine.StackCompiler.Uniform.noEdgeRow line 76
  16. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_noEdges line 81
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.noEdgeTest line 87
  18. theorem OAI.ThreeMachine.StackCompiler.Costs.noEdgeRow line 89
  19. theorem OAI.ThreeMachine.StackCompiler.Costs.noEdges line 91
  20. abbrev OAI.ThreeMachine.StackCompiler.Uniform.StateEqInput line 99
  21. def OAI.ThreeMachine.StackCompiler.Uniform.stateEqL line 100
  22. def OAI.ThreeMachine.StackCompiler.Uniform.stateEqM line 102
  23. def OAI.ThreeMachine.StackCompiler.Uniform.stateEqR line 104
  24. def OAI.ThreeMachine.StackCompiler.Uniform.stateEqMR line 106
  25. def OAI.ThreeMachine.StackCompiler.Uniform.stateEqLMR line 107
  26. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_stateEq line 108
  27. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEqL line 111
  28. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEqM line 113
  29. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEqR line 115
  30. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEqMR line 117
  31. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEqLMR line 119
  32. theorem OAI.ThreeMachine.StackCompiler.Costs.stateEq line 121
  33. theorem OAI.ThreeMachine.StackCompiler.Costs.setCard line 128
  34. theorem OAI.ThreeMachine.StackCompiler.Costs.setUnion line 130
  35. theorem OAI.ThreeMachine.StackCompiler.Costs.stateCandidate line 132
  36. theorem OAI.ThreeMachine.StackCompiler.Costs.stateUpto line 135
  37. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_stateCompatible line 139
  38. theorem OAI.ThreeMachine.StackCompiler.Costs.scLZ line 144
  39. theorem OAI.ThreeMachine.StackCompiler.Costs.scLZR line 146
  40. theorem OAI.ThreeMachine.StackCompiler.Costs.scA line 148
  41. theorem OAI.ThreeMachine.StackCompiler.Costs.scB line 150
  42. theorem OAI.ThreeMachine.StackCompiler.Costs.scC line 152
  43. theorem OAI.ThreeMachine.StackCompiler.Costs.scD line 154
  44. theorem OAI.ThreeMachine.StackCompiler.Costs.scE line 156
  45. theorem OAI.ThreeMachine.StackCompiler.Costs.scF line 158
  46. theorem OAI.ThreeMachine.StackCompiler.Costs.scH line 160
  47. theorem OAI.ThreeMachine.StackCompiler.Costs.scI line 162
  48. theorem OAI.ThreeMachine.StackCompiler.Costs.scJ line 164
  49. theorem OAI.ThreeMachine.StackCompiler.Costs.scIJ line 166
  50. theorem OAI.ThreeMachine.StackCompiler.Costs.scHIJ line 168
  51. theorem OAI.ThreeMachine.StackCompiler.Costs.scFHIJ line 170
  52. theorem OAI.ThreeMachine.StackCompiler.Costs.scEFHIJ line 172
  53. theorem OAI.ThreeMachine.StackCompiler.Costs.scDEFHIJ line 174
  54. theorem OAI.ThreeMachine.StackCompiler.Costs.scCDEFHIJ line 176
  55. theorem OAI.ThreeMachine.StackCompiler.Costs.scBCDEFHIJ line 178
  56. theorem OAI.ThreeMachine.StackCompiler.Costs.scAll line 180
  57. theorem OAI.ThreeMachine.StackCompiler.Costs.stateCompatible line 182
  58. theorem OAI.ThreeMachine.StackCompiler.Costs.blockEmpty line 185
  59. theorem OAI.ThreeMachine.StackCompiler.Costs.blockTriple line 187