def tr.rr

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

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

896def tr.rr(xs: List<&2, M.CmBlock>, acc: List<&2, M.CmBlock>, b: List<&2, M.CmBlock>) -> {M.cm.blocks.rev_onto(M.cm.blocks.rev_onto(xs, acc), b) == M.cm.blocks.rev_onto(acc, List.append(&2, M.CmBlock, xs, b)) : List<&2, M.CmBlock>}:
897  match xs:
898    case Nil{}:
899      {==}
900    case Con{h, t}:
901      tr.rr(t, Con{h, acc}, b)