def shl_wof

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

import Base

371def shl_wof(+n: Nat, +l: List<&2, Bool>) -> {Word.shl(n, wof(n, l)) == wof(n, False{} <> l) : Word(n)}:
372  match n l:
373    case 0n _:
374      {==}
375    case 1n+p Nil{}:
376      %wof_false_nil(p) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
377      %put_wof(p, False{}, Nil{}) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
378      {==}
379    case 1n+p x <> xs:
380      %put_wof(p, x, xs) : {WCon{False{}, Word.shl.put(p, x, wof(p, xs))} == WCon{False{}, _} : Word(1n+p)}
381      {==}