def xor_zero_l

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

import Base

95def xor_zero_l(+n: Nat, +w: Word(n)) -> {Word.xor(n, Word.zero(n), w) == w : Word(n)}:
96  match n w:
97    case 0n WNil{}:
98      {==}
99    case 1n+p WCon{b, t}:
100      %xor_zero_l(p, t) : {WCon{b, Word.xor(p, Word.zero(p), t)} == WCon{b, _} : Word(1n+p)}
101      {==}