def regs7

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:182

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

182def 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}:
183  +hx = Lg.and_left(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h)
184  +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))
185  +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))
186  +gx = Lg.and_left(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g)
187  +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))
188  +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))
189  +hb = b3_r(one, h1)
190  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, {==})))))))