PROOF.h.sz_del_hit.br: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 3569-3599 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=3569&end_line=3599

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat
import bend-kit-collections@0.1.4.1/hmap.bend as M
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

def h.sz_del_hit.br(
  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +lo: M.HMap<K, V>,
  +hi: M.HMap<K, V>, +hk: U32, +k: K, -w: V, b: Bool, eb: {b == U32.is_eq((hk .&. mask : U32), 0) : Bool},
  hit: {M.HMap.bool(Maybe<&2, V>, U32.is_eq((hk .&. mask : U32), 0),
    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == Some{w} : Maybe<&2, V>},
  il: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k) == Some{w} : Maybe<&2, V>}
    -> {1n+h.Sz(K, V, h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)) == h.Sz(K, V, lo) : Nat},
  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k) == Some{w} : Maybe<&2, V>}
    -> {1n+h.Sz(K, V, h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == h.Sz(K, V, hi) : Nat}
) -> {1n+h.Sz(K, V, h.db(~K, ~V, ~eq, b, p, mask, lo, hi, hk, k))
      == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}:
  match b:
    case True{}:
      +dlo = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)
      %h.size_join(K, V, dlo, hi) : {1n+_ == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}
      Ord.cong_add(1n+h.Sz(K, V, dlo), h.Sz(K, V, lo), h.Sz(K, V, hi), h.Sz(K, V, hi),
        il(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == Some{w} : Maybe<&2, V>},
          True{}, U32.is_eq((hk .&. mask : U32), 0), eb, hit)),
        {==})
    case False{}:
      +dhi = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)
      %h.size_join(K, V, lo, dhi) : {1n+_ == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}
      %MNat.add_succ(h.Sz(K, V, lo), h.Sz(K, V, dhi)) : {_ == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}
      Ord.cong_add(h.Sz(K, V, lo), h.Sz(K, V, lo), 1n+h.Sz(K, V, dhi), h.Sz(K, V, hi), {==},
        ih(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == Some{w} : Maybe<&2, V>},
          False{}, U32.is_eq((hk .&. mask : U32), 0), eb, hit)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat.add
  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/PROOF.bend&name=h.D
  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.Sz
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.db
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.size_join
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=rw
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap.bool
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=cong_add
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_succ