def sp_nib_1_t

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

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

577def sp_nib_1_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp1{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp1{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp1{}, True{}, n))}) : P.LcSpNib}:
578  match n:
579    case P.LcSpNib{a, b, c, d}:
580      match a b c d:
581        case True{} True{} True{} True{}:
582          {==}
583        case True{} True{} True{} False{}:
584          {==}
585        case True{} True{} False{} True{}:
586          {==}
587        case True{} True{} False{} False{}:
588          {==}
589        case True{} False{} True{} True{}:
590          {==}
591        case True{} False{} True{} False{}:
592          {==}
593        case True{} False{} False{} True{}:
594          {==}
595        case True{} False{} False{} False{}:
596          {==}
597        case False{} True{} True{} True{}:
598          {==}
599        case False{} True{} True{} False{}:
600          {==}
601        case False{} True{} False{} True{}:
602          {==}
603        case False{} True{} False{} False{}:
604          {==}
605        case False{} False{} True{} True{}:
606          {==}
607        case False{} False{} True{} False{}:
608          {==}
609        case False{} False{} False{} True{}:
610          {==}
611        case False{} False{} False{} False{}:
612          {==}