OAI/Combinatorics/ThinTrees/Encoding/BoundaryCases.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Boundary cases.

  1. lemma OAI.AlgorithmicThinTrees.singleton_vertex_cut line 13
  2. lemma OAI.AlgorithmicThinTrees.one_vertex_empty_thinTree line 21
  3. lemma OAI.AlgorithmicThinTrees.one_vertex_tree_unique line 30
  4. lemma OAI.AlgorithmicThinTrees.one_vertex_output line 38
  5. def OAI.AlgorithmicThinTrees.emptyTreeMachine line 49
  6. lemma OAI.AlgorithmicThinTrees.emptyTreeMachine_run_one line 57
  7. theorem OAI.AlgorithmicThinTrees.one_vertex_polynomial line 63
  8. lemma OAI.AlgorithmicThinTrees.ExplicitInput.treeOutput_of_thinTree line 74
  9. lemma OAI.AlgorithmicThinTrees.BinaryInput.treeOutput_of_thinTree line 80
  10. lemma OAI.AlgorithmicThinTrees.companion_existence_extension line 91