def nth_r

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:50

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

50def nth_r(+one: Nat, +h1: {one == 1n : Nat}, i: Nat, rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {red(one, P.nth(i, rs)) == True{} : Bool}:
51  match i rs:
52    case 0n Nil{}:
53      zero_r(one, h1)
54    case 1n+k Nil{}:
55      zero_r(one, h1)
56    case 0n +r <> +t:
57      Lg.and_left(red(one, r), allred(one, t), h)
58    case 1n+ +k +r <> +t:
59      nth_r(one, h1, k, t, Lg.and_right(red(one, r), allred(one, t), h))