def h.sz_del_miss.br

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

import Base
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

3642def h.sz_del_miss.br(
3643  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +lo: M.HMap<K, V>,
3644  +hi: M.HMap<K, V>, +hk: U32, +k: K, b: Bool, eb: {b == U32.is_eq((hk .&. mask : U32), 0) : Bool},
3645  miss: {M.HMap.bool(Maybe<&2, V>, U32.is_eq((hk .&. mask : U32), 0),
3646    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3647    u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3648  il: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k) == None{} : Maybe<&2, V>}
3649    -> {h.Sz(K, V, h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)) == h.Sz(K, V, lo) : Nat},
3650  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k) == None{} : Maybe<&2, V>}
3651    -> {h.Sz(K, V, h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == h.Sz(K, V, hi) : Nat}
3652) -> {h.Sz(K, V, h.db(~K, ~V, ~eq, b, p, mask, lo, hi, hk, k))
3653      == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}:
3654  match b:
3655    case True{}:
3656      +dlo = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)
3657      %h.size_join(K, V, dlo, hi) : {_ == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}
3658      Ord.cong_add(h.Sz(K, V, dlo), h.Sz(K, V, lo), h.Sz(K, V, hi), h.Sz(K, V, hi),
3659        il(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
3660            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3661            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3662          True{}, U32.is_eq((hk .&. mask : U32), 0), eb, miss)),
3663        {==})
3664    case False{}:
3665      +dhi = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)
3666      %h.size_join(K, V, lo, dhi) : {_ == Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) : Nat}
3667      Ord.cong_add(h.Sz(K, V, lo), h.Sz(K, V, lo), h.Sz(K, V, dhi), h.Sz(K, V, hi), {==},
3668        ih(rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z,
3669            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k),
3670            u => h.G(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)) == None{} : Maybe<&2, V>},
3671          False{}, U32.is_eq((hk .&. mask : U32), 0), eb, miss)))