OAI/Combinatorics/UniformKServer/RankedTree.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A finite ranked rooted tree is enumerated in increasing rank and converted to the ordered finite shapes used by the allocator and rounding proofs.

  1. structure OAI.UniformKServer.RankedTree.Data line 16
  2. def OAI.UniformKServer.RankedTree.size line 26
  3. theorem OAI.UniformKServer.RankedTree.size_card line 28
  4. def OAI.UniformKServer.RankedTree.orderKey line 34
  5. theorem OAI.UniformKServer.RankedTree.orderKey_injective line 36
  6. abbrev OAI.UniformKServer.RankedTree.order line 41
  7. def OAI.UniformKServer.RankedTree.chart line 43
  8. theorem OAI.UniformKServer.RankedTree.key_less line 47
  9. theorem OAI.UniformKServer.RankedTree.vertex_less line 50
  10. theorem OAI.UniformKServer.RankedTree.chart_zero line 55
  11. theorem OAI.UniformKServer.RankedTree.root_vertex line 64
  12. def OAI.UniformKServer.RankedTree.shape line 66
  13. theorem OAI.UniformKServer.RankedTree.shape_parent line 78
  14. theorem OAI.UniformKServer.RankedTree.depth_eq line 81