Gf.shl_wof: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend as Gf
Lines 371-381 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend&start_line=371&end_line=381

import Base

def shl_wof(+n: Nat, +l: List<&2, Bool>) -> {Word.shl(n, wof(n, l)) == wof(n, False{} <> l) : Word(n)}:
  match n l:
    case 0n _:
      {==}
    case 1n+p Nil{}:
      %wof_false_nil(p) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
      %put_wof(p, False{}, Nil{}) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
      {==}
    case 1n+p x <> xs:
      %put_wof(p, x, xs) : {WCon{False{}, Word.shl.put(p, x, wof(p, xs))} == WCon{False{}, _} : Word(1n+p)}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.put
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend&name=put_wof
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend&name=wof
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend&name=wof_false_nil