def h.gp_other.lf

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

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

3157def h.gp_other.lf(
3158  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool,
3159  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
3160  +p: Nat, +mask: U32, +o: U32, +es: List<&2, M.Entry<K, V>>, +h2: U32, +k2: K, +k: K, +v: V,
3161  +nk: {eq(k, k2) == False{} : Bool}, b: Bool,
3162  sp: {h.G(~K, ~V, ~eq, 1n+p, mask, h.S(~K, ~V, ~eq, 1n+p, mask, o, es, h2, k2, v), hash(k), k)
3163       == h.G(~K, ~V, ~eq, 1n+p, mask, M.HLeaf{o, es}, hash(k), k) : Maybe<&2, V>}
3164) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.pl(~K, ~V, ~eq, b, p, mask, o, es, h2, k2, v), hash(k), k)
3165      == h.G(~K, ~V, ~eq, 1n+p, mask, M.HLeaf{o, es}, hash(k), k) : Maybe<&2, V>}:
3166  match b:
3167    case True{}:
3168      h.bool_l(Maybe<&2, V>, U32.is_eq(o, hash(k)),
3169        h.EG(~K, ~V, ~eq, M.HMap.entries.put(~K, ~V, ~eq, es, k2, v), k), h.EG(~K, ~V, ~eq, es, k), None{},
3170        h.eg_put_other(~K, ~V, ~eq, ~sound, es, k2, k, v, nk))
3171    case False{}:
3172      sp