OAI/Computability/Scheduling/GlobalBoundaries.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.Structure.GlobalUpset line 9
  2. def OAI.ThreeMachine.Structure.GlobalDownset line 12
  3. theorem OAI.ThreeMachine.Structure.GlobalUpset.inter line 15
  4. theorem OAI.ThreeMachine.Structure.GlobalUpset.union line 20
  5. theorem OAI.ThreeMachine.Structure.GlobalDownset.compl line 25
  6. structure OAI.ThreeMachine.Structure.GlobalList line 30
  7. def OAI.ThreeMachine.Structure.GlobalList.Qual line 37
  8. def OAI.ThreeMachine.Structure.GlobalList.Upsets line 39
  9. def OAI.ThreeMachine.Structure.GlobalList.memberships line 42
  10. def OAI.ThreeMachine.Structure.GlobalList.lastIndex line 46
  11. def OAI.ThreeMachine.Structure.GlobalList.KeyLT line 49
  12. theorem OAI.ThreeMachine.Structure.GlobalList.mem_memberships line 53
  13. theorem OAI.ThreeMachine.Structure.GlobalList.le_lastIndex line 58
  14. theorem OAI.ThreeMachine.Structure.GlobalList.lastIndex_mem line 62
  15. theorem OAI.ThreeMachine.Structure.GlobalList.qual_upset line 73
  16. theorem OAI.ThreeMachine.Structure.GlobalList.key_extends line 78
  17. def OAI.ThreeMachine.Structure.GlobalList.carry line 87
  18. theorem OAI.ThreeMachine.Structure.GlobalList.carry_membership line 92
  19. theorem OAI.ThreeMachine.Structure.GlobalList.carry_selection line 102
  20. theorem OAI.ThreeMachine.Structure.GlobalList.carry_lastIndex line 127
  21. theorem OAI.ThreeMachine.Structure.GlobalList.carry_key line 146
  22. theorem OAI.ThreeMachine.Structure.GlobalList.carry_upsets line 151
  23. def OAI.ThreeMachine.Structure.GlobalList.prune line 165
  24. theorem OAI.ThreeMachine.Structure.GlobalList.prune_membership line 169
  25. theorem OAI.ThreeMachine.Structure.GlobalList.prune_qual_subset line 179
  26. theorem OAI.ThreeMachine.Structure.GlobalList.prune_qual line 184
  27. theorem OAI.ThreeMachine.Structure.GlobalList.prune_lastIndex_le line 192
  28. theorem OAI.ThreeMachine.Structure.GlobalList.prune_lastIndex line 199
  29. theorem OAI.ThreeMachine.Structure.GlobalList.prune_key line 208
  30. theorem OAI.ThreeMachine.Structure.GlobalList.prune_upsets line 218
  31. def OAI.ThreeMachine.Structure.Layout.FixedOutside line 232
  32. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.refl line 235
  33. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.trans line 238
  34. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.mono line 242
  35. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.time line 246
  36. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.symm_position line 250
  37. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.position_mem line 256
  38. theorem OAI.ThreeMachine.Structure.Layout.FixedOutside.time_range line 264
  39. theorem OAI.ThreeMachine.Structure.reorder_respects line 270
  40. def OAI.ThreeMachine.Structure.Layout.NormalizedOn line 293
  41. theorem OAI.ThreeMachine.Structure.exists_normalizedOn line 298
  42. theorem OAI.ThreeMachine.Structure.normalizedOn_no_improvement line 311
  43. theorem OAI.ThreeMachine.Structure.exchange_fixedOutside line 321
  44. theorem OAI.ThreeMachine.Structure.normalizedOn_prefix_no_exchange line 328
  45. theorem OAI.ThreeMachine.Structure.normalizedOn_local_obstruction line 363
  46. abbrev OAI.ThreeMachine.Structure.Triple line 398
  47. inductive OAI.ThreeMachine.Structure.Boundary line 400
  48. def OAI.ThreeMachine.Structure.Boundary.pred line 408
  49. def OAI.ThreeMachine.Structure.Boundary.desc line 413
  50. def OAI.ThreeMachine.Structure.Boundary.weakPred line 418
  51. def OAI.ThreeMachine.Structure.Boundary.weakDesc line 423
  52. def OAI.ThreeMachine.Structure.Boundary.reverse line 428
  53. theorem OAI.ThreeMachine.Structure.Boundary.reverse_reverse line 433
  54. theorem OAI.ThreeMachine.Structure.Boundary.pred_reverse line 435
  55. theorem OAI.ThreeMachine.Structure.Boundary.desc_reverse line 438
  56. theorem OAI.ThreeMachine.Structure.Boundary.weakPred_reverse line 441
  57. theorem OAI.ThreeMachine.Structure.Boundary.weakDesc_reverse line 444
  58. theorem OAI.ThreeMachine.Structure.Boundary.pred_downset line 447
  59. theorem OAI.ThreeMachine.Structure.Boundary.desc_upset line 458
  60. theorem OAI.ThreeMachine.Structure.Boundary.weakPred_downset line 469
  61. theorem OAI.ThreeMachine.Structure.Boundary.weakDesc_upset line 481
  62. def OAI.ThreeMachine.Structure.Boundary.At line 493
  63. theorem OAI.ThreeMachine.Structure.Boundary.pred_time line 498
  64. theorem OAI.ThreeMachine.Structure.Boundary.desc_time line 511
  65. theorem OAI.ThreeMachine.Structure.Boundary.weakPred_time line 524
  66. theorem OAI.ThreeMachine.Structure.Boundary.weakDesc_time line 536
  67. theorem OAI.ThreeMachine.Structure.Boundary.mem_weak_at_time line 548
  68. theorem OAI.ThreeMachine.Structure.Boundary.actual_pred_eq line 556
  69. theorem OAI.ThreeMachine.Structure.Boundary.actual_desc_eq line 562
  70. inductive OAI.ThreeMachine.Structure.Formula line 570
  71. def OAI.ThreeMachine.Structure.Formula.leaves line 578
  72. def OAI.ThreeMachine.Structure.Formula.eval line 582
  73. def OAI.ThreeMachine.Structure.Formula.negate line 588
  74. theorem OAI.ThreeMachine.Structure.Formula.leaves_negate line 593
  75. theorem OAI.ThreeMachine.Structure.Formula.eval_negate line 598
  76. theorem OAI.ThreeMachine.Structure.Formula.leaves_pos line 608
  77. def OAI.ThreeMachine.Structure.Described line 615
  78. theorem OAI.ThreeMachine.Structure.Described.mono line 621
  79. theorem OAI.ThreeMachine.Structure.Described.atom line 625
  80. theorem OAI.ThreeMachine.Structure.Described.compl line 627
  81. theorem OAI.ThreeMachine.Structure.Described.inter line 631
  82. theorem OAI.ThreeMachine.Structure.Described.union line 637
  83. theorem OAI.ThreeMachine.Structure.Described.diff line 643
  84. theorem OAI.ThreeMachine.Structure.Described.finite_union line 646