def sp_nib_6_t

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

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

947def sp_nib_6_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp6{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp6{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp6{}, True{}, n))}) : P.LcSpNib}:
948  match n:
949    case P.LcSpNib{a, b, c, d}:
950      match a b c d:
951        case True{} True{} True{} True{}:
952          {==}
953        case True{} True{} True{} False{}:
954          {==}
955        case True{} True{} False{} True{}:
956          {==}
957        case True{} True{} False{} False{}:
958          {==}
959        case True{} False{} True{} True{}:
960          {==}
961        case True{} False{} True{} False{}:
962          {==}
963        case True{} False{} False{} True{}:
964          {==}
965        case True{} False{} False{} False{}:
966          {==}
967        case False{} True{} True{} True{}:
968          {==}
969        case False{} True{} True{} False{}:
970          {==}
971        case False{} True{} False{} True{}:
972          {==}
973        case False{} True{} False{} False{}:
974          {==}
975        case False{} False{} True{} True{}:
976          {==}
977        case False{} False{} True{} False{}:
978          {==}
979        case False{} False{} False{} True{}:
980          {==}
981        case False{} False{} False{} False{}:
982          {==}