PROOF.sp_lt_inv: 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 1248-1256 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=1248&end_line=1256

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_inv(+s: M.CmBlock) -> {s == P.sp.ilt(P.sp.lt(s)) : M.CmBlock}:
  %sp_lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(_))))))) : M.CmBlock}
  %sp_lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(_)))))) : M.CmBlock}
  %sp_lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(_))))) : M.CmBlock}
  %sp_lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(_)))) : M.CmBlock}
  %sp_lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(_))) : M.CmBlock}
  %sp_lt3(P.sp.lt2(P.sp.lt1(s))) : {s == P.sp.ilt1(P.sp.ilt2(_)) : M.CmBlock}
  %sp_lt2(P.sp.lt1(s)) : {s == P.sp.ilt1(_) : M.CmBlock}
  sp_lt1(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_lt1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_lt2
  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_lt5
  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_lt8
  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.ilt1
  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.lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.lt1
  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