OAI/Computability/BinPacking/Trees/TreeAvoidance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.pullMarks line 7
  2. theorem OAI.BinPackingGap.mem_pullMarks line 10
  3. theorem OAI.BinPackingGap.nil_mem_pullMarks line 29
  4. theorem OAI.BinPackingGap.levelCount_pullMarks_le line 33
  5. theorem OAI.BinPackingGap.disjoint_prefixes_append_of_pull line 45
  6. def OAI.BinPackingGap.extendPhaseQuota line 60
  7. theorem OAI.BinPackingGap.extendPhaseQuota_old line 63
  8. theorem OAI.BinPackingGap.extendPhaseQuota_new line 67
  9. theorem OAI.BinPackingGap.graft_avoids line 72