def constant_false_xor

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:250

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P

250def constant_false_xor(+n: Nat) -> {Word.xor(n, P.constant(n, False{}), Word.zero(n)) == Word.zero(n) : Word(n)}:
251  match n:
252    case 0n:
253      {==}
254    case 1n+p:
255      xor_zero_l(1n+p, Word.zero(1n+p))