OAI/Computability/Scheduling/PriorityUpdates.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.Structure.pairCode_lt line 11
  2. def OAI.ThreeMachine.Structure.GlobalList.keyValue line 28
  3. theorem OAI.ThreeMachine.Structure.GlobalList.keyValue_lt_iff line 31
  4. theorem OAI.ThreeMachine.Structure.GlobalList.keyValue_injective line 36
  5. theorem OAI.ThreeMachine.Structure.GlobalList.lastIndex_le_sup line 50
  6. theorem OAI.ThreeMachine.Structure.GlobalList.keyValue_bound line 56
  7. theorem OAI.ThreeMachine.Structure.GlobalList.carryNumeric_selection line 66
  8. def OAI.ThreeMachine.Structure.GlobalList.samePriority line 95
  9. theorem OAI.ThreeMachine.Structure.GlobalList.samePriority_injective line 101
  10. theorem OAI.ThreeMachine.Structure.GlobalList.samePriority_extends line 135
  11. theorem OAI.ThreeMachine.Structure.GlobalList.samePriority_key line 166
  12. theorem OAI.ThreeMachine.Structure.GlobalList.samePriority_cut line 173
  13. def OAI.ThreeMachine.Structure.switchPriority line 203
  14. theorem OAI.ThreeMachine.Structure.switchPriority_injective line 207
  15. theorem OAI.ThreeMachine.Structure.switchPriority_extends line 221
  16. theorem OAI.ThreeMachine.Structure.switchPriority_cut line 239
  17. theorem OAI.ThreeMachine.Structure.GlobalList.pair_lastIndex_right line 252
  18. theorem OAI.ThreeMachine.Structure.GlobalList.pair_lastIndex_left line 263
  19. theorem OAI.ThreeMachine.Structure.GlobalList.switchPair_agreement line 274
  20. theorem OAI.ThreeMachine.Structure.GlobalList.switchPair_key line 286
  21. structure OAI.ThreeMachine.Structure.ReverseSeed line 316
  22. theorem OAI.ThreeMachine.Structure.reverse_seed_at_edge line 326
  23. def OAI.ThreeMachine.Structure.ReverseSeed.reorder line 387
  24. structure OAI.ThreeMachine.Structure.AtomSupport line 405
  25. theorem OAI.ThreeMachine.Structure.RunData.qual_small line 418
  26. theorem OAI.ThreeMachine.Structure.RunData.carry_cutoff_small line 432
  27. theorem OAI.ThreeMachine.Structure.RunData.carry_low_extension line 439
  28. theorem OAI.ThreeMachine.Structure.global_child_small line 459
  29. def OAI.ThreeMachine.Structure.GlobalList.sameUpdate line 485
  30. theorem OAI.ThreeMachine.Structure.GlobalList.carry_qual_subset line 489
  31. theorem OAI.ThreeMachine.Structure.GlobalList.sameUpdate_agreement line 494
  32. theorem OAI.ThreeMachine.Structure.GlobalList.sameUpdate_disjoint line 511
  33. theorem OAI.ThreeMachine.Structure.GlobalList.sameUpdate_upsets line 519
  34. theorem OAI.ThreeMachine.Structure.GlobalList.sameUpdate_key line 528
  35. theorem OAI.ThreeMachine.Structure.Boundary.desc_eq_of_interior line 586
  36. theorem OAI.ThreeMachine.Structure.sameUpdate_past line 594
  37. theorem OAI.ThreeMachine.Structure.sameUpdate_swap_inherited line 671