PROOF.h.wf_join: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 2869-2886 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=2869&end_line=2886

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
import bend-kit-collections@0.1.4.1/hmap.bend as M

def h.wf_join(
  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +p: Nat, lo: M.HMap<K, V>,
  hi: M.HMap<K, V>, wl: {h.WF(~K, ~V, ~hash, ~eq, p, lo) == True{} : Bool},
  wh: {h.WF(~K, ~V, ~hash, ~eq, p, hi) == True{} : Bool}
) -> {h.WF(~K, ~V, ~hash, ~eq, 1n+p, M.HMap.join(K, V, lo, hi)) == True{} : Bool}:
  match lo:
    case M.HNil{}:
      match hi:
        case M.HNil{}:
          {==}
        case M.HLeaf{+a, +b}:
          MBool.and_eq_true(h.WF(~K, ~V, ~hash, ~eq, p, M.HNil{}), h.WF(~K, ~V, ~hash, ~eq, p, M.HLeaf{a, b}), wl, wh)
        case M.HBranch{+a, +b}:
          MBool.and_eq_true(h.WF(~K, ~V, ~hash, ~eq, p, M.HNil{}), h.WF(~K, ~V, ~hash, ~eq, p, M.HBranch{a, b}), wl, wh)
    case M.HLeaf{+a, +b}:
      MBool.and_eq_true(h.WF(~K, ~V, ~hash, ~eq, p, M.HLeaf{a, b}), h.WF(~K, ~V, ~hash, ~eq, p, hi), wl, wh)
    case M.HBranch{+a, +b}:
      MBool.and_eq_true(h.WF(~K, ~V, ~hash, ~eq, p, M.HBranch{a, b}), h.WF(~K, ~V, ~hash, ~eq, p, hi), wl, wh)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.WF
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap.join
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_eq_true