Cipher.xor4_cong: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
Lines 85-98 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend&start_line=85&end_line=98

import Base

law xor4_cong:
  for +p: U32
  for +q: U32
  for +r: U32
  for +s: U32
  for +p2: U32
  for +q2: U32
  for +r2: U32
  for +s2: U32
  for +ep: {p == p2 : U32}
  for +eq: {q == q2 : U32}
  for +er: {r == r2 : U32}
  for +es: {s == s2 : U32}
  {U32.xor(U32.xor(U32.xor(p, q), r), s) == U32.xor(U32.xor(U32.xor(p2, q2), r2), s2) : U32}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor