OAI/Computability/Scheduling/SolverCosts.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Costs.tryW line 12
  2. theorem OAI.ThreeMachine.StackCompiler.Costs.tryL line 20
  3. theorem OAI.ThreeMachine.StackCompiler.Costs.tryP line 28
  4. theorem OAI.ThreeMachine.StackCompiler.Costs.tryDiff line 38
  5. theorem OAI.ThreeMachine.StackCompiler.Costs.tryO line 48
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.tryWork line 57
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.tryAdvance line 77
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.finishing line 102
  9. abbrev OAI.ThreeMachine.StackCompiler.Uniform.SolveInput line 127
  10. def OAI.ThreeMachine.StackCompiler.Uniform.solveU line 129
  11. def OAI.ThreeMachine.StackCompiler.Uniform.solveM line 130
  12. def OAI.ThreeMachine.StackCompiler.Uniform.solveT line 131
  13. def OAI.ThreeMachine.StackCompiler.Uniform.solveF line 132
  14. def OAI.ThreeMachine.StackCompiler.Uniform.solveZ line 133
  15. def OAI.ThreeMachine.StackCompiler.Uniform.solveW line 134
  16. def OAI.ThreeMachine.StackCompiler.Uniform.solveS line 135
  17. def OAI.ThreeMachine.StackCompiler.Uniform.solveMarks line 137
  18. def OAI.ThreeMachine.StackCompiler.Uniform.solveOut line 139
  19. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_solve line 142
  20. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSolve line 148
  21. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSolveOut line 164