Point.regs7: 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 182-190 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=182&end_line=190

import Base
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/proofs/lib/logic.bend as Lg

def regs7(+one: Nat, +h1: {one == 1n : Nat}, +x1: List<&2, Nat>, +y1: List<&2, Nat>, +z1: List<&2, Nat>, +x2: List<&2, Nat>, +y2: List<&2, Nat>, +z2: List<&2, Nat>, +h: {Bool.and(red(one, x1), Bool.and(red(one, y1), red(one, z1))) == True{} : Bool}, +g: {Bool.and(red(one, x2), Bool.and(red(one, y2), red(one, z2))) == True{} : Bool}) -> {allred(one, [x1, y1, z1, x2, y2, z2, P.b3()]) == True{} : Bool}:
  +hx = Lg.and_left(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h)
  +hy = Lg.and_left(red(one, y1), red(one, z1), Lg.and_right(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h))
  +hz = Lg.and_right(red(one, y1), red(one, z1), Lg.and_right(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h))
  +gx = Lg.and_left(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g)
  +gy = Lg.and_left(red(one, y2), red(one, z2), Lg.and_right(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g))
  +gz = Lg.and_right(red(one, y2), red(one, z2), Lg.and_right(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g))
  +hb = b3_r(one, h1)
  Lg.and_intro(red(one, x1), allred(one, [y1, z1, x2, y2, z2, P.b3()]), hx, Lg.and_intro(red(one, y1), allred(one, [z1, x2, y2, z2, P.b3()]), hy, Lg.and_intro(red(one, z1), allred(one, [x2, y2, z2, P.b3()]), hz, Lg.and_intro(red(one, x2), allred(one, [y2, z2, P.b3()]), gx, Lg.and_intro(red(one, y2), allred(one, [z2, P.b3()]), gy, Lg.and_intro(red(one, z2), allred(one, [P.b3()]), gz, Lg.and_intro(red(one, P.b3()), True{}, hb, {==})))))))

Uses (11):
  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=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=allred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=b3_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=red
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_intro
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=b3