def h.sz_put_new.br

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

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

3419def h.sz_put_new.br(
3420  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +lo: M.HMap<K, V>,
3421  +hi: M.HMap<K, V>, +hk: U32, +k: K, +v: V, b: Bool, eb: {b == U32.is_eq((hk .&. mask : U32), 0) : Bool},
3422  miss: {M.HMap.bool(Maybe<&2, V>, U32.is_eq((hk .&. mask : U32), 0),
3423    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3424    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3425  il: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k) == None{} : Maybe<&2, V>}
3426    -> {h.Sz(K, V, h.P(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k, v)) == 1n+h.Sz(K, V, lo) : Nat},
3427  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k) == None{} : Maybe<&2, V>}
3428    -> {h.Sz(K, V, h.P(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k, v)) == 1n+h.Sz(K, V, hi) : Nat}
3429) -> {h.Sz(K, V, h.pb(~K, ~V, ~eq, b, p, mask, lo, hi, hk, k, v))
3430      == 1n+Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}:
3431  match b:
3432    case True{}:
3433      Ord.cong_add(h.Sz(K, V, h.P(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k, v)), 1n+h.Sz(K, V, lo),
3434        h.Sz(K, V, hi), h.Sz(K, V, hi),
3435        il(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
3436            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3437            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3438          True{}, U32.is_eq((hk .&. mask : U32), 0), eb, miss)),
3439        {==})
3440    case False{}:
3441      Ord.tr(Nat.add(h.Sz(K, V, lo), h.Sz(K, V, h.P(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k, v))),
3442        Nat.add(h.Sz(K, V, lo), 1n+h.Sz(K, V, hi)), 1n+Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)),
3443        Ord.cong_add(h.Sz(K, V, lo), h.Sz(K, V, lo),
3444          h.Sz(K, V, h.P(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k, v)), 1n+h.Sz(K, V, hi), {==},
3445          ih(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
3446              u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3447              u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3448            False{}, U32.is_eq((hk .&. mask : U32), 0), eb, miss))),
3449        MNat.add_succ(h.Sz(K, V, lo), h.Sz(K, V, hi)))