OAI/Computability/Scheduling/OutputCosts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_mapOption_linear line 11
  2. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_functionListOption_le line 28
  3. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_sndFunctionListOption_le line 37
  4. theorem OAI.ThreeMachine.StackCompiler.volume_optionFunctionList line 57
  5. theorem OAI.ThreeMachine.StackCompiler.volume_optionSndFunctionList_le line 60
  6. theorem OAI.ThreeMachine.StackCompiler.volume_instance line 70
  7. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeInstance line 73
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.edgePairEq line 83
  9. theorem OAI.ThreeMachine.StackCompiler.Costs.edgeAt line 86
  10. theorem OAI.ThreeMachine.StackCompiler.Costs.edgeMatrix line 94
  11. theorem OAI.ThreeMachine.StackCompiler.Costs.nextMatrixCell line 107
  12. theorem OAI.ThreeMachine.StackCompiler.Costs.nextMatrix line 110
  13. theorem OAI.ThreeMachine.StackCompiler.Costs.closureMatrixStep line 113
  14. theorem OAI.ThreeMachine.StackCompiler.Costs.reachMatrix line 117