OAI/Computability/Scheduling/SchedulingAlgorithm.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.Algorithm.closureStep line 11
  2. def OAI.ThreeMachine.Algorithm.closureTable line 14
  3. def OAI.ThreeMachine.Algorithm.reachable line 17
  4. instance OAI.ThreeMachine.Algorithm.(instance at line 19) line 19
  5. theorem OAI.ThreeMachine.Algorithm.closureTable_zero line 22
  6. theorem OAI.ThreeMachine.Algorithm.closureTable_succ line 23
  7. theorem OAI.ThreeMachine.Algorithm.closureStep_mono line 27
  8. theorem OAI.ThreeMachine.Algorithm.closureTable_mono line 30
  9. theorem OAI.ThreeMachine.Algorithm.closureTable_sound line 41
  10. theorem OAI.ThreeMachine.Algorithm.walk_closure line 52
  11. theorem OAI.ThreeMachine.Algorithm.transGen_walk line 71
  12. theorem OAI.ThreeMachine.Algorithm.reachable_iff line 77
  13. def OAI.ThreeMachine.Structure.Atomic.finsetEval line 99
  14. theorem OAI.ThreeMachine.Structure.Atomic.coe_finsetEval line 115
  15. instance OAI.ThreeMachine.Structure.Atomic.decideEval line 126
  16. def OAI.ThreeMachine.Structure.Formula.evalFinset line 133
  17. theorem OAI.ThreeMachine.Structure.Formula.coe_evalFinset line 138
  18. def OAI.ThreeMachine.Structure.effectiveFamily line 144
  19. theorem OAI.ThreeMachine.Structure.effectiveFamily_complete line 151
  20. theorem OAI.ThreeMachine.Structure.effectiveFamily_length line 170
  21. instance OAI.ThreeMachine.(instance at line 180) line 180
  22. def OAI.ThreeMachine.Algorithm.fullSolve line 188
  23. theorem OAI.ThreeMachine.Algorithm.fullSolve_sound line 193
  24. theorem OAI.ThreeMachine.Algorithm.fullSolve_complete line 197
  25. theorem OAI.ThreeMachine.Algorithm.reachable_trans line 215
  26. theorem OAI.ThreeMachine.Algorithm.reachable_irrefl line 221
  27. def OAI.ThreeMachine.Algorithm.scheduleAt line 224
  28. theorem OAI.ThreeMachine.Algorithm.Block.restrict_feasible line 230
  29. theorem OAI.ThreeMachine.Algorithm.scheduleAt_sound line 260
  30. theorem OAI.ThreeMachine.Algorithm.scheduleAt_complete line 268
  31. theorem OAI.ThreeMachine.Algorithm.scheduleAt_none_iff line 281
  32. def OAI.ThreeMachine.Algorithm.best line 298
  33. def OAI.ThreeMachine.Algorithm.BestSpec line 304
  34. theorem OAI.ThreeMachine.Algorithm.best_spec line 309
  35. theorem OAI.ThreeMachine.Algorithm.serial_feasible line 341
  36. theorem OAI.ThreeMachine.Algorithm.best_optimum line 354
  37. def OAI.ThreeMachine.Algorithm.output line 375
  38. theorem OAI.ThreeMachine.Algorithm.output_correct line 379