PROOF.sp_nib_2_f: 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 688-723 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=688&end_line=723

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

def sp_nib_2_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp2{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp2{}, False{}, n))}) : P.LcSpNib}:
  match n:
    case P.LcSpNib{a, b, c, d}:
      match a b c d:
        case True{} True{} True{} True{}:
          {==}
        case True{} True{} True{} False{}:
          {==}
        case True{} True{} False{} True{}:
          {==}
        case True{} True{} False{} False{}:
          {==}
        case True{} False{} True{} True{}:
          {==}
        case True{} False{} True{} False{}:
          {==}
        case True{} False{} False{} True{}:
          {==}
        case True{} False{} False{} False{}:
          {==}
        case False{} True{} True{} True{}:
          {==}
        case False{} True{} True{} False{}:
          {==}
        case False{} True{} False{} True{}:
          {==}
        case False{} True{} False{} False{}:
          {==}
        case False{} False{} True{} True{}:
          {==}
        case False{} False{} True{} False{}:
          {==}
        case False{} False{} False{} True{}:
          {==}
        case False{} False{} False{} False{}:
          {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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