def shl_zero

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

import Base

181def shl_zero(+n: Nat) -> {Word.shl(n, Word.zero(n)) == Word.zero(n) : Word(n)}:
182  match n:
183    case 0n:
184      {==}
185    case 1n+p:
186      %put_zero(p) : {WCon{False{}, Word.shl.put(p, False{}, Word.zero(p))} == WCon{False{}, _} : Word(1n+p)}
187      {==}