def h.size_join

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

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

2835def h.size_join(-K: Data, -V: Data, lo: M.HMap<K, V>, hi: M.HMap<K, V>)
2836  -> {Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) == h.Sz(K, V, M.HMap.join(K, V, lo, hi)) : Nat}:
2837  match lo:
2838    case M.HNil{}:
2839      match hi:
2840        case M.HNil{}:
2841          {==}
2842        case M.HLeaf{a, b}:
2843          {==}
2844        case M.HBranch{a, b}:
2845          {==}
2846    case M.HLeaf{a, b}:
2847      {==}
2848    case M.HBranch{a, b}:
2849      {==}