def h.wf_put.lf

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

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

3755def h.wf_put.lf(
3756  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, ~refl: @x: K -> {eq(x, x) == True{} : Bool},
3757  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
3758  +p: Nat, +mask: U32, +o: U32, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V,
3759  hs: {Laws.hmap_hashed(~K, ~V, ~hash, es, o) == True{} : Bool},
3760  ds: {Laws.hmap_distinct(~K, ~V, ~eq, es) == True{} : Bool},
3761  b: Bool, eb: {b == U32.is_eq(o, hash(k)) : Bool},
3762  sp: {h.WF(~K, ~V, ~hash, ~eq, 1n+p, h.S(~K, ~V, ~eq, 1n+p, mask, o, es, hash(k), k, v)) == True{} : Bool}
3763) -> {h.WF(~K, ~V, ~hash, ~eq, 1n+p, h.pl(~K, ~V, ~eq, b, p, mask, o, es, hash(k), k, v)) == True{} : Bool}:
3764  match b:
3765    case True{}:
3766      MBool.and_eq_true(Laws.hmap_hashed(~K, ~V, ~hash, M.HMap.entries.put(~K, ~V, ~eq, es, k, v), o), Laws.hmap_distinct(~K, ~V, ~eq, M.HMap.entries.put(~K, ~V, ~eq, es, k, v)), h.hashed_put(~K, ~V, ~hash, ~eq, es, o, k, v, h.sb(True{}, U32.is_eq(o, hash(k)), eb), hs), h.distinct_put(~K, ~V, ~eq, ~refl, ~sound, es, k, v, ds))
3767    case False{}:
3768      sp