OAI/Combinatorics/ThinTrees/Encoding/InputOutput.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Input output.

  1. def OAI.AlgorithmicThinTrees.InputStack.eEdges line 16
  2. def OAI.AlgorithmicThinTrees.InputStack.bEdges line 18
  3. def OAI.AlgorithmicThinTrees.InputStack.eOutput line 21
  4. def OAI.AlgorithmicThinTrees.InputStack.bOutput line 22
  5. def OAI.AlgorithmicThinTrees.InputStack.eRun line 24
  6. def OAI.AlgorithmicThinTrees.InputStack.lookupPair line 33
  7. instance OAI.AlgorithmicThinTrees.InputStack.poly_lookupPair line 38
  8. def OAI.AlgorithmicThinTrees.InputStack.pairsOutput line 40
  9. instance OAI.AlgorithmicThinTrees.InputStack.poly_pairsOutput line 43
  10. lemma OAI.AlgorithmicThinTrees.InputStack.bOutput_code line 45
  11. def OAI.AlgorithmicThinTrees.InputStack.bRun line 63
  12. lemma OAI.AlgorithmicThinTrees.InputStack.enum_toFinset line 67
  13. lemma OAI.AlgorithmicThinTrees.InputStack.enum_image line 74
  14. lemma OAI.AlgorithmicThinTrees.InputStack.thinTree_mono line 82
  15. lemma OAI.AlgorithmicThinTrees.InputStack.eRun_good line 94
  16. lemma OAI.AlgorithmicThinTrees.InputStack.bRun_good line 108
  17. lemma OAI.AlgorithmicThinTrees.InputStack.runsPoly_eRun line 137
  18. lemma OAI.AlgorithmicThinTrees.InputStack.runsPoly_bRun line 145