PROOF.rhd.wb: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF Lines 1368-1402 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=1368&end_line=1402 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 rhd.wb( -K: Data, -V: Data, lh: O.OMap, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, +hi: O.OMap, +wbl: {WB(K, V, O.OBin{0, lk, lv, ll, lh}) == True{} : Bool}, wbh: {WB(K, V, hi) == True{} : Bool}, +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), Nat.add(W(K, V, ll), W(K, V, lh))), +alm: Ord.LE(Nat.add(W(K, V, ll), W(K, V, lh)), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))), +hd: Ord.LE(Nat.mul(2n, W(K, V, ll)), W(K, V, lh)) ) -> {WB(K, V, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, lh, hi)) == True{} : Bool}: match lh: case O.OTip{}: 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))) case O.OBin{s, +mk, +mv, +ml, +mh}: +lh = {O.OBin{0, mk, mv, ml, mh} : O.OMap} +l = W(K, V, hi) +x = W(K, V, mh) +y = W(K, V, ml) +b = W(K, V, ll) +okl = wb.ok(K, V, lk, lv, ll, lh, wbl) +h1 = Ord.wok_l(b, Nat.add(y, x), okl) +h2 = Ord.wok_r(b, Nat.add(y, x), okl) +wbm = wb.h(K, V, lk, lv, ll, lh, wbl) +okm = wb.ok(K, V, mk, mv, ml, mh, wbm) +h5 = Ord.wok_l(y, x, okm) +h6 = Ord.wok_r(y, x, okm) +pl = w_pos(K, V, hi) +px = w_pos(K, V, mh) +py = w_pos(K, V, ml) +pb = w_pos(K, V, ll) wb.i(K, V, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml), O.OMap.bin(K, V, k, v, mh, hi), Ord.rhd.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 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), wb.l(K, V, lk, lv, ll, lh, wbl), wb.l(K, V, mk, mv, ml, mh, wbm)), 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), wb.h(K, V, mk, mv, ml, mh, wbm), 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=rhd.w0 https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=rhd.w1 https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=rhd.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_hi.double