OAI/Combinatorics/ThinTrees/Encoding/GreedyTree.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Greedy tree.

  1. def OAI.AlgorithmicThinTrees.GreedyTree.expand line 14
  2. def OAI.AlgorithmicThinTrees.GreedyTree.reach line 19
  3. lemma OAI.AlgorithmicThinTrees.GreedyTree.subset_expand line 22
  4. lemma OAI.AlgorithmicThinTrees.GreedyTree.reach_succ line 25
  5. lemma OAI.AlgorithmicThinTrees.GreedyTree.reach_mono line 28
  6. lemma OAI.AlgorithmicThinTrees.GreedyTree.reach_root line 32
  7. lemma OAI.AlgorithmicThinTrees.GreedyTree.expand_strict line 35
  8. lemma OAI.AlgorithmicThinTrees.GreedyTree.reach_full line 50
  9. lemma OAI.AlgorithmicThinTrees.GreedyTree.reach_same line 71
  10. lemma OAI.AlgorithmicThinTrees.GreedyTree.connected_iff_reach line 92
  11. def OAI.AlgorithmicThinTrees.GreedyTree.connected line 100
  12. lemma OAI.AlgorithmicThinTrees.GreedyTree.connected_correct line 103
  13. lemma OAI.AlgorithmicThinTrees.GreedyTree.connected_mono line 115
  14. def OAI.AlgorithmicThinTrees.GreedyTree.eraseIf line 120
  15. def OAI.AlgorithmicThinTrees.GreedyTree.deletePass line 123
  16. def OAI.AlgorithmicThinTrees.GreedyTree.tree line 126
  17. lemma OAI.AlgorithmicThinTrees.GreedyTree.eraseIf_subset line 128
  18. lemma OAI.AlgorithmicThinTrees.GreedyTree.eraseIf_connected line 133
  19. lemma OAI.AlgorithmicThinTrees.GreedyTree.deletePass_correct line 140
  20. theorem OAI.AlgorithmicThinTrees.GreedyTree.tree_correct line 162