OAI/Combinatorics/ThinTrees/Sparsification/IterationRealization.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Iteration realization.

  1. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.nextCount_le line 16
  2. def OAI.AlgorithmicThinTrees.Iteration.Stack.nextCountBinary line 24
  3. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_nextCountBinary line 28
  4. def OAI.AlgorithmicThinTrees.Iteration.Stack.nextCountProgram line 32
  5. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_nextCountProgram line 33
  6. structure OAI.AlgorithmicThinTrees.Iteration.Stack.State line 41
  7. def OAI.AlgorithmicThinTrees.Iteration.Stack.stateCode line 45
  8. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.stateView line 47
  9. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_stateView line 51
  10. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.problem line 55
  11. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_problem line 56
  12. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.labels line 60
  13. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_labels line 61
  14. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.graph line 65
  15. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_graph line 66
  16. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.count line 70
  17. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_count line 71
  18. def OAI.AlgorithmicThinTrees.Iteration.Stack.State.restrict line 75
  19. def OAI.AlgorithmicThinTrees.Iteration.Stack.halve line 78
  20. def OAI.AlgorithmicThinTrees.Iteration.Stack.step line 79
  21. def OAI.AlgorithmicThinTrees.Iteration.Stack.selectState line 81
  22. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_selectState line 109
  23. def OAI.AlgorithmicThinTrees.Iteration.Stack.halveProgram line 115
  24. def OAI.AlgorithmicThinTrees.Iteration.Stack.large line 126
  25. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_large line 128
  26. def OAI.AlgorithmicThinTrees.Iteration.Stack.stepProgram line 130
  27. def OAI.AlgorithmicThinTrees.Iteration.Stack.finishData line 133
  28. def OAI.AlgorithmicThinTrees.Iteration.Stack.finish line 135
  29. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_finish line 138
  30. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.restrict_length line 140
  31. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.step_length line 150
  32. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.orbit_length line 155
  33. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.orbit_packed line 161
  34. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.runsPoly_step line 176
  35. def OAI.AlgorithmicThinTrees.Iteration.Stack.run line 211
  36. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.runsPoly_run line 214
  37. lemma OAI.AlgorithmicThinTrees.OrderedGraph.sorted_lift line 236
  38. lemma OAI.AlgorithmicThinTrees.OrderedGraph.mapped_sorted_lift line 253
  39. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.run_data line 264
  40. def OAI.AlgorithmicThinTrees.Iteration.Stack.initialCountProgram line 281
  41. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_initialCountProgram line 289
  42. abbrev OAI.AlgorithmicThinTrees.Iteration.Stack.TreeProblem line 292
  43. def OAI.AlgorithmicThinTrees.Iteration.Stack.start line 294
  44. def OAI.AlgorithmicThinTrees.Iteration.Stack.startProgram line 296
  45. instance OAI.AlgorithmicThinTrees.Iteration.Stack.poly_startProgram line 308
  46. def OAI.AlgorithmicThinTrees.Iteration.Stack.treeData line 310
  47. def OAI.AlgorithmicThinTrees.Iteration.Stack.treeProgram line 312
  48. lemma OAI.AlgorithmicThinTrees.Iteration.Stack.runsPoly_tree line 315