OAI/Combinatorics/ThinTrees/Pencil/SearchRealization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Search realization.

  1. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphDim line 16
  2. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphSizeProgram line 17
  3. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphRadius line 19
  4. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphRadius line 22
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphBound line 24
  6. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphBound line 27
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphZeros line 35
  8. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphZeros line 41
  9. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Params.searchState line 43
  10. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.initializeSearch line 47
  11. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_initializeSearch line 51
  12. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.solvePencil line 53
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.isPoly_graph_n line 57
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.isPoly_graph_m line 60
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.isPoly_graph_fuel line 63
  16. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_solvePencil line 69
  17. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.gridStep line 77
  18. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_gridStep line 78
  19. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.gridMesh line 80
  20. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_gridMesh line 83
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.search_parts_bound line 85
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.search_output_bound line 103