OAI/Computability/BinPacking/Trees/TreeColorCounts.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.phaseQuota line 17
  2. theorem OAI.BinPackingGap.phaseQuota_succ line 19
  3. theorem OAI.BinPackingGap.phaseQuota_pos line 22
  4. def OAI.BinPackingGap.shiftedPhaseQuota line 25
  5. theorem OAI.BinPackingGap.shiftedPhaseQuota_add line 27
  6. theorem OAI.BinPackingGap.shiftedPhaseQuota_pos line 31
  7. theorem OAI.BinPackingGap.sum_phaseQuota_add_one line 34
  8. theorem OAI.BinPackingGap.sum_phaseQuota line 47
  9. theorem OAI.BinPackingGap.sum_phaseQuota_lt line 52
  10. theorem OAI.BinPackingGap.sum_phaseQuota_initial_add_tail line 57
  11. theorem OAI.BinPackingGap.sum_phaseQuota_tail line 72
  12. def OAI.BinPackingGap.continuationCount line 79
  13. theorem OAI.BinPackingGap.continuationCount_pos line 82
  14. theorem OAI.BinPackingGap.continuationCount_self line 86
  15. theorem OAI.BinPackingGap.continuationCount_eq line 89
  16. theorem OAI.BinPackingGap.card_rank_window_eq line 97
  17. theorem OAI.BinPackingGap.card_rank_window_le line 132
  18. theorem OAI.BinPackingGap.card_rank_interval_le line 141
  19. theorem OAI.BinPackingGap.card_rank_initial_lt_pow line 150
  20. theorem OAI.BinPackingGap.card_rank_tail_lt_continuations line 158
  21. theorem OAI.BinPackingGap.card_length_interval_le line 170
  22. def OAI.BinPackingGap.ForkGadget.spine line 185
  23. def OAI.BinPackingGap.ForkGadget.continuation line 187
  24. def OAI.BinPackingGap.ForkGadget.leafWord line 190
  25. def OAI.BinPackingGap.ForkGadget.leaves line 192
  26. theorem OAI.BinPackingGap.ForkGadget.spine_length line 196
  27. theorem OAI.BinPackingGap.ForkGadget.continuation_length line 201
  28. theorem OAI.BinPackingGap.ForkGadget.leafWord_length line 210
  29. theorem OAI.BinPackingGap.ForkGadget.spine_injective line 215
  30. theorem OAI.BinPackingGap.ForkGadget.leafWord_positive line 220
  31. theorem OAI.BinPackingGap.ForkGadget.leafWord_mem line 233
  32. theorem OAI.BinPackingGap.ForkGadget.mem_leaves_iff line 238
  33. def OAI.BinPackingGap.ForkGadget.tree line 250
  34. theorem OAI.BinPackingGap.ForkGadget.tree_height line 264
  35. def OAI.BinPackingGap.ForkGadget.red line 267
  36. def OAI.BinPackingGap.ForkGadget.blue line 270
  37. theorem OAI.BinPackingGap.ForkGadget.two_mul_phaseQuota line 273
  38. theorem OAI.BinPackingGap.ForkGadget.card_red line 277
  39. theorem OAI.BinPackingGap.ForkGadget.card_blue line 280
  40. theorem OAI.BinPackingGap.ForkGadget.red_depth line 285
  41. theorem OAI.BinPackingGap.ForkGadget.blue_depth line 290
  42. theorem OAI.BinPackingGap.ForkGadget.root_not_red line 295
  43. theorem OAI.BinPackingGap.ForkGadget.root_not_blue line 301
  44. theorem OAI.BinPackingGap.ForkGadget.red_blue_disjoint line 307
  45. theorem OAI.BinPackingGap.ForkGadget.spine_mem_vertices line 317
  46. theorem OAI.BinPackingGap.ForkGadget.red_subset line 323
  47. theorem OAI.BinPackingGap.ForkGadget.blue_subset line 333
  48. theorem OAI.BinPackingGap.ForkGadget.level_le_of_single_depth line 339
  49. theorem OAI.BinPackingGap.ForkGadget.red_level line 351
  50. theorem OAI.BinPackingGap.ForkGadget.blue_level line 355
  51. theorem OAI.BinPackingGap.ForkGadget.spine_prefix_leafWord_iff line 359
  52. theorem OAI.BinPackingGap.ForkGadget.colorCount_spines line 371
  53. theorem OAI.BinPackingGap.ForkGadget.red_count line 395
  54. theorem OAI.BinPackingGap.ForkGadget.blue_count line 400
  55. theorem OAI.BinPackingGap.ForkGadget.total_count line 406
  56. theorem OAI.BinPackingGap.ForkGadget.red_witness line 412
  57. theorem OAI.BinPackingGap.ForkGadget.blue_witness line 418
  58. theorem OAI.BinPackingGap.ForkGadget.avoids line 428
  59. def OAI.BinPackingGap.ForkGadget.auxiliary line 495
  60. theorem OAI.BinPackingGap.ForkGadget.auxiliary_height line 515
  61. theorem OAI.BinPackingGap.ForkGadget.auxiliary_quota line 518
  62. theorem OAI.BinPackingGap.ForkGadget.auxiliary_red_depth line 521
  63. theorem OAI.BinPackingGap.ForkGadget.auxiliary_blue_depth line 525
  64. theorem OAI.BinPackingGap.ForkGadget.auxiliary_card_red line 529
  65. theorem OAI.BinPackingGap.ForkGadget.auxiliary_card_blue line 532
  66. theorem OAI.BinPackingGap.UniformTree.marking_card_le line 541
  67. theorem OAI.BinPackingGap.CompetingTrees.markingPlus_card_le line 565
  68. theorem OAI.BinPackingGap.CompetingTrees.markingMinus_card_le line 572
  69. def OAI.BinPackingGap.UniformTree.liftMarks line 584
  70. theorem OAI.BinPackingGap.UniformTree.mem_liftMarks line 587
  71. theorem OAI.BinPackingGap.UniformTree.root_not_mem_lift line 599
  72. theorem OAI.BinPackingGap.UniformTree.height_lt_length_of_mem_lift line 608
  73. theorem OAI.BinPackingGap.UniformTree.liftMarks_subset_graft_vertices line 618
  74. theorem OAI.BinPackingGap.UniformTree.old_marks_disjoint_lift line 626
  75. theorem OAI.BinPackingGap.UniformTree.liftMarks_disjoint line 635
  76. theorem OAI.BinPackingGap.UniformTree.union_liftMarks_disjoint line 648
  77. theorem OAI.BinPackingGap.UniformTree.filter_liftMarks_prefix line 666
  78. theorem OAI.BinPackingGap.UniformTree.colorCount_liftMarks line 684
  79. theorem OAI.BinPackingGap.UniformTree.colorCount_union_liftMarks line 691
  80. theorem OAI.BinPackingGap.UniformTree.levelCount_liftMarks_eq_zero line 709
  81. theorem OAI.BinPackingGap.UniformTree.levelCount_liftMarks_le line 719
  82. theorem OAI.BinPackingGap.UniformTree.levelCount_union_liftMarks line 756
  83. theorem OAI.BinPackingGap.UniformTree.levelCount_union_liftMarks_le line 784