def h.split_size.b

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

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

3368# size after put and del.
3369def h.split_size.b(
3370  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +o: U32,
3371  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, +v: V, b1: Bool, b2: Bool,
3372  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}
3373) -> {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}:
3374  match b1 b2:
3375    case True{} True{}:
3376      Ord.tr(Nat.add(h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v)), 0n),
3377        h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v)), 1n+h.len(K, V, es),
3378        MNat.add_zero(h.Sz(K, V, h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v))), ih)
3379    case True{} False{}:
3380      ih
3381    case False{} True{}:
3382      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),
3383        MNat.add_succ(h.len(K, V, es), 0n),
3384        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(h.len(K, V, es), 0n), h.len(K, V, es),
3385          MNat.add_zero(h.len(K, V, es))))
3386    case False{} False{}:
3387      {==}