def pm.wb

bend-kit-collections@0.1.4.1 · PROOF.bend:1633

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

1633def pm.wb(
1634  -K: Data, -V: Data, lo: O.OMap<K, V>, +k: K, +v: V, +hi: O.OMap<K, V>,
1635  +e: {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool}
1636) -> {PMW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_pop_min(K, V, lo, k, v, hi)) == True{} : Bool}:
1637  match lo:
1638    case O.OTip{}:
1639      MBool.and_eq_true(WB(K, V, hi), Ord.near(1n+W(K, V, hi), W(K, V, hi)), wb.h(K, V, k, v, O.OTip{}, hi, e), Ord.nearpm.w0(W(K, V, hi)))
1640    case O.OBin{s, +lk, +lv, +ll, +lh}:
1641      +lo = {O.OBin{0, lk, lv, ll, lh} : O.OMap<K, V>}
1642      pm.fin.wb(K, V, Laws.g_pop_min(K, V, ll, lk, lv, lh), k, v, lo, hi,
1643        wb.ok(K, V, k, v, lo, hi, e), wb.h(K, V, k, v, lo, hi, e),
1644        pm.wb(K, V, ll, lk, lv, lh, wb.l(K, V, k, v, lo, hi, e)))