def rlp.w

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

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

1462# Balancing keeps the weight.
1463def rlp.w(
1464  -K: Data, -V: Data, single: Bool, -k: K, -v: V, +lo: O.OMap<K, V>, -hk: K, -hv: V,
1465  hl: O.OMap<K, V>, +hh: O.OMap<K, V>
1466) -> {Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh)))
1467      == W(K, V, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh)) : Nat}:
1468  match single hl:
1469    case True{} +hl:
1470      Ord.sy(Nat.add(Nat.add(W(K, V, lo), W(K, V, hl)), W(K, V, hh)),
1471        Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh))),
1472        MNat.add_assoc(W(K, V, lo), W(K, V, hl), W(K, V, hh)))
1473    case False{} O.OTip{}:
1474      Ord.sy(Nat.add(Nat.add(W(K, V, lo), 1n), W(K, V, hh)), Nat.add(W(K, V, lo), Nat.add(1n, W(K, V, hh))),
1475        MNat.add_assoc(W(K, V, lo), 1n, W(K, V, hh)))
1476    case False{} O.OBin{s, mk, mv, +ml, +mh}:
1477      +l = W(K, V, lo)
1478      +x = W(K, V, ml)
1479      +y = W(K, V, mh)
1480      +b = W(K, V, hh)
1481      Ord.tr(Nat.add(l, Nat.add(Nat.add(x, y), b)), Nat.add(l, Nat.add(x, Nat.add(y, b))),
1482        Nat.add(Nat.add(l, x), Nat.add(y, b)),
1483        Ord.cong_add(l, l, Nat.add(Nat.add(x, y), b), Nat.add(x, Nat.add(y, b)), {==}, MNat.add_assoc(x, y, b)),
1484        Ord.sy(Nat.add(Nat.add(l, x), Nat.add(y, b)), Nat.add(l, Nat.add(x, Nat.add(y, b))),
1485          MNat.add_assoc(l, x, Nat.add(y, b))))