Phc.sv_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
Lines 702-706 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&start_line=702&end_line=706

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

def sv_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sv(PH.sext(x, y, z)) == y : U32}:
  %LW.rt(x) : {PH.sv(PH.sext(_, y, z)) == y : U32}
  %LW.rt(y) : {PH.sv(PH.sext(u(U32.to_nat(x)), _, z)) == _ : U32}
  %LW.rt(z) : {PH.sv(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(y)) : U32}
  sv_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=sv_eq_n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend&name=rt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=sext
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=sv