def sp_nib_7_f

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

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

1058def sp_nib_7_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp7{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp7{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp7{}, False{}, n))}) : P.LcSpNib}:
1059  match n:
1060    case P.LcSpNib{a, b, c, d}:
1061      match a b c d:
1062        case True{} True{} True{} True{}:
1063          {==}
1064        case True{} True{} True{} False{}:
1065          {==}
1066        case True{} True{} False{} True{}:
1067          {==}
1068        case True{} True{} False{} False{}:
1069          {==}
1070        case True{} False{} True{} True{}:
1071          {==}
1072        case True{} False{} True{} False{}:
1073          {==}
1074        case True{} False{} False{} True{}:
1075          {==}
1076        case True{} False{} False{} False{}:
1077          {==}
1078        case False{} True{} True{} True{}:
1079          {==}
1080        case False{} True{} True{} False{}:
1081          {==}
1082        case False{} True{} False{} True{}:
1083          {==}
1084        case False{} True{} False{} False{}:
1085          {==}
1086        case False{} False{} True{} True{}:
1087          {==}
1088        case False{} False{} True{} False{}:
1089          {==}
1090        case False{} False{} False{} True{}:
1091          {==}
1092        case False{} False{} False{} False{}:
1093          {==}