~/bend-docscommunity

proofs/containers/balanced_search_tree/range.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/range.bend as Range

3 imports
import Base
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/types/dynamic_array.bend as DE

Definitions

def choice_equivalent source · line 7 · raw

@+x:Nat -> @+p:Nat -> @+q:Nat -> @+found:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ascend_choice(x, p, q, found) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Ascend, found, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Ascend{0n, p, True{}}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Ascend{x, q, False{}}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Ascend}

Universal local laws for the traversal optimization, not a proof of the complete indexed TreeMap or of arbitrary iterator histories.