OAI/Computability/Scheduling/TableCosts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Uniform.tableBody line 11
  2. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_tableBody_le line 14
  3. theorem OAI.ThreeMachine.StackCompiler.volume_tableBody line 37
  4. theorem OAI.ThreeMachine.StackCompiler.Poly.tableOfTime line 44
  5. abbrev OAI.ThreeMachine.StackCompiler.Uniform.eval line 70
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.expandBody line 78
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.expand line 97
  8. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeExpand line 141
  9. def OAI.ThreeMachine.StackCompiler.Uniform.initialMarkBody line 172
  10. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_initialMarks line 174
  11. theorem OAI.ThreeMachine.StackCompiler.Costs.initialMarkBody line 179
  12. abbrev OAI.ThreeMachine.StackCompiler.Uniform.MarkEnv line 190
  13. def OAI.ThreeMachine.StackCompiler.Uniform.markingsStep line 191
  14. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_markings line 195
  15. theorem OAI.ThreeMachine.StackCompiler.markingsStep_iterate line 201
  16. theorem OAI.ThreeMachine.StackCompiler.Costs.initialMarks line 213
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.markingsStep line 231
  18. theorem OAI.ThreeMachine.StackCompiler.Costs.markings line 255