OAI/Combinatorics/ThinTrees/Continuation/BitBound.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Continuation bit bound.

  1. lemma OAI.CurrentKS.Realization.QParts.neg line 12
  2. lemma OAI.CurrentKS.Realization.QParts.sub line 14
  3. lemma OAI.CurrentKS.Realization.QParts.max line 16
  4. structure OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.MeshPoint line 27
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.meshPointCode line 31
  6. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.meshView line 32
  7. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_meshView line 36
  8. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.meshGraph line 40
  9. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.meshVector line 41
  10. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.meshRaw line 42
  11. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_meshRaw line 51
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.response_parts_bound line 57
  13. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.coefficients line 70
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.coefficients_parts_bound line 78
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State.Parts line 100
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State.Parts.mono line 103
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.update_parts_bound line 106
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.advance_parts line 137
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loop_parts line 158
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.loop_parts_length line 176
  21. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.size_next line 190
  22. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_extract line 220