OAI/Combinatorics/TriangleRemoval/Coupling/HyperScanAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.hyperScanAction line 19
  2. def OAI.SharpTerminalLeave.hyperScan line 22
  3. theorem OAI.SharpTerminalLeave.hyperScan_append line 26
  4. theorem OAI.SharpTerminalLeave.hyperScan_singleton line 31
  5. theorem OAI.SharpTerminalLeave.hyperScanAction_subset line 35
  6. theorem OAI.SharpTerminalLeave.sorted_filter_lt_succ line 43
  7. theorem OAI.SharpTerminalLeave.clockOrder_level_singleton line 70
  8. theorem OAI.SharpTerminalLeave.levelDeletes_one line 84
  9. theorem OAI.SharpTerminalLeave.timeScan_eq_hyperScan_prefix line 91
  10. theorem OAI.SharpTerminalLeave.timeScan_eq_hyperScan line 118