def regs4

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

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

216def regs4(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {Bool.and(red(one, x), Bool.and(red(one, y), red(one, z))) == True{} : Bool}) -> {allred(one, [x, y, z, P.b3()]) == True{} : Bool}:
217  +hx = Lg.and_left(red(one, x), Bool.and(red(one, y), red(one, z)), h)
218  +hy = Lg.and_left(red(one, y), red(one, z), Lg.and_right(red(one, x), Bool.and(red(one, y), red(one, z)), h))
219  +hz = Lg.and_right(red(one, y), red(one, z), Lg.and_right(red(one, x), Bool.and(red(one, y), red(one, z)), h))
220  +hb = b3_r(one, h1)
221  Lg.and_intro(red(one, x), allred(one, [y, z, P.b3()]), hx, Lg.and_intro(red(one, y), allred(one, [z, P.b3()]), hy, Lg.and_intro(red(one, z), allred(one, [P.b3()]), hz, Lg.and_intro(red(one, P.b3()), True{}, hb, {==}))))