def h.sz_del_hit.lf

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

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

3552def h.sz_del_hit.lf(
3553  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +o: U32,
3554  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, -w: V,
3555  b: Bool, eb: {b == U32.is_eq(o, hk) : Bool},
3556  hit: {M.HMap.bool(Maybe<&2, V>, U32.is_eq(o, hk), u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == Some{w} : Maybe<&2, V>}
3557) -> {1n+h.Sz(K, V, h.dl(~K, ~V, ~eq, b, o, es, k)) == h.len(K, V, es) : Nat}:
3558  match b:
3559    case True{}:
3560      %h.size_leaf(K, V, o, M.HMap.entries.del(~K, ~V, ~eq, es, k)) : {1n+_ == h.len(K, V, es) : Nat}
3561      h.elen_del_hit(~K, ~V, ~eq, es, k, w,
3562        rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z, u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == Some{w} : Maybe<&2, V>},
3563          True{}, U32.is_eq(o, hk), eb, hit))
3564    case False{}:
3565      h.none_some({1n+h.len(K, V, es) == h.len(K, V, es) : Nat}, V, w,
3566        rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z, u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == Some{w} : Maybe<&2, V>},
3567          False{}, U32.is_eq(o, hk), eb, hit))