OAI/Computability/Scheduling/HierarchySoundness.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThreeMachine.Structure.FullBlock line 11
  2. def OAI.ThreeMachine.Structure.FullBlock.empty line 22
  3. def OAI.ThreeMachine.Structure.FullBlock.triple line 30
  4. def OAI.ThreeMachine.Structure.FullBlock.append line 39
  5. theorem OAI.ThreeMachine.Structure.SplitVertex.gap_subset_right line 104
  6. theorem OAI.ThreeMachine.Structure.SplitVertex.left_union_gap line 111
  7. def OAI.ThreeMachine.Structure.SplitVertex.add_middle line 122
  8. def OAI.ThreeMachine.Structure.SplitVertex.advance line 126
  9. def OAI.ThreeMachine.Structure.SplitVertex.finish line 138
  10. theorem OAI.ThreeMachine.Structure.SplitVertex.path_sound line 149
  11. theorem OAI.ThreeMachine.Structure.AcceptedAt.sound line 161
  12. inductive OAI.ThreeMachine.Structure.Atomic line 179
  13. def OAI.ThreeMachine.Structure.Atomic.eval line 187
  14. theorem OAI.ThreeMachine.Structure.Atomic.eval_reversed line 201
  15. theorem OAI.ThreeMachine.Structure.Atomic.support line 213
  16. theorem OAI.ThreeMachine.Structure.Atomic.support_reverse line 253
  17. def OAI.ThreeMachine.Structure.rankOfKey line 283
  18. theorem OAI.ThreeMachine.Structure.rankOfKey_strict line 286
  19. theorem OAI.ThreeMachine.Structure.rankOfKey_bounds line 302
  20. theorem OAI.ThreeMachine.Structure.rankOfKey_injective line 314
  21. def OAI.ThreeMachine.Structure.predecessorCount line 329
  22. def OAI.ThreeMachine.Structure.jobKey line 331
  23. def OAI.ThreeMachine.Structure.jobRank line 333
  24. def OAI.ThreeMachine.Structure.reverseJobRank line 335
  25. theorem OAI.ThreeMachine.Structure.jobKey_injective line 337
  26. theorem OAI.ThreeMachine.Structure.jobRank_injective line 341
  27. theorem OAI.ThreeMachine.Structure.jobRank_bounds line 343
  28. theorem OAI.ThreeMachine.Structure.jobRank_strict line 346
  29. theorem OAI.ThreeMachine.Structure.reverseJobRank_bounds line 360
  30. theorem OAI.ThreeMachine.Structure.reverseJobRank_injective line 365
  31. theorem OAI.ThreeMachine.Structure.reverseJobRank_strict line 373
  32. theorem OAI.ThreeMachine.Structure.exists_slot_embedding line 388
  33. theorem OAI.ThreeMachine.Structure.exists_layout_time line 432
  34. theorem OAI.ThreeMachine.Structure.FullBlock.layout line 443
  35. theorem OAI.ThreeMachine.Structure.accepted_iff_full_layout line 453