Pver.vrs: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver
Lines 48-73 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&start_line=48&end_line=73

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
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/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
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/src/crypto/secp256k1/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as SP
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

def vrs(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.verify_rs(q, z, r, s) == ES.verify_rs(one, PT.pv(one, q), FS.value(one, z), FS.value(one, r), FS.value(one, s)) : Bool}:
  +hw = SP.inv_r(one, h1, s, hs)
  +hu1 = SO.mul_r(one, h1, z, S.inv(s), hz, hw)
  +hu2 = SO.mul_r(one, h1, r, S.inv(s), hr, hw)
  +hg = PA.g_r(one, h1)
  +hp1 = PM.mul_r(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)
  +hp2 = PM.mul_r(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)
  +hrr = PT.padd_r(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)
  %Equal.sym(Bool, Bool.and(Bool.not(P.is_inf(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)))), S.eq(S.reduce(P.aff_x(P.to_affine(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), r)), Bool.and(Bool.not(CV.is_inf(PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))), vfin(one, h1, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)), hrr, r, hr)) : {_ == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(_)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), _)), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
  {==}

Uses (48):
  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=Bool.not
  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.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=g_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=g_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend&name=mul_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend&name=mul_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=padd_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=padd_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&name=vfin
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=mul_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=mul_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend&name=inv_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend&name=inv_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sl16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SPoint
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=aff_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=padd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=pmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=verify_rs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=minv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=mmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=reduced
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=verify_rs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Point
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=aff_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=reduce