def rhd.wb

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

import Base
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

1368def rhd.wb(
1369  -K: Data, -V: Data, lh: O.OMap<K, V>, +k: K, +v: V, +lk: K, +lv: V,
1370  +ll: O.OMap<K, V>, +hi: O.OMap<K, V>,
1371  +wbl: {WB(K, V, O.OBin{0, lk, lv, ll, lh}) == True{} : Bool},
1372  wbh: {WB(K, V, hi) == True{} : Bool},
1373  +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), Nat.add(W(K, V, ll), W(K, V, lh))),
1374  +alm: Ord.LE(Nat.add(W(K, V, ll), W(K, V, lh)), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))),
1375  +hd: Ord.LE(Nat.mul(2n, W(K, V, ll)), W(K, V, lh))
1376) -> {WB(K, V, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, lh, hi)) == True{} : Bool}:
1377  match lh:
1378    case O.OTip{}:
1379      Empty.absurd({WB(K, V, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, O.OTip{}, hi)) == True{} : Bool}, Ord.dtip(W(K, V, ll), hd, w_pos(K, V, ll)))
1380    case O.OBin{s, +mk, +mv, +ml, +mh}:
1381      +lh = {O.OBin{0, mk, mv, ml, mh} : O.OMap<K, V>}
1382      +l = W(K, V, hi)
1383      +x = W(K, V, mh)
1384      +y = W(K, V, ml)
1385      +b = W(K, V, ll)
1386      +okl = wb.ok(K, V, lk, lv, ll, lh, wbl)
1387      +h1 = Ord.wok_l(b, Nat.add(y, x), okl)
1388      +h2 = Ord.wok_r(b, Nat.add(y, x), okl)
1389      +wbm = wb.h(K, V, lk, lv, ll, lh, wbl)
1390      +okm = wb.ok(K, V, mk, mv, ml, mh, wbm)
1391      +h5 = Ord.wok_l(y, x, okm)
1392      +h6 = Ord.wok_r(y, x, okm)
1393      +pl = w_pos(K, V, hi)
1394      +px = w_pos(K, V, mh)
1395      +py = w_pos(K, V, ml)
1396      +pb = w_pos(K, V, ll)
1397      wb.i(K, V, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml), O.OMap.bin(K, V, k, v, mh, hi),
1398        Ord.rhd.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1399        wb.i(K, V, lk, lv, ll, ml, Ord.rhd.w1(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1400          wb.l(K, V, lk, lv, ll, lh, wbl), wb.l(K, V, mk, mv, ml, mh, wbm)),
1401        wb.i(K, V, k, v, mh, hi, Ord.rhd.w2(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1402          wb.h(K, V, mk, mv, ml, mh, wbm), wbh))