SubtleEq.step: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend as SubtleEq
Lines 10-15 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&start_line=10&end_line=15

import Base

law step:
  for +acc: U32
  for +x: U32
  for +y: U32
  for +e: Bool
  {Bool.and(U32.is_eq(U32.or(acc, U32.xor(x, y)), 0), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}

Uses (10):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=and_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=u32_or_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=u32_xor_zero