OAI/Combinatorics/ThinTrees/Pencil/ScalarConstraintRealization.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Scalar constraint realization.

  1. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalar_poly_pointField line 17
  2. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarValue line 20
  3. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarTriple line 23
  4. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarTriple line 28
  5. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeScalarEquiv line 30
  6. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeScalarCode line 31
  7. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esPoint line 32
  8. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esP line 33
  9. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esEdge line 35
  10. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esE line 36
  11. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esE line 37
  12. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esY line 41
  13. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esZ line 42
  14. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esX line 43
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esU line 44
  16. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esY line 45
  17. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esZ line 49
  18. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esX line 53
  19. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esU line 57
  20. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esK line 61
  21. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esT line 62
  22. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esActive line 64
  23. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esActive line 65
  24. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esCapacityRate line 67
  25. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esCapacityRate line 73
  26. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.esCapacity line 80
  27. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_esCapacity line 83
  28. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarEdge line 89
  29. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarEdge line 100
  30. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.rootEdgeEquiv line 106
  31. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.rootEdgeCode line 107
  32. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.rePoint line 108
  33. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.reR line 109
  34. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.reE line 110
  35. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_reR line 111
  36. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_reE line 115
  37. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.reA line 119
  38. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.reB line 120
  39. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.reX line 121
  40. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_reA line 122
  41. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_reB line 126
  42. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_reX line 130
  43. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.flowScalarEquiv line 135
  44. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.flowScalarCode line 136
  45. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.fsRE line 137
  46. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.fsP line 139
  47. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarFlow line 142
  48. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarFlow line 150
  49. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.budgetCode line 155
  50. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.bsPoint line 156
  51. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.bsR line 157
  52. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.bsV line 158
  53. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.budgetEdgeCode line 159
  54. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beBudget line 160
  55. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beE line 161
  56. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.bePoint line 162
  57. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beR line 163
  58. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beV line 164
  59. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beGraphEdge line 165
  60. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beA line 166
  61. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.beB line 167
  62. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_beA line 168
  63. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_beB line 173
  64. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.budgetEdge line 179
  65. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_budgetEdge line 191
  66. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.budgetIncoming line 196
  67. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_budgetIncoming line 199
  68. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarBudget line 201
  69. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarBudget line 211
  70. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.xePoint line 219
  71. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.xeE line 220
  72. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeTotal line 221
  73. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_edgeTotal line 223
  74. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarTotalBase line 225
  75. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarTotalBase line 229
  76. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarTotal line 235
  77. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarTotal line 238
  78. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarEquiv line 240
  79. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarCode line 242
  80. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.scalarConstraints line 244
  81. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_scalarConstraints line 257