def rl.w

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

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

1508def rl.w(-K: Data, -V: Data, hi: O.OMap<K, V>, -k: K, -v: V, +lo: O.OMap<K, V>)
1509  -> {Nat.add(W(K, V, lo), W(K, V, hi)) == W(K, V, Laws.g_rot_lo(K, V, k, v, lo, hi)) : Nat}:
1510  match hi:
1511    case O.OTip{}:
1512      {==}
1513    case O.OBin{s, hk, hv, +hl, +hh}:
1514      rlp.w(K, V, Nat.is_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh))), k, v, lo, hk, hv, hl, hh)