law step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/subtle_eq.bend:10

import Base

10law step:
11  for +acc: U32
12  for +x: U32
13  for +y: U32
14  for +e: Bool
15  {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}