OAI/Computability/Scheduling/FamilyCosts.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_finEmpty line 10
  2. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_finCons line 11
  3. def OAI.ThreeMachine.StackCompiler.Uniform.assignmentsInner line 14
  4. def OAI.ThreeMachine.StackCompiler.Uniform.assignmentsStep line 17
  5. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_assignments_succ line 19
  6. theorem OAI.ThreeMachine.StackCompiler.Costs.assignmentsInner line 26
  7. theorem OAI.ThreeMachine.StackCompiler.Costs.assignmentsStep line 39
  8. theorem OAI.ThreeMachine.StackCompiler.Costs.assignments line 57
  9. theorem OAI.ThreeMachine.StackCompiler.Costs.evalTemplate line 85
  10. theorem OAI.ThreeMachine.StackCompiler.Costs.evalTemplates line 92
  11. def OAI.ThreeMachine.StackCompiler.Uniform.atomSetsC line 107
  12. def OAI.ThreeMachine.StackCompiler.Uniform.atomSetsT line 109
  13. def OAI.ThreeMachine.StackCompiler.Uniform.atomSetsD line 110
  14. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_atomSets line 111
  15. theorem OAI.ThreeMachine.StackCompiler.Costs.lengthThresholds line 117
  16. theorem OAI.ThreeMachine.StackCompiler.Costs.lengthCones line 125
  17. theorem OAI.ThreeMachine.StackCompiler.Costs.thresholds line 136
  18. theorem OAI.ThreeMachine.StackCompiler.Costs.atomSetsC line 150
  19. theorem OAI.ThreeMachine.StackCompiler.Costs.atomSetsT line 152
  20. theorem OAI.ThreeMachine.StackCompiler.Costs.atomSetsD line 159
  21. theorem OAI.ThreeMachine.StackCompiler.Costs.atomSets line 164
  22. theorem OAI.ThreeMachine.StackCompiler.Costs.evalTemplatesCanonical line 174
  23. def OAI.ThreeMachine.StackCompiler.Uniform.familyAssignments line 182
  24. def OAI.ThreeMachine.StackCompiler.Uniform.familyEval line 183
  25. def OAI.ThreeMachine.StackCompiler.Uniform.familyFlatten line 184
  26. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_family line 185
  27. theorem OAI.ThreeMachine.StackCompiler.Costs.familyAssignments line 190
  28. theorem OAI.ThreeMachine.StackCompiler.Costs.familyEval line 203
  29. theorem OAI.ThreeMachine.StackCompiler.Costs.familyFlatten line 207
  30. theorem OAI.ThreeMachine.StackCompiler.Costs.familyBound line 223
  31. theorem OAI.ThreeMachine.StackCompiler.Costs.family line 237