OAI/Computability/Scheduling/MatrixCosts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Costs.solveS line 13
  2. theorem OAI.ThreeMachine.StackCompiler.Costs.solveMarks line 24
  3. theorem OAI.ThreeMachine.StackCompiler.Costs.solveOut line 45
  4. theorem OAI.ThreeMachine.StackCompiler.Costs.solve line 82
  5. abbrev OAI.ThreeMachine.StackCompiler.Uniform.LayerEnv line 100
  6. def OAI.ThreeMachine.StackCompiler.Uniform.layerBody line 101
  7. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_layerStep line 106
  8. theorem OAI.ThreeMachine.StackCompiler.layerStep_iterate line 112
  9. theorem OAI.ThreeMachine.StackCompiler.Costs.layerBody line 125
  10. theorem OAI.ThreeMachine.StackCompiler.volume_list_getD_le line 144
  11. theorem OAI.ThreeMachine.StackCompiler.volume_list_getElem?_le line 154
  12. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_getElemD_le line 162
  13. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_matrixRows line 170
  14. theorem OAI.ThreeMachine.StackCompiler.Costs.matrixReadNat line 179
  15. def OAI.ThreeMachine.StackCompiler.Uniform.paddedCell line 199
  16. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_paddedMatrix line 203
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.paddedCell line 207
  18. theorem OAI.ThreeMachine.StackCompiler.Costs.paddedMatrix line 220