def h.gd_other.lf

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

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

3294def h.gd_other.lf(
3295  ~K: Data, ~V: Data, ~eq: K -> K -> Bool,
3296  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
3297  +p: Nat, +mask: U32, +o: U32, +es: List<&2, M.Entry<K, V>>, +k2: K, +hk: U32, +k: K,
3298  +nk: {eq(k, k2) == False{} : Bool}, b: Bool
3299) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.dl(~K, ~V, ~eq, b, o, es, k2), hk, k)
3300      == h.G(~K, ~V, ~eq, 1n+p, mask, M.HLeaf{o, es}, hk, k) : Maybe<&2, V>}:
3301  match b:
3302    case True{}:
3303      %h.get_leaf(~K, ~V, ~eq, 1n+p, mask, o, M.HMap.entries.del(~K, ~V, ~eq, es, k2), hk, k)
3304        : {_ == h.G(~K, ~V, ~eq, 1n+p, mask, M.HLeaf{o, es}, hk, k) : Maybe<&2, V>}
3305      h.bool_l(Maybe<&2, V>, U32.is_eq(o, hk),
3306        h.EG(~K, ~V, ~eq, M.HMap.entries.del(~K, ~V, ~eq, es, k2), k), h.EG(~K, ~V, ~eq, es, k), None{},
3307        h.eg_del_other(~K, ~V, ~eq, ~sound, es, k2, k, nk))
3308    case False{}:
3309      {==}