OAI/Combinatorics/UniformKServer/PrefixTree.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The full fixed finite wordPrefix universe. Its vertices include every formal wordPrefix, without deleting presently empty branches.

  1. abbrev OAI.UniformKServer.PrefixTree.Word line 16
  2. def OAI.UniformKServer.PrefixTree.root line 19
  3. def OAI.UniformKServer.PrefixTree.parent line 20
  4. def OAI.UniformKServer.PrefixTree.ranked line 24
  5. abbrev OAI.UniformKServer.PrefixTree.size line 48
  6. def OAI.UniformKServer.PrefixTree.shape line 49
  7. def OAI.UniformKServer.PrefixTree.chart line 50
  8. def OAI.UniformKServer.PrefixTree.wordPrefix line 52
  9. def OAI.UniformKServer.PrefixTree.atLevel line 54
  10. def OAI.UniformKServer.PrefixTree.endpoint line 56
  11. theorem OAI.UniformKServer.PrefixTree.depth_chart line 58
  12. theorem OAI.UniformKServer.PrefixTree.depth_at line 61
  13. theorem OAI.UniformKServer.PrefixTree.depth_bound line 65
  14. theorem OAI.UniformKServer.PrefixTree.at_nonzero line 69
  15. theorem OAI.UniformKServer.PrefixTree.prefix_parent line 76
  16. theorem OAI.UniformKServer.PrefixTree.at_parent line 82
  17. theorem OAI.UniformKServer.PrefixTree.at_descends line 89
  18. theorem OAI.UniformKServer.PrefixTree.endpoint_leaf line 96
  19. theorem OAI.UniformKServer.PrefixTree.ancestor_endpoint line 105
  20. theorem OAI.UniformKServer.PrefixTree.desc_endpoint line 109