def rT

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/prel.bend:56

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL

56def rT(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, t, d):
57  snd(RL.R(pp, z, c), RL.R(pp, t, d), snd(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h)))