OAI/Combinatorics/ThinTrees/Encoding/InputExpansion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Input expansion.

  1. def OAI.AlgorithmicThinTrees.InputStack.makeProblem line 15
  2. lemma OAI.AlgorithmicThinTrees.InputStack.makeProblem_n line 28
  3. lemma OAI.AlgorithmicThinTrees.InputStack.makeProblem_code line 31
  4. lemma OAI.AlgorithmicThinTrees.InputStack.makeProblem_connected line 39
  5. lemma OAI.AlgorithmicThinTrees.InputStack.makeProblem_thin line 44
  6. abbrev OAI.AlgorithmicThinTrees.InputStack.eProblem line 51
  7. abbrev OAI.AlgorithmicThinTrees.InputStack.bProblem line 52
  8. def OAI.AlgorithmicThinTrees.InputStack.ePrepare line 55
  9. instance OAI.AlgorithmicThinTrees.InputStack.poly_ePrepare line 61
  10. lemma OAI.AlgorithmicThinTrees.InputStack.eProblem_good line 63
  11. def OAI.AlgorithmicThinTrees.InputStack.bMultiplicityRat line 68
  12. instance OAI.AlgorithmicThinTrees.InputStack.poly_bMultiplicityRat line 70
  13. def OAI.AlgorithmicThinTrees.InputStack.bCountBinary line 72
  14. instance OAI.AlgorithmicThinTrees.InputStack.poly_bCountBinary line 91
  15. def OAI.AlgorithmicThinTrees.InputStack.bCount line 93
  16. instance OAI.AlgorithmicThinTrees.InputStack.poly_bCount line 94
  17. def OAI.AlgorithmicThinTrees.InputStack.bEndpointBlock line 107
  18. instance OAI.AlgorithmicThinTrees.InputStack.poly_bEndpointBlock line 111
  19. def OAI.AlgorithmicThinTrees.InputStack.bLefts line 114
  20. def OAI.AlgorithmicThinTrees.InputStack.bRights line 118
  21. def OAI.AlgorithmicThinTrees.InputStack.bRecords line 122
  22. instance OAI.AlgorithmicThinTrees.InputStack.poly_bLefts line 127
  23. instance OAI.AlgorithmicThinTrees.InputStack.poly_bRights line 128
  24. instance OAI.AlgorithmicThinTrees.InputStack.poly_bRecords line 129
  25. def OAI.AlgorithmicThinTrees.InputStack.bPrepare line 131
  26. instance OAI.AlgorithmicThinTrees.InputStack.poly_bPrepare line 137
  27. lemma OAI.AlgorithmicThinTrees.InputStack.bProblem_good line 139