def sp_nib_0_f

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:540

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

540def sp_nib_0_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp0{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp0{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp0{}, False{}, n))}) : P.LcSpNib}:
541  match n:
542    case P.LcSpNib{a, b, c, d}:
543      match a b c d:
544        case True{} True{} True{} True{}:
545          {==}
546        case True{} True{} True{} False{}:
547          {==}
548        case True{} True{} False{} True{}:
549          {==}
550        case True{} True{} False{} False{}:
551          {==}
552        case True{} False{} True{} True{}:
553          {==}
554        case True{} False{} True{} False{}:
555          {==}
556        case True{} False{} False{} True{}:
557          {==}
558        case True{} False{} False{} False{}:
559          {==}
560        case False{} True{} True{} True{}:
561          {==}
562        case False{} True{} True{} False{}:
563          {==}
564        case False{} True{} False{} True{}:
565          {==}
566        case False{} True{} False{} False{}:
567          {==}
568        case False{} False{} True{} True{}:
569          {==}
570        case False{} False{} True{} False{}:
571          {==}
572        case False{} False{} False{} True{}:
573          {==}
574        case False{} False{} False{} False{}:
575          {==}