def rld.wb

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

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

1277def rld.wb(
1278  -K: Data, -V: Data, hl: O.OMap<K, V>, +k: K, +v: V, +lo: O.OMap<K, V>, +hk: K, +hv: V,
1279  +hh: O.OMap<K, V>,
1280  wbl: {WB(K, V, lo) == True{} : Bool},
1281  +wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool},
1282  +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))),
1283  +alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))),
1284  +hd: Ord.LE(Nat.mul(2n, W(K, V, hh)), W(K, V, hl))
1285) -> {WB(K, V, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, hl, hh)) == True{} : Bool}:
1286  match hl:
1287    case O.OTip{}:
1288      Empty.absurd({WB(K, V, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, O.OTip{}, hh)) == True{} : Bool}, Ord.dtip(W(K, V, hh), hd, w_pos(K, V, hh)))
1289    case O.OBin{s, +mk, +mv, +ml, +mh}:
1290      +hl = {O.OBin{0, mk, mv, ml, mh} : O.OMap<K, V>}
1291      +l = W(K, V, lo)
1292      +x = W(K, V, ml)
1293      +y = W(K, V, mh)
1294      +b = W(K, V, hh)
1295      +okh = wb.ok(K, V, hk, hv, hl, hh, wbh)
1296      +h1 = Ord.wok_r(Nat.add(x, y), b, okh)
1297      +h2 = Ord.wok_l(Nat.add(x, y), b, okh)
1298      +wbm = wb.l(K, V, hk, hv, hl, hh, wbh)
1299      +okm = wb.ok(K, V, mk, mv, ml, mh, wbm)
1300      +h5 = Ord.wok_r(x, y, okm)
1301      +h6 = Ord.wok_l(x, y, okm)
1302      +pl = w_pos(K, V, lo)
1303      +px = w_pos(K, V, ml)
1304      +py = w_pos(K, V, mh)
1305      +pb = w_pos(K, V, hh)
1306      wb.i(K, V, mk, mv, O.OMap.bin(K, V, k, v, lo, ml), O.OMap.bin(K, V, hk, hv, mh, hh),
1307        Ord.rld.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1308        wb.i(K, V, k, v, lo, ml, Ord.rld.w1(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1309          wbl, wb.l(K, V, mk, mv, ml, mh, wbm)),
1310        wb.i(K, V, hk, hv, mh, hh, Ord.rld.w2(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb),
1311          wb.h(K, V, mk, mv, ml, mh, wbm), wb.h(K, V, hk, hv, hl, hh, wbh)))