OAI/Combinatorics/UniformKServer/PartitionTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual fixed full-prefix tree associated with the literal partition. The alphabet, tree and independent tape domains are instance-dependent but law- and horizon-independent (apart from a finite tape restriction).

  1. def OAI.UniformKServer.PartitionTree.height line 21
  2. abbrev OAI.UniformKServer.PartitionTree.Label line 22
  3. abbrev OAI.UniformKServer.PartitionTree.LevelTape line 25
  4. abbrev OAI.UniformKServer.PartitionTree.Tape line 29
  5. abbrev OAI.UniformKServer.PartitionTree.size line 30
  6. def OAI.UniformKServer.PartitionTree.shape line 31
  7. def OAI.UniformKServer.PartitionTree.word line 33
  8. def OAI.UniformKServer.PartitionTree.map line 38
  9. def OAI.UniformKServer.PartitionTree.region line 48
  10. theorem OAI.UniformKServer.PartitionTree.root_region line 52
  11. theorem OAI.UniformKServer.PartitionTree.nested line 58
  12. theorem OAI.UniformKServer.PartitionTree.region_prefix line 65
  13. theorem OAI.UniformKServer.PartitionTree.same_prefix line 71