def put_zero

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

import Base

173def put_zero(+p: Nat) -> {Word.shl.put(p, False{}, Word.zero(p)) == Word.zero(p) : Word(p)}:
174  match p:
175    case 0n:
176      {==}
177    case 1n+q:
178      %put_zero(q) : {WCon{False{}, Word.shl.put(q, False{}, Word.zero(q))} == WCon{False{}, _} : Word(1n+q)}
179      {==}