def cancel5

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

import Base

96def cancel5(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [x0, x1, x2, x3, x4] : List<&2, U32>}:
97  %xor_inv(x0, k0) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [_, x1, x2, x3, x4] : List<&2, U32>}
98  %xor_inv(x1, k1) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [U32.xor(U32.xor(x0, k0), k0), _, x2, x3, x4] : List<&2, U32>}
99  %xor_inv(x2, k2) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), _, x3, x4] : List<&2, U32>}
100  %xor_inv(x3, k3) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), _, x4] : List<&2, U32>}
101  %xor_inv(x4, k4) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), _] : List<&2, U32>}
102  {==}