proofs/containers/balanced_search_tree/range.bend

bend-collections-laws-containers@1.0.0.0 · 12 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DE
4
5# Universal local laws for the traversal optimization, not a proof of the
6# complete indexed TreeMap or of arbitrary iterator histories.
7def choice_equivalent(+x: Nat, +p: Nat, +q: Nat, +found: Bool) -> {M.ascend_choice(x, p, q, found) == M.pick(M.Ascend, found, M.Ascend{0n, p, True{}}, M.Ascend{x, q, False{}}) : M.Ascend}:
8  match found:
9    case False{}:
10      {==}
11    case True{}:
12      {==}