OAI/Computability/Scheduling/DynamicProgram.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThreeMachine.Algorithm.Block line 10
  2. def OAI.ThreeMachine.Algorithm.Block.Valid line 17
  3. def OAI.ThreeMachine.Algorithm.Block.empty line 20
  4. def OAI.ThreeMachine.Algorithm.Block.triple line 21
  5. def OAI.ThreeMachine.Algorithm.Block.append line 22
  6. theorem OAI.ThreeMachine.Algorithm.Block.valid_empty line 26
  7. theorem OAI.ThreeMachine.Algorithm.Block.valid_triple line 37
  8. theorem OAI.ThreeMachine.Algorithm.Block.valid_append line 41
  9. theorem OAI.ThreeMachine.Algorithm.Block.Valid.of_eq line 61
  10. structure OAI.ThreeMachine.Algorithm.State line 66
  11. def OAI.ThreeMachine.Algorithm.State.candidate line 75
  12. def OAI.ThreeMachine.Algorithm.State.Compatible line 78
  13. instance OAI.ThreeMachine.Algorithm.State.(instance at line 87) line 87
  14. def OAI.ThreeMachine.Algorithm.State.upto line 90
  15. def OAI.ThreeMachine.Algorithm.State.advance line 92
  16. def OAI.ThreeMachine.Algorithm.State.finish line 95
  17. theorem OAI.ThreeMachine.Algorithm.State.Compatible.left_subset line 98
  18. theorem OAI.ThreeMachine.Algorithm.State.Compatible.right_subset line 104
  19. def OAI.ThreeMachine.Algorithm.State.toSplit line 109
  20. theorem OAI.ThreeMachine.Algorithm.State.valid_advance line 131
  21. theorem OAI.ThreeMachine.Algorithm.State.valid_finish line 153
  22. theorem OAI.ThreeMachine.Algorithm.State.left_card_strict line 166
  23. def OAI.ThreeMachine.Algorithm.lookup line 178
  24. def OAI.ThreeMachine.Algorithm.Has line 182
  25. theorem OAI.ThreeMachine.Algorithm.lookup_mem line 185
  26. theorem OAI.ThreeMachine.Algorithm.has_iff_mem line 198
  27. def OAI.ThreeMachine.Algorithm.firstResult line 215
  28. theorem OAI.ThreeMachine.Algorithm.firstResult_some line 221
  29. theorem OAI.ThreeMachine.Algorithm.firstResult_has line 234
  30. def OAI.ThreeMachine.Algorithm.tableOf line 256
  31. theorem OAI.ThreeMachine.Algorithm.mem_tableOf line 259
  32. theorem OAI.ThreeMachine.Algorithm.has_tableOf line 273
  33. inductive OAI.ThreeMachine.Algorithm.Walk line 278
  34. theorem OAI.ThreeMachine.Algorithm.Walk.of_path line 285
  35. theorem OAI.ThreeMachine.Algorithm.Walk.rank_bound line 290
  36. def OAI.ThreeMachine.Algorithm.states line 304
  37. def OAI.ThreeMachine.Algorithm.tryAdvance line 307
  38. def OAI.ThreeMachine.Algorithm.expand line 311
  39. def OAI.ThreeMachine.Algorithm.markings line 317
  40. def OAI.ThreeMachine.Algorithm.solve line 322
  41. def OAI.ThreeMachine.Algorithm.layers line 328
  42. def OAI.ThreeMachine.Algorithm.TableGood line 332
  43. def OAI.ThreeMachine.Algorithm.MarksGood line 335
  44. theorem OAI.ThreeMachine.Algorithm.states_compatible line 338
  45. theorem OAI.ThreeMachine.Algorithm.markings_good line 343
  46. theorem OAI.ThreeMachine.Algorithm.solve_good line 370
  47. theorem OAI.ThreeMachine.Algorithm.layers_good line 386
  48. theorem OAI.ThreeMachine.Algorithm.markings_stay line 399
  49. theorem OAI.ThreeMachine.Algorithm.markings_mono line 407
  50. theorem OAI.ThreeMachine.Algorithm.markings_step line 417
  51. def OAI.ThreeMachine.Algorithm.Arc line 431
  52. theorem OAI.ThreeMachine.Algorithm.markings_walk line 435
  53. theorem OAI.ThreeMachine.Algorithm.solve_complete_path line 442
  54. theorem OAI.ThreeMachine.Algorithm.State.ext line 473
  55. def OAI.ThreeMachine.Algorithm.State.erase line 482
  56. theorem OAI.ThreeMachine.Algorithm.State.erase_compatible line 485
  57. theorem OAI.ThreeMachine.Algorithm.State.erase_candidate line 508
  58. theorem OAI.ThreeMachine.Algorithm.State.erase_mem_states line 522
  59. theorem OAI.ThreeMachine.Algorithm.State.erase_inclusion line 533
  60. theorem OAI.ThreeMachine.Algorithm.State.erase_gap line 543
  61. theorem OAI.ThreeMachine.Algorithm.layers_complete line 559