def critbit
bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/invariants.bend:82
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import Base
82def critbit(-V: Data, m: Map<&2, V>) -> Bool:
83 match m:
84 case MTip{}:
85 True{}
86 case MLeaf{key, value}:
87 True{}
88 case MNode{+p, +lo, +hi}:
89 common_prefix(V, MNode{p, lo, hi}, MNode{p, lo, hi}, p) && nonempty(V, lo) && nonempty(V, hi) && below(V, lo, p) && below(V, hi, p) && routed(V, lo, p, False{}) && routed(V, hi, p, True{}) && critbit(V, lo) && critbit(V, hi)