def suf_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/blist.bend:70

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

70def suf_len(a: Nat, +b: Nat, xs: List<&2, U32>, +h: {B.has_len(Nat.add(a, b), xs) == True{} : Bool}) -> {B.has_len(b, CV.after(a, xs)) == True{} : Bool}:
71  match a xs:
72    case 0n _:
73      h
74    case 1n+k Nil{}:
75      Empty.absurd({B.has_len(b, CV.after(1n+k, [])) == True{} : Bool}, Lg.false_true(h))
76    case 1n+k x <> t:
77      suf_len(k, b, t, h)