def tr.join_go

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

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

1006def tr.join_go(xs: List<&2, M.CmBlock>, rs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join.go(M.cm.blocks.rev_onto(xs, rs), rest) == M.cm.join.go(rs, M.cm.join_onto(xs, rest)) : List<&2, U32>}:
1007  match xs:
1008    case Nil{}:
1009      {==}
1010    case Con{x, t}:
1011      tr.join_go(t, Con{x, rs}, rest)