Point.padd_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as Point
Lines 195-214 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&start_line=195&end_line=214

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/src/crypto/secp256k1/point.bend as P

def padd_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, b: P.Point, +ha: {pred(one, a) == True{} : Bool}, +hb: {pred(one, b) == True{} : Bool}) -> {pv(one, P.add(a, b)) == CV.padd(FS.prime(one), pv(one, a), pv(one, b)) : CV.SPoint}:
  match a b:
    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
      +hr = regs7(one, h1, x1, y1, z1, x2, y2, z2, ha, hb)
      %Equal.sym(Nat, FS.value(one, P.nth(33n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 33n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{_, FS.value(one, P.nth(36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(Nat, FS.value(one, P.nth(36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), _, FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(Nat, FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), _} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, _), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, _), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, _)} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), _)), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), _)), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), _))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
      {==}

Uses (30):
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=add_prog_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=b3_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=cprog
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=nth_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/point.bend&name=regs7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=run_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=vals
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=vals7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SOp
  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=add_out
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=add_prog
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=b3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=nth
  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=run
  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=value
  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=add_prog
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=b3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=nth
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=run