Invariants.critbit: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Invariants
Lines 82-89 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend&start_line=82&end_line=89

import Base

def critbit(-V: Data, m: Map<&2, V>) -> Bool:
  match m:
    case MTip{}:
      True{}
    case MLeaf{key, value}:
      True{}
    case MNode{+p, +lo, +hi}:
      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)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend&name=below
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend&name=common_prefix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend&name=nonempty
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend&name=routed