PROOF.h.split_other.b: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF Lines 3068-3136 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=3068&end_line=3136 import Base import bend-kit-collections@0.1.4.1/LAWS.bend as Laws import bend-kit-collections@0.1.4.1/hmap.bend as M def h.split_other.b( ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}, +p: Nat, +mask: U32, +o: U32, +es: List<&2, M.Entry>, +h2: U32, +k2: K, +k: K, +v: V, +hs: {Laws.hmap_hashed(~K, ~V, ~hash, es, o) == True{} : Bool}, +nk: {eq(k, k2) == False{} : Bool}, b1: Bool, b2: Bool, e2: {b2 == U32.is_eq((o .&. mask : U32), 0) : Bool}, ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, h2, k2, v), hash(k), k) == h.R(~K, ~V, ~hash, ~eq, o, es, k) : Maybe<&2, V>} ) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.sp(~K, ~V, ~eq, b1, b2, p, mask, o, es, h2, k2, v), hash(k), k) == h.R(~K, ~V, ~hash, ~eq, o, es, k) : Maybe<&2, V>}: match b1 b2: case True{} True{}: +mm = (mask << 1n : U32) +d = U32.is_eq((hash(k) .&. mask : U32), 0) +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v) +old = {M.HLeaf{o, es} : M.HMap} +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap} +r = h.R(~K, ~V, ~hash, ~eq, o, es, k) h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, sub, hash(k), k), h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), r, ed => ih, ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), None{}, r, h.gnil(~K, ~V, ~eq, p, mm, hash(k), k), h.r_none(~K, ~V, ~hash, ~eq, o, es, k, h.u_diff(o, hash(k), mask, True{}, h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2), ed)))) case True{} False{}: +mm = (mask << 1n : U32) +d = U32.is_eq((hash(k) .&. mask : U32), 0) +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v) +old = {M.HLeaf{o, es} : M.HMap} +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap} +r = h.R(~K, ~V, ~hash, ~eq, o, es, k) h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), h.G(~K, ~V, ~eq, p, mm, sub, hash(k), k), r, ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), None{}, r, h.gnil(~K, ~V, ~eq, p, mm, hash(k), k), h.r_none(~K, ~V, ~hash, ~eq, o, es, k, h.u_diff(o, hash(k), mask, False{}, h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))), ed => ih) case False{} True{}: +mm = (mask << 1n : U32) +d = U32.is_eq((hash(k) .&. mask : U32), 0) +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v) +old = {M.HLeaf{o, es} : M.HMap} +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap} +r = h.R(~K, ~V, ~hash, ~eq, o, es, k) h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, old, hash(k), k), h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), r, ed => h.g_leaf_r(~K, ~V, ~hash, ~eq, ~sound, p, mm, o, es, k, hs), ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), None{}, r, h.g_fresh_none(~K, ~V, ~eq, ~sound, p, mm, h2, k2, hash(k), k, v, nk), h.r_none(~K, ~V, ~hash, ~eq, o, es, k, h.u_diff(o, hash(k), mask, True{}, h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2), ed)))) case False{} False{}: +mm = (mask << 1n : U32) +d = U32.is_eq((hash(k) .&. mask : U32), 0) +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v) +old = {M.HLeaf{o, es} : M.HMap} +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap} +r = h.R(~K, ~V, ~hash, ~eq, o, es, k) h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), h.G(~K, ~V, ~eq, p, mm, old, hash(k), k), r, ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), None{}, r, h.g_fresh_none(~K, ~V, ~eq, ~sound, p, mm, h2, k2, hash(k), k, v, nk), h.r_none(~K, ~V, ~hash, ~eq, o, es, k, h.u_diff(o, hash(k), mask, False{}, h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))), ed => h.g_leaf_r(~K, ~V, ~hash, ~eq, ~sound, p, mm, o, es, k, hs)) Uses (23): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_hashed https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.G https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.R https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.S https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.bsel https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.g_fresh_none https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.g_leaf_r https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.gnil https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.r_none https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.sb https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.sp https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.u_diff https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=Entry https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap