def rhp.w

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

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat
import bend-kit-collections@0.1.4.1/omap.bend as O
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

1487def rhp.w(
1488  -K: Data, -V: Data, single: Bool, -k: K, -v: V, -lk: K, -lv: V, +ll: O.OMap<K, V>,
1489  lh: O.OMap<K, V>, +hi: O.OMap<K, V>
1490) -> {Nat.add(Nat.add(W(K, V, ll), W(K, V, lh)), W(K, V, hi))
1491      == W(K, V, O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi)) : Nat}:
1492  match single lh:
1493    case True{} +lh:
1494      MNat.add_assoc(W(K, V, ll), W(K, V, lh), W(K, V, hi))
1495    case False{} O.OTip{}:
1496      MNat.add_assoc(W(K, V, ll), 1n, W(K, V, hi))
1497    case False{} O.OBin{s, mk, mv, +ml, +mh}:
1498      +l = W(K, V, hi)
1499      +x = W(K, V, mh)
1500      +y = W(K, V, ml)
1501      +b = W(K, V, ll)
1502      Ord.tr(Nat.add(Nat.add(b, Nat.add(y, x)), l), Nat.add(Nat.add(Nat.add(b, y), x), l),
1503        Nat.add(Nat.add(b, y), Nat.add(x, l)),
1504        Ord.cong_add(Nat.add(b, Nat.add(y, x)), Nat.add(Nat.add(b, y), x), l, l,
1505          Ord.sy(Nat.add(Nat.add(b, y), x), Nat.add(b, Nat.add(y, x)), MNat.add_assoc(b, y, x)), {==}),
1506        MNat.add_assoc(Nat.add(b, y), x, l))