OAI/Combinatorics/TriangleRemoval/Process/LevelDeletes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.ExposureTree.evaluate_exposeLabeled line 18
  2. theorem OAI.SharpTerminalLeave.ExposureTree.evaluate_checkNone line 24
  3. def OAI.SharpTerminalLeave.levelDeletes line 37
  4. def OAI.SharpTerminalLeave.timeScan line 40
  5. theorem OAI.SharpTerminalLeave.mem_levelDeletes line 45
  6. theorem OAI.SharpTerminalLeave.timeScan_subset_initial line 52
  7. theorem OAI.SharpTerminalLeave.timeScan_mem_iff line 60
  8. theorem OAI.SharpTerminalLeave.evaluate_gridQueryDepth_succ line 87
  9. theorem OAI.SharpTerminalLeave.evaluate_gridQueryDepth_iff line 109