Point.run_go_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 120-130 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=120&end_line=130

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 run_go_v(+one: Nat, +h1: {one == 1n : Nat}, prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {vals(one, P.run_go(prog, rs)) == CV.run_go(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}:
  match prog:
    case Nil{}:
      {==}
    case +op <> +t:
      +rs2 = List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)])
      +h2 = allred_app(one, rs, P.exec(op, rs), h, exec_r(one, h1, op, rs, h))
      %Equal.sym(List<&2, Nat>, vals(one, P.run_go(t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]))), CV.run_go(FS.prime(one), cprog(t), vals(one, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]))), run_go_v(one, h1, t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]), h2)) : {_ == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, vals(one, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)])), List.append(&2, Nat, vals(one, rs), [FS.value(one, P.exec(op, rs))]), vals_app(one, rs, P.exec(op, rs))) : {CV.run_go(FS.prime(one), cprog(t), _) == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
      %Equal.sym(Nat, FS.value(one, P.exec(op, rs)), CV.exec(FS.prime(one), cop(op), vals(one, rs)), exec_v(one, h1, op, rs, h)) : {CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [_])) == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
      {==}

Uses (20):
  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=List.append
  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=allred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=allred_app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=cop
  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=exec_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=exec_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=vals_app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=exec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=run_go
  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=Op
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=exec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=run_go