PROOF.sp_lt_invd: 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 1258-1266 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=1258&end_line=1266

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/serpent.bend as P

def sp_lt_invd(+s: M.CmBlock) -> {s == P.sp.lt(P.sp.ilt(s)) : M.CmBlock}:
  %sp_lt1d(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(_))))))) : M.CmBlock}
  %sp_lt2d(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(_)))))) : M.CmBlock}
  %sp_lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(_))))) : M.CmBlock}
  %sp_lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(_)))) : M.CmBlock}
  %sp_lt5d(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(_))) : M.CmBlock}
  %sp_lt6(P.sp.lt7(P.sp.ilt8(s))) : {s == P.sp.lt8(P.sp.lt7(_)) : M.CmBlock}
  %sp_lt7(P.sp.ilt8(s)) : {s == P.sp.lt8(_) : M.CmBlock}
  sp_lt8d(s)

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt1d
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt2d
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt5d
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt6
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt7
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt8d
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.ilt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.ilt2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.ilt5
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.ilt8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt5
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt6
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt7
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt8