OAI/Combinatorics/RamseyFive/Trees/PivotTree.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.PivotTree.balanced line 10
  2. def OAI.SharpRamseyFive.PivotTree.inorder line 16
  3. lemma OAI.SharpRamseyFive.PivotTree.balanced_nodes line 20
  4. lemma OAI.SharpRamseyFive.PivotTree.balanced_height line 29
  5. lemma OAI.SharpRamseyFive.PivotTree.balanced_inorder line 46
  6. def OAI.SharpRamseyFive.PivotTree.rootValue line 59
  7. def OAI.SharpRamseyFive.PivotTree.total line 63
  8. def OAI.SharpRamseyFive.PivotTree.Controls line 67
  9. lemma OAI.SharpRamseyFive.PivotTree.root_nonneg line 72
  10. theorem OAI.SharpRamseyFive.PivotTree.total_le_height line 78
  11. def OAI.SharpRamseyFive.PivotTree.prune line 95
  12. lemma OAI.SharpRamseyFive.PivotTree.prune_height line 99
  13. lemma OAI.SharpRamseyFive.PivotTree.prune_nodes line 109
  14. def OAI.SharpRamseyFive.TreeCodec.Tape line 128
  15. instance OAI.SharpRamseyFive.TreeCodec.tapeFintype line 132
  16. def OAI.SharpRamseyFive.TreeCodec.Message line 142
  17. instance OAI.SharpRamseyFive.TreeCodec.messageFintype line 147
  18. def OAI.SharpRamseyFive.TreeCodec.encoded line 158
  19. def OAI.SharpRamseyFive.TreeCodec.retained line 165
  20. lemma OAI.SharpRamseyFive.TreeCodec.retained_nodes_le line 174
  21. def OAI.SharpRamseyFive.TreeCodec.cost line 185
  22. def OAI.SharpRamseyFive.TreeCodec.tapeLaw line 193