def h.wf_join

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

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

2869def h.wf_join(
2870  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +p: Nat, lo: M.HMap<K, V>,
2871  hi: M.HMap<K, V>, wl: {h.WF(~K, ~V, ~hash, ~eq, p, lo) == True{} : Bool},
2872  wh: {h.WF(~K, ~V, ~hash, ~eq, p, hi) == True{} : Bool}
2873) -> {h.WF(~K, ~V, ~hash, ~eq, 1n+p, M.HMap.join(K, V, lo, hi)) == True{} : Bool}:
2874  match lo:
2875    case M.HNil{}:
2876      match hi:
2877        case M.HNil{}:
2878          {==}
2879        case M.HLeaf{+a, +b}:
2880          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)
2881        case M.HBranch{+a, +b}:
2882          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)
2883    case M.HLeaf{+a, +b}:
2884      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)
2885    case M.HBranch{+a, +b}:
2886      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)