OAI/Combinatorics/ThinTrees/Encoding/InputDispatch.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Input dispatch.

  1. abbrev OAI.AlgorithmicThinTrees.InputStack.Good line 16
  2. abbrev OAI.AlgorithmicThinTrees.InputStack.Large line 17
  3. abbrev OAI.AlgorithmicThinTrees.InputStack.goodCode line 18
  4. abbrev OAI.AlgorithmicThinTrees.InputStack.largeCode line 19
  5. lemma OAI.AlgorithmicThinTrees.InputStack.valid_n line 20
  6. def OAI.AlgorithmicThinTrees.InputStack.isBinary line 23
  7. def OAI.AlgorithmicThinTrees.InputStack.asBinary line 27
  8. def OAI.AlgorithmicThinTrees.InputStack.asExplicit line 31
  9. lemma OAI.AlgorithmicThinTrees.InputStack.asBinary_input line 36
  10. lemma OAI.AlgorithmicThinTrees.InputStack.asExplicit_input line 41
  11. def OAI.AlgorithmicThinTrees.InputStack.formatTest line 47
  12. instance OAI.AlgorithmicThinTrees.InputStack.poly_formatTest line 50
  13. def OAI.AlgorithmicThinTrees.InputStack.binaryTail line 52
  14. def OAI.AlgorithmicThinTrees.InputStack.explicitTail line 59
  15. instance OAI.AlgorithmicThinTrees.InputStack.poly_binaryTail line 66
  16. instance OAI.AlgorithmicThinTrees.InputStack.poly_explicitTail line 67
  17. def OAI.AlgorithmicThinTrees.InputStack.largeOutput line 69
  18. def OAI.AlgorithmicThinTrees.InputStack.largeRun line 71
  19. def OAI.AlgorithmicThinTrees.InputStack.makeLarge line 74
  20. lemma OAI.AlgorithmicThinTrees.InputStack.makeLarge_input line 80
  21. def OAI.AlgorithmicThinTrees.InputStack.inputFields line 82
  22. lemma OAI.AlgorithmicThinTrees.InputStack.inputFields_code line 85
  23. def OAI.AlgorithmicThinTrees.InputStack.goodFields line 91
  24. instance OAI.AlgorithmicThinTrees.InputStack.poly_goodFields line 94
  25. def OAI.AlgorithmicThinTrees.InputStack.goodN line 96
  26. instance OAI.AlgorithmicThinTrees.InputStack.poly_goodN line 98
  27. def OAI.AlgorithmicThinTrees.InputStack.singletonTest line 100
  28. instance OAI.AlgorithmicThinTrees.InputStack.poly_singletonTest line 107
  29. def OAI.AlgorithmicThinTrees.InputStack.output line 109
  30. def OAI.AlgorithmicThinTrees.InputStack.program line 111
  31. lemma OAI.AlgorithmicThinTrees.InputStack.largeRun_good line 121
  32. lemma OAI.AlgorithmicThinTrees.InputStack.program_good line 129
  33. lemma OAI.AlgorithmicThinTrees.InputStack.runsPoly_largeRun line 140
  34. lemma OAI.AlgorithmicThinTrees.InputStack.runsPoly_program line 151