def h.wf_del

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

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/hmap.bend as M

3847def h.wf_del(
3848  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool,
3849  n: Nat, +mask: U32, m: M.HMap<K, V>, +hk: U32, +k: K,
3850  +wf: {h.WF(~K, ~V, ~hash, ~eq, n, m) == True{} : Bool}
3851) -> {h.WF(~K, ~V, ~hash, ~eq, n, h.D(~K, ~V, ~eq, n, mask, m, hk, k)) == True{} : Bool}:
3852  match n:
3853    case 0n:
3854      match m:
3855        case M.HNil{}:
3856          {==}
3857        case M.HLeaf{+o, +es}:
3858          h.wf_leaf(~K, ~V, ~hash, ~eq, 0n, o, M.HMap.entries.del(~K, ~V, ~eq, es, k),
3859            h.distinct_del(~K, ~V, ~eq, es, k, wf))
3860        case M.HBranch{lo, hi}:
3861          wf
3862    case 1n+(+p):
3863      match m:
3864        case M.HNil{}:
3865          {==}
3866        case M.HLeaf{+o, +es}:
3867          h.wf_del.lf(~K, ~V, ~hash, ~eq, p, o, es, k,
3868            MBool.eq_true_of_and_left(Laws.hmap_hashed(~K, ~V, ~hash, es, o), Laws.hmap_distinct(~K, ~V, ~eq, es), wf),
3869            MBool.eq_true_of_and_right(Laws.hmap_hashed(~K, ~V, ~hash, es, o), Laws.hmap_distinct(~K, ~V, ~eq, es), wf),
3870            U32.is_eq(o, hk))
3871        case M.HBranch{+lo, +hi}:
3872          h.wf_del.br(~K, ~V, ~hash, ~eq, p, mask, lo, hi, hk, k, U32.is_eq((hk .&. mask : U32), 0),
3873            MBool.eq_true_of_and_left(h.WF(~K, ~V, ~hash, ~eq, p, lo), h.WF(~K, ~V, ~hash, ~eq, p, hi), wf),
3874            MBool.eq_true_of_and_right(h.WF(~K, ~V, ~hash, ~eq, p, lo), h.WF(~K, ~V, ~hash, ~eq, p, hi), wf),
3875            h.wf_del(~K, ~V, ~hash, ~eq, p, (mask << 1n : U32), lo, hk, k,
3876              MBool.eq_true_of_and_left(h.WF(~K, ~V, ~hash, ~eq, p, lo), h.WF(~K, ~V, ~hash, ~eq, p, hi), wf)),
3877            h.wf_del(~K, ~V, ~hash, ~eq, p, (mask << 1n : U32), hi, hk, k,
3878              MBool.eq_true_of_and_right(h.WF(~K, ~V, ~hash, ~eq, p, lo), h.WF(~K, ~V, ~hash, ~eq, p, hi), wf)))