def fold_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:33

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

33def fold_v(+c: List<&2, Nat>, +xs: List<&2, Nat>) -> {LV.ev(L.fold(c, xs)) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat}:
34  %Equal.sym(Nat, LV.ev(L.add(L.take(16n, xs), L.conv(L.drop(16n, xs), c))), Nat.add(LV.ev(L.take(16n, xs)), LV.ev(L.conv(L.drop(16n, xs), c))), LV.add_v(L.take(16n, xs), L.conv(L.drop(16n, xs), c))) : {_ == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat}
35  %Equal.sym(Nat, LV.ev(L.conv(L.drop(16n, xs), c)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c)), LV.conv_v(L.drop(16n, xs), c)) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), LV.ev(c))) : Nat}
36  {==}