def rlp.wb

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

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat
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

1313def rlp.wb(
1314  -K: Data, -V: Data, single: Bool, +k: K, +v: V, +lo: O.OMap<K, V>, +hk: K, +hv: V,
1315  +hl: O.OMap<K, V>, +hh: O.OMap<K, V>,
1316  es: {Nat.is_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh))) == single : Bool},
1317  wbl: {WB(K, V, lo) == True{} : Bool},
1318  wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool},
1319  heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))),
1320  alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo))))
1321) -> {WB(K, V, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh)) == True{} : Bool}:
1322  match single:
1323    case True{}:
1324      rls.wb(K, V, k, v, lo, hk, hv, hl, hh, wbl, wbh, heavy, alm,
1325        MNat.succ_le_of_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh)), es))
1326    case False{}:
1327      rld.wb(K, V, hl, k, v, lo, hk, hv, hh, wbl, wbh, heavy, alm,
1328        MNat.le_of_not_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh)), es))