PROOF.sp_nib_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 1095-1144 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=1095&end_line=1144

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as P

def sp_nib_inv(bx: P.LcSpBox, inv: Bool, +n: P.LcSpNib) -> {n == P.sp.nib(bx, Bool.not(inv), P.LcSpNib{P.sp.na(P.sp.nib(bx, inv, n)), P.sp.nb(P.sp.nib(bx, inv, n)), P.sp.nc(P.sp.nib(bx, inv, n)), P.sp.nd(P.sp.nib(bx, inv, n))}) : P.LcSpNib}:
  match bx:
    case P.LcSp0{}:
      match inv:
        case True{}:
          sp_nib_0_t(n)
        case False{}:
          sp_nib_0_f(n)
    case P.LcSp1{}:
      match inv:
        case True{}:
          sp_nib_1_t(n)
        case False{}:
          sp_nib_1_f(n)
    case P.LcSp2{}:
      match inv:
        case True{}:
          sp_nib_2_t(n)
        case False{}:
          sp_nib_2_f(n)
    case P.LcSp3{}:
      match inv:
        case True{}:
          sp_nib_3_t(n)
        case False{}:
          sp_nib_3_f(n)
    case P.LcSp4{}:
      match inv:
        case True{}:
          sp_nib_4_t(n)
        case False{}:
          sp_nib_4_f(n)
    case P.LcSp5{}:
      match inv:
        case True{}:
          sp_nib_5_t(n)
        case False{}:
          sp_nib_5_f(n)
    case P.LcSp6{}:
      match inv:
        case True{}:
          sp_nib_6_t(n)
        case False{}:
          sp_nib_6_f(n)
    case P.LcSp7{}:
      match inv:
        case True{}:
          sp_nib_7_t(n)
        case False{}:
          sp_nib_7_f(n)

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_0_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_0_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_1_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_1_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_2_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_2_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_3_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_3_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_4_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_4_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_5_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_5_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_6_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_6_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_7_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=sp_nib_7_t
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=LcSpBox
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=LcSpNib
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.na
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend&name=sp.nib