Bytes.fill_inv: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
Lines 131-140 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&start_line=131&end_line=140

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

# THEOREM: after k bytes the accumulator, read back, is the old one followed
# by the first k bytes of the pending bytes and the stream
def fill_inv(+k: Nat, +f: CR.Fill) -> {rev(facc(CR.fill(k, f))) == SCR.append(rev(facc(f)), SCR.take(k, SCR.append(fpend(f), SCR.flat(outs(k, fsrc(f)))))) : List<&2, U32>}:
  match k:
    case 0n:
      Equal.sym(List<&2, U32>, SCR.append(rev(facc(f)), []), rev(facc(f)), app_nil(rev(facc(f))))
    case 1n+j:
      Equal.trans(List<&2, U32>, rev(facc(CR.fill(j, CR.take1(f)))), SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))), SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))),
        fill_inv(j, CR.take1(f)),
        step(j, f))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=app_nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=facc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=fpend
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=fsrc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=outs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=rev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=flat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=Fill
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=fill
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=take1