def h.sz_del_miss

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

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

3673def h.sz_del_miss(
3674  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, n: Nat, +mask: U32, m: M.HMap<K, V>, +hk: U32, +k: K,
3675  miss: {h.G(~K, ~V, ~eq, n, mask, m, hk, k) == None{} : Maybe<&2, V>}
3676) -> {h.Sz(K, V, h.D(~K, ~V, ~eq, n, mask, m, hk, k)) == h.Sz(K, V, m) : Nat}:
3677  match n:
3678    case 0n:
3679      match m:
3680        case M.HNil{}:
3681          {==}
3682        case M.HLeaf{+o, +es}:
3683          %h.size_leaf(K, V, o, M.HMap.entries.del(~K, ~V, ~eq, es, k)) : {_ == h.len(K, V, es) : Nat}
3684          Equal.cong(List<&2, M.Entry<K, V>>, Nat, xs => h.len(K, V, xs), M.HMap.entries.del(~K, ~V, ~eq, es, k), es,
3685            h.edel_miss(~K, ~V, ~eq, es, k, miss))
3686        case M.HBranch{lo, hi}:
3687          {==}
3688    case 1n+(+p):
3689      match m:
3690        case M.HNil{}:
3691          {==}
3692        case M.HLeaf{+o, +es}:
3693          h.sz_del_miss.lf(~K, ~V, ~eq, o, es, hk, k, U32.is_eq(o, hk), {==}, miss)
3694        case M.HBranch{+lo, +hi}:
3695          h.sz_del_miss.br(~K, ~V, ~eq, p, mask, lo, hi, hk, k, U32.is_eq((hk .&. mask : U32), 0), {==}, miss,
3696            e => h.sz_del_miss(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k, e),
3697            e => h.sz_del_miss(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k, e))