PROOF.rld.wb: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF Lines 1277-1311 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=1277&end_line=1311 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 def rld.wb( -K: Data, -V: Data, hl: O.OMap, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, +hh: O.OMap, wbl: {WB(K, V, lo) == True{} : Bool}, +wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool}, +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))), +alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))), +hd: Ord.LE(Nat.mul(2n, W(K, V, hh)), W(K, V, hl)) ) -> {WB(K, V, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, hl, hh)) == True{} : Bool}: match hl: case O.OTip{}: 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))) case O.OBin{s, +mk, +mv, +ml, +mh}: +hl = {O.OBin{0, mk, mv, ml, mh} : O.OMap} +l = W(K, V, lo) +x = W(K, V, ml) +y = W(K, V, mh) +b = W(K, V, hh) +okh = wb.ok(K, V, hk, hv, hl, hh, wbh) +h1 = Ord.wok_r(Nat.add(x, y), b, okh) +h2 = Ord.wok_l(Nat.add(x, y), b, okh) +wbm = wb.l(K, V, hk, hv, hl, hh, wbh) +okm = wb.ok(K, V, mk, mv, ml, mh, wbm) +h5 = Ord.wok_r(x, y, okm) +h6 = Ord.wok_l(x, y, okm) +pl = w_pos(K, V, lo) +px = w_pos(K, V, ml) +py = w_pos(K, V, mh) +pb = w_pos(K, V, hh) wb.i(K, V, mk, mv, O.OMap.bin(K, V, k, v, lo, ml), O.OMap.bin(K, V, hk, hv, mh, hh), Ord.rld.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 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), wbl, wb.l(K, V, mk, mv, ml, mh, wbm)), 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), wb.h(K, V, mk, mv, ml, mh, wbm), wb.h(K, V, hk, hv, hl, hh, wbh))) Uses (22): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=W https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=WB https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=w_pos https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=wb.h https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=wb.i https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=wb.l https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=wb.ok https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=LE https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=dtip https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=rld.w0 https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=rld.w1 https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=rld.w2 https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=wok_l https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=wok_r https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.bin https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.rot_lo.double