def c6_unrun_run

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1701

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend as C6

1701def c6_unrun_run(os: List<&2, C6.LcCast6Op>, +s: M.CmBlock) -> {s == C6.c6.unrun(os, C6.c6.run(os, s)) : M.CmBlock}:
1702  match os:
1703    case Nil{}:
1704      {==}
1705    case Con{+o, +t}:
1706      %c6_unrun_run(t, C6.c6.op(o, s)) : {s == C6.c6.unop(o, _) : M.CmBlock}
1707      c6_unop_op(o, s)