def sq01

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldpow.bend:325

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV

325def sq01(xs: List<&2, Nat>, +ys: List<&2, Nat>, +h: {BV.all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}) -> {BV.all01(xs) == True{} : Bool}:
326  match xs:
327    case Nil{}:
328      {==}
329    case +x <> +t:
330      Lg.and_intro(Nat.is_lt(x, 2n), BV.all01(t), Lg.and_left(Nat.is_lt(x, 2n), BV.all01(List.append(&2, Nat, t, ys)), h), sq01(t, ys, Lg.and_right(Nat.is_lt(x, 2n), BV.all01(List.append(&2, Nat, t, ys)), h)))