def ks_after_append

bend-osdev-crypto@0.1.0.0 · PROOF.bend:208

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/stream.bend as St

208def ks_after_append(~S: Data, ~next: S -> St.CrKsStep<S>, xs: List<&2, U32>, +ys: List<&2, U32>, +s: S) -> {St.cr.ks.after(~S, ~next, B.append(xs, ys), s) == St.cr.ks.after(~S, ~next, ys, St.cr.ks.after(~S, ~next, xs, s)) : S}:
209  match xs:
210    case Nil{}:
211      {==}
212    case Con{x, t}:
213      ks_after_append(~S, ~next, t, ys, St.CrKsStep.st(~S, next(s)))