Listops.nonzero_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
Lines 53-63 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&start_line=53&end_line=63

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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

def nonzero_v(xs: List<&2, Nat>, +acc: Nat) -> {Nat.is_eq(L.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), 0n)) : Bool}:
  match xs:
    case Nil{}:
      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
    case +x <> +t:
      %Equal.sym(Bool, Nat.is_eq(L.nonzero(t, Nat.add(acc, x)), 0n), Bool.and(Nat.is_eq(Nat.add(acc, x), 0n), Nat.is_eq(LV.ev(t), 0n)), nonzero_v(t, Nat.add(acc, x))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, x), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), is_eq_add0(acc, x)) : {Bool.and(_, Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(C.shift(16n, LV.ev(t)), 0n)), is_eq_add0(x, C.shift(16n, LV.ev(t)))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
      %Equal.sym(Bool, Nat.is_eq(C.shift(16n, LV.ev(t)), 0n), Nat.is_eq(LV.ev(t), 0n), sh_eq0(LV.ev(t))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), _)) : Bool}
      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : Bool}
      {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=and_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=and_true_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=is_eq_add0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=sh_eq0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=nonzero