def cancel1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:74

import Base

74def cancel1(+x0: U32, +k0: U32) -> {[U32.xor(U32.xor(x0, k0), k0)] == [x0] : List<&2, U32>}:
75  %xor_inv(x0, k0) : {[U32.xor(U32.xor(x0, k0), k0)] == [_] : List<&2, U32>}
76  {==}