OAI/Computability/Scheduling/CutoffSimplification.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.Structure.GlobalList.append line 11
  2. def OAI.ThreeMachine.Structure.GlobalList.nextIndex line 16
  3. theorem OAI.ThreeMachine.Structure.GlobalList.lt_nextIndex line 18
  4. theorem OAI.ThreeMachine.Structure.GlobalList.nextIndex_not_mem line 25
  5. theorem OAI.ThreeMachine.Structure.GlobalList.append_membership line 29
  6. theorem OAI.ThreeMachine.Structure.GlobalList.append_qual line 41
  7. theorem OAI.ThreeMachine.Structure.GlobalList.append_upsets line 56
  8. theorem OAI.ThreeMachine.Structure.GlobalList.append_lastIndex_of_mem line 68
  9. theorem OAI.ThreeMachine.Structure.GlobalList.append_lastIndex_of_not_mem line 79
  10. theorem OAI.ThreeMachine.Structure.GlobalList.append_key_of_not_mem line 86
  11. theorem OAI.ThreeMachine.Structure.GlobalList.append_old_before_new line 91
  12. theorem OAI.ThreeMachine.Structure.GlobalList.injection_card_bound line 98
  13. def OAI.ThreeMachine.Structure.Window line 131
  14. theorem OAI.ThreeMachine.Structure.Boundary.pred_subset_weakPred line 135
  15. theorem OAI.ThreeMachine.Structure.Boundary.desc_subset_weakDesc line 142
  16. def OAI.ThreeMachine.Structure.Boundary.Separates line 149
  17. def OAI.ThreeMachine.Structure.Boundary.before line 154
  18. theorem OAI.ThreeMachine.Structure.Boundary.separates_description line 157
  19. theorem OAI.ThreeMachine.Structure.Boundary.separates_congr line 181
  20. theorem OAI.ThreeMachine.Structure.Boundary.left_separates line 192
  21. theorem OAI.ThreeMachine.Structure.Boundary.right_separates line 196
  22. theorem OAI.ThreeMachine.Structure.Boundary.actual_separates line 204
  23. def OAI.ThreeMachine.Structure.PastInvariant line 214
  24. theorem OAI.ThreeMachine.Structure.past_prune line 218
  25. theorem OAI.ThreeMachine.Structure.global_high_identity line 224
  26. theorem OAI.ThreeMachine.Structure.global_low_identity line 247
  27. def OAI.ThreeMachine.Structure.SwitchSet line 299
  28. theorem OAI.ThreeMachine.Structure.switchSet_upset line 302
  29. theorem OAI.ThreeMachine.Structure.switchSet_properties line 309
  30. theorem OAI.ThreeMachine.Structure.flatten_pair line 356