def sp.join_append

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1430

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1430def sp.join_append(bs: List<&2, M.CmBlock>, +x: M.CmBlock, +rest: List<&2, U32>) -> {M.cm.join_onto(List.append(&2, M.CmBlock, bs, Con{x, Nil{}}), rest) == M.cm.join_onto(bs, M.cm.bytes_onto(x, rest)) : List<&2, U32>}:
1431  match bs:
1432    case Nil{}:
1433      {==}
1434    case Con{+b, +t}:
1435      %sp.join_append(t, x, rest) : {M.cm.bytes_onto(b, M.cm.join_onto(List.append(&2, M.CmBlock, t, Con{x, Nil{}}), rest)) == M.cm.bytes_onto(b, _) : List<&2, U32>}
1436      {==}