OAI/Combinatorics/ThinTrees/Pencil/PointPrograms.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Point programs.

  1. def OAI.CurrentKS.Realization.Realizes.cons line 14
  2. instance OAI.CurrentKS.Realization.poly_cons line 17
  3. def OAI.CurrentKS.Realization.select3 line 21
  4. instance OAI.CurrentKS.Realization.poly_select3 line 27
  5. def OAI.CurrentKS.Realization.select7 line 32
  6. instance OAI.CurrentKS.Realization.poly_select7 line 42
  7. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_nadd_explicit line 57
  8. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_nmul_explicit line 64
  9. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeCoord line 71
  10. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_edgeCoord line 78
  11. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.flowCoord line 91
  12. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_flowCoord line 101
  13. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.storedU line 116
  14. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_storedU line 120
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphEdge line 124
  16. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphEdge line 129
  17. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.vEquiv line 133
  18. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.eEquiv line 134
  19. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.pairEquiv line 135
  20. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleEquiv line 136
  21. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleCode line 137
  22. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.triplePoint line 138
  23. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleHead line 139
  24. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleTail line 140
  25. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.pairHead line 141
  26. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.pairTail line 142
  27. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleI line 143
  28. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleJ line 144
  29. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleK line 145
  30. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleCoordinate line 147
  31. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_tripleCoordinate line 151
  32. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.tripleDistinct line 163
  33. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_tripleDistinct line 166