PROOF.feed_append: def of bend-osdev-hashes@0.1.0.0
Import: import bend-osdev-hashes@0.1.0.0/PROOF.bend as PROOF
Lines 16-22 of bend-osdev-hashes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&start_line=16&end_line=22

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs

# The engine: feeding xs ++ ys is feeding xs, then ys (induction on xs)
def feed_append(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, xs: List<&2, U32>, +ys: List<&2, U32>, s: Hs.HsMdState<C>) -> {Hs.hs.md.feed(~C, ~compress, ~last, B.append(xs, ys), s) == Hs.hs.md.feed(~C, ~compress, ~last, ys, Hs.hs.md.feed(~C, ~compress, ~last, xs, s)) : Hs.HsMdState<C>}:
  match xs:
    case Nil{}:
      {==}
    case Con{x, t}:
      feed_append(~C, ~compress, ~last, t, ys, Hs.hs.md.step(~C, ~compress, ~last, s, x))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/hashes.bend&name=HsMdState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/hashes.bend&name=hs.md.feed
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/hashes.bend&name=hs.md.step