PROOF.h.split_size.b: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 3368-3387 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=3368&end_line=3387

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

# size after put and del.
def h.split_size.b(
  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +o: U32,
  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, +v: V, b1: Bool, b2: Bool,
  ih: {h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v)) == 1n+h.len(K, V, es) : Nat}
) -> {h.Sz(K, V, h.sp(~K, ~V, ~eq, b1, b2, p, mask, o, es, hk, k, v)) == 1n+h.len(K, V, es) : Nat}:
  match b1 b2:
    case True{} True{}:
      Ord.tr(Nat.add(h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v)), 0n),
        h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v)), 1n+h.len(K, V, es),
        MNat.add_zero(h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v))), ih)
    case True{} False{}:
      ih
    case False{} True{}:
      Ord.tr(Nat.add(h.len(K, V, es), 1n), 1n+Nat.add(h.len(K, V, es), 0n), 1n+h.len(K, V, es),
        MNat.add_succ(h.len(K, V, es), 0n),
        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(h.len(K, V, es), 0n), h.len(K, V, es),
          MNat.add_zero(h.len(K, V, es))))
    case False{} False{}:
      {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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.shln
  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.Sz
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.len
  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/hmap.bend&name=Entry
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=tr
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_zero