Listops.ltm_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 187-196 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=187&end_line=196

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/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as R

def ltm_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
  +u = L.carry(32n, L.add(x, c), 0n)
  +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(x, c), 0n, {==})
  +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16))
  %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_eq(_, 0n) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
  %Equal.sym(Bool, Nat.is_eq(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), 0n), Nat.is_lt(Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), C.shift(256n, one)), hz(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one), ll)) : {_ == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
  %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), LV.ev(L.carry(32n, L.add(x, c), 0n)), Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), R.split256(one, h1, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(x), LV.ev(c)), R.u_val(c, x)) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+mp, LV.ev(c)), Equal.sym(Nat, Nat.add(1n+mp, LV.ev(c)), C.shift(256n, one), hm)) : {Nat.is_lt(Nat.add(LV.ev(x), LV.ev(c)), _) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
  WW.lt_cancel_r(LV.ev(x), 1n+mp, LV.ev(c))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=carry_limbs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=limbs_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=pos16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r
  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/limbs.bend&name=horner_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=hz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=split256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=u_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_cancel_r
  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=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=carry
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=horner
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=ltm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=take