OAI/Computability/DeterministicSum/PrunedTree.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Prefix-pruned coordinate trees and enumeration bounds.

  1. structure OAI.DeterministicThreeSum.Pruned.Alphabet line 10
  2. abbrev OAI.DeterministicThreeSum.Pruned.Node line 14
  3. def OAI.DeterministicThreeSum.Pruned.next line 16
  4. def OAI.DeterministicThreeSum.Pruned.children line 19
  5. def OAI.DeterministicThreeSum.Pruned.expand line 22
  6. lemma OAI.DeterministicThreeSum.Pruned.children_length_le line 25
  7. lemma OAI.DeterministicThreeSum.Pruned.mem_children_iff line 29
  8. lemma OAI.DeterministicThreeSum.Pruned.expand_length_le line 36
  9. lemma OAI.DeterministicThreeSum.Pruned.expand_append line 44
  10. lemma OAI.DeterministicThreeSum.Pruned.children_valid line 47
  11. lemma OAI.DeterministicThreeSum.Pruned.expand_valid line 51
  12. lemma OAI.DeterministicThreeSum.Pruned.children_nonempty line 57
  13. lemma OAI.DeterministicThreeSum.Pruned.length_le_expand line 62
  14. def OAI.DeterministicThreeSum.Pruned.enumerate line 72
  15. def OAI.DeterministicThreeSum.Pruned.volume line 76
  16. def OAI.DeterministicThreeSum.Pruned.degree line 80
  17. lemma OAI.DeterministicThreeSum.Pruned.enumerate_valid line 84
  18. lemma OAI.DeterministicThreeSum.Pruned.enumerate_child line 89
  19. lemma OAI.DeterministicThreeSum.Pruned.length_enumerate_suffix line 126