OAI/Combinatorics/ThinTrees/Encoding/GreedyRealization.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

Greedy realization.

  1. structure OAI.AlgorithmicThinTrees.GreedyTree.Stack.Subgraph line 18
  2. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.Subgraph.bits line 22
  3. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphCode line 23
  4. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphView line 24
  5. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_subgraphView line 26
  6. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphGraph line 30
  7. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphBits line 31
  8. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphN line 32
  9. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_subgraphN line 33
  10. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraphM line 40
  11. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.subgraph_length line 42
  12. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.SEdge line 46
  13. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.sedgeCode line 47
  14. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.sedgeContext line 48
  15. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.sedgeIndex line 49
  16. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.selected line 51
  17. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_selected line 54
  18. structure OAI.AlgorithmicThinTrees.GreedyTree.Stack.ReachState line 56
  19. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.ReachState.bits line 60
  20. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachCode line 61
  21. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachView line 62
  22. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_reachView line 64
  23. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachSubgraph line 68
  24. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachBits line 69
  25. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachN line 70
  26. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_reachN line 71
  27. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachM line 75
  28. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.Vertex line 76
  29. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.vertexCode line 77
  30. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.vertexContext line 78
  31. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.vertexIndex line 79
  32. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.reached line 81
  33. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_reached line 84
  34. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.Arc line 86
  35. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcCode line 87
  36. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcVertex line 88
  37. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcNumber line 89
  38. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcState line 90
  39. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcSubedge line 92
  40. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_arcSubedge line 95
  41. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcEdge line 97
  42. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_arcEdge line 100
  43. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcLeft line 101
  44. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.arcRight line 102
  45. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.leftReached line 104
  46. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.rightReached line 108
  47. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_leftReached line 112
  48. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_rightReached line 113
  49. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.incident line 115
  50. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_incident line 122
  51. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.expands line 124
  52. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_expands line 143
  53. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.ReachState.next line 145
  54. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.next line 147
  55. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_next line 149
  56. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.next_length line 151
  57. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.size_next line 154
  58. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.InitVertex line 164
  59. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.initVertexCode line 165
  60. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.initBit line 166
  61. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_initBit line 168
  62. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.Subgraph.start line 170
  63. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.start line 171
  64. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_start line 176
  65. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.Walk line 178
  66. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.walk line 179
  67. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_walk line 180
  68. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.reachedAll line 182
  69. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_reachedAll line 184
  70. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.walk_eq line 186
  71. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.walk_connected line 195
  72. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.connectedProgram line 214
  73. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_connectedProgram line 219
  74. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.EraseInput line 221
  75. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseInputCode line 222
  76. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseContext line 223
  77. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseIndex line 224
  78. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.EraseEdge line 225
  79. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseEdgeCode line 226
  80. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseEdgeContext line 227
  81. abbrev OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseEdgeIndex line 228
  82. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseSubedge line 230
  83. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_eraseSubedge line 233
  84. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseBit line 235
  85. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_eraseBit line 238
  86. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.erase line 240
  87. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.eraseProgram line 241
  88. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_eraseProgram line 246
  89. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.deleteAt line 248
  90. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.deleteProgram line 251
  91. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_deleteProgram line 253
  92. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.deleteAt_graph line 255
  93. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.folded_graph line 257
  94. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.size_deleteProgram line 263
  95. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.whole line 271
  96. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_whole line 275
  97. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.deleteAt_fin line 277
  98. lemma OAI.AlgorithmicThinTrees.GreedyTree.Stack.fold_deletes line 290
  99. def OAI.AlgorithmicThinTrees.GreedyTree.Stack.treeProgram line 298
  100. instance OAI.AlgorithmicThinTrees.GreedyTree.Stack.poly_treeProgram line 305