PROOF.tdes_rt: def of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
Lines 8622-8623 of bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=8622&end_line=8623

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend as T
import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as Laws

def tdes_rt(k: T.LcTdesKey, +b: L.LcBlock64) -> {b == T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)) : L.LcBlock64}:
  Equal.sym(L.LcBlock64, T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)), b, Laws.tdes_round_trip(k, b))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&name=tdes_round_trip
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend&name=LcTdes.decrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend&name=LcTdes.encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend&name=LcTdesKey