OAI/Combinatorics/ThinTrees/Continuation/Realization.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Continuation realization.

  1. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphBaseline line 17
  2. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphBaseline line 19
  3. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphStep line 23
  4. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphStep line 25
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.graphError line 29
  6. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_graphError line 32
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.gainProgram line 34
  8. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_gainProgram line 36
  9. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.clockProgram line 38
  10. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_clockProgram line 43
  11. structure OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop line 51
  12. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopTailCode line 56
  13. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopDataCode line 57
  14. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop.data line 58
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopCode line 60
  16. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopView line 61
  17. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopView line 63
  18. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopGraph line 67
  19. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopGraph line 69
  20. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopRest line 73
  21. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopCount line 74
  22. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopCount line 75
  23. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopState line 79
  24. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopScale line 80
  25. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopScale line 82
  26. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopTail line 86
  27. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopQuality line 87
  28. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopQuality line 89
  29. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopArrays line 93
  30. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopMatrix line 94
  31. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopCapacity line 95
  32. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopN line 96
  33. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopM line 97
  34. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopStep line 98
  35. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopBase line 99
  36. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopGain line 100
  37. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopTarget line 101
  38. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopTarget line 105
  39. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop.params line 109
  40. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopParams line 112
  41. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_loopParams line 117
  42. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop.vector line 119
  43. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.found line 122
  44. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_found line 125
  45. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.updatedMatrix line 127
  46. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_updatedMatrix line 136
  47. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.LoopEdge line 138
  48. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loopEdgeCode line 139
  49. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeLoop line 140
  50. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeNumber line 141
  51. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.updatedCapacity line 143
  52. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_updatedCapacity line 150
  53. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop.updated line 166
  54. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.updateProgram line 168
  55. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_updateProgram line 175
  56. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.Loop.next line 177
  57. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.next line 178
  58. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_next line 181
  59. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.next_iterate line 183
  60. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.extractionInputCode line 192
  61. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.extractionGraph line 193
  62. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.extractionCount line 194
  63. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.initializeLoop line 196
  64. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_initializeLoop line 204
  65. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.extract line 206