def sp_nib_3_t

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

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

725def sp_nib_3_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp3{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp3{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp3{}, True{}, n))}) : P.LcSpNib}:
726  match n:
727    case P.LcSpNib{a, b, c, d}:
728      match a b c d:
729        case True{} True{} True{} True{}:
730          {==}
731        case True{} True{} True{} False{}:
732          {==}
733        case True{} True{} False{} True{}:
734          {==}
735        case True{} True{} False{} False{}:
736          {==}
737        case True{} False{} True{} True{}:
738          {==}
739        case True{} False{} True{} False{}:
740          {==}
741        case True{} False{} False{} True{}:
742          {==}
743        case True{} False{} False{} False{}:
744          {==}
745        case False{} True{} True{} True{}:
746          {==}
747        case False{} True{} True{} False{}:
748          {==}
749        case False{} True{} False{} True{}:
750          {==}
751        case False{} True{} False{} False{}:
752          {==}
753        case False{} False{} True{} True{}:
754          {==}
755        case False{} False{} True{} False{}:
756          {==}
757        case False{} False{} False{} True{}:
758          {==}
759        case False{} False{} False{} False{}:
760          {==}