def h.split_same.b

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

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

2900def h.split_same.b(
2901  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +o: U32,
2902  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, +v: V, ob: {h.onebit(mask) == True{} : Bool},
2903  b1: Bool, b2: Bool,
2904  e1: {b1 == U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)) : Bool},
2905  e2: {b2 == U32.is_eq((o .&. mask : U32), 0) : Bool},
2906  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v), hk, k) == Some{v} : Maybe<&2, V>},
2907  fr: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), M.HLeaf{hk, [M.Entry{k, v}]}, hk, k) == Some{v} : Maybe<&2, V>}
2908) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.sp(~K, ~V, ~eq, b1, b2, p, mask, o, es, hk, k, v), hk, k) == Some{v} : Maybe<&2, V>}:
2909  match b1 b2:
2910    case True{} True{}:
2911      %h.g_lo(~K, ~V, ~eq, p, mask, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v), M.HNil{}, hk, k,
2912        h.u_same0(o, hk, mask, True{},
2913          h.sb(True{}, U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)), e1),
2914          h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2)))
2915        : {_ == Some{v} : Maybe<&2, V>}
2916      ih
2917    case True{} False{}:
2918      %h.g_hi(~K, ~V, ~eq, p, mask, M.HNil{}, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v), hk, k,
2919        h.u_same0(o, hk, mask, False{},
2920          h.sb(True{}, U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)), e1),
2921          h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2)))
2922        : {_ == Some{v} : Maybe<&2, V>}
2923      ih
2924    case False{} True{}:
2925      %h.g_hi(~K, ~V, ~eq, p, mask, M.HLeaf{o, es}, M.HLeaf{hk, [M.Entry{k, v}]}, hk, k,
2926        h.u_ne0((o .&. mask : U32), (hk .&. mask : U32),
2927          h.sb(False{}, U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)), e1),
2928          h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2)))
2929        : {_ == Some{v} : Maybe<&2, V>}
2930      fr
2931    case False{} False{}:
2932      %h.g_lo(~K, ~V, ~eq, p, mask, M.HLeaf{hk, [M.Entry{k, v}]}, M.HLeaf{o, es}, hk, k,
2933        h.u_route_t(o, hk, mask, ob,
2934          h.sb(False{}, U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)), e1),
2935          h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2)))
2936        : {_ == Some{v} : Maybe<&2, V>}
2937      fr