OAI/Computability/BinPacking/Trees/TreePruning.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.BinPackingGap.UniformTree.decidableAncestor line 14
  2. def OAI.BinPackingGap.UniformTree.prune line 17
  3. theorem OAI.BinPackingGap.UniformTree.prune_height line 25
  4. theorem OAI.BinPackingGap.UniformTree.prune_leaves line 29
  5. theorem OAI.BinPackingGap.UniformTree.prune_vertices_subset line 33
  6. def OAI.BinPackingGap.UniformTree.pruneEmbedding line 40
  7. theorem OAI.BinPackingGap.UniformTree.pruneEmbedding_val line 46
  8. theorem OAI.BinPackingGap.UniformTree.pruneEmbedding_depth line 51
  9. theorem OAI.BinPackingGap.UniformTree.pruneEmbedding_ancestor line 56
  10. theorem OAI.BinPackingGap.UniformTree.pruneEmbedding_child line 62
  11. def OAI.BinPackingGap.UniformTree.projectMarks line 68
  12. theorem OAI.BinPackingGap.UniformTree.mem_projectMarks line 71
  13. theorem OAI.BinPackingGap.UniformTree.projectMarks_filter_card line 75
  14. theorem OAI.BinPackingGap.UniformTree.levelCount_projectMarks line 95
  15. theorem OAI.BinPackingGap.UniformTree.colorCount_projectMarks line 99
  16. theorem OAI.BinPackingGap.UniformTree.root_not_projectMarks line 103
  17. def OAI.BinPackingGap.UniformTree.retainMarks line 110
  18. theorem OAI.BinPackingGap.UniformTree.mem_retainMarks line 113
  19. theorem OAI.BinPackingGap.UniformTree.mem_project_retainMarks line 117
  20. theorem OAI.BinPackingGap.UniformTree.retainMarks_root_not_mem line 128
  21. theorem OAI.BinPackingGap.UniformTree.retainMarks_level_le line 132
  22. theorem OAI.BinPackingGap.UniformTree.retainMarks_leaf_count line 141
  23. structure OAI.BinPackingGap.CompetingTrees line 162
  24. def OAI.BinPackingGap.AuxiliaryTree.richLeaves line 193
  25. theorem OAI.BinPackingGap.AuxiliaryTree.richLeaves_subset line 197
  26. theorem OAI.BinPackingGap.AuxiliaryTree.richLeaves_nonempty line 201
  27. theorem OAI.BinPackingGap.AuxiliaryTree.richLeaves_cover line 208
  28. theorem OAI.BinPackingGap.AuxiliaryTree.height_pos line 216
  29. def OAI.BinPackingGap.AuxiliaryTree.richTree line 235
  30. theorem OAI.BinPackingGap.levelCount_project_union line 241
  31. def OAI.BinPackingGap.CompetingTrees.quotaTotal line 258
  32. theorem OAI.BinPackingGap.CompetingTrees.markingPlus_depth_pos line 261
  33. theorem OAI.BinPackingGap.CompetingTrees.markingMinus_depth_pos line 267
  34. def OAI.BinPackingGap.CompetingTrees.ofAuxiliary line 273