def sp_nib_7_t

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

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

1021def sp_nib_7_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp7{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp7{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp7{}, True{}, n))}) : P.LcSpNib}:
1022  match n:
1023    case P.LcSpNib{a, b, c, d}:
1024      match a b c d:
1025        case True{} True{} True{} True{}:
1026          {==}
1027        case True{} True{} True{} False{}:
1028          {==}
1029        case True{} True{} False{} True{}:
1030          {==}
1031        case True{} True{} False{} False{}:
1032          {==}
1033        case True{} False{} True{} True{}:
1034          {==}
1035        case True{} False{} True{} False{}:
1036          {==}
1037        case True{} False{} False{} True{}:
1038          {==}
1039        case True{} False{} False{} False{}:
1040          {==}
1041        case False{} True{} True{} True{}:
1042          {==}
1043        case False{} True{} True{} False{}:
1044          {==}
1045        case False{} True{} False{} True{}:
1046          {==}
1047        case False{} True{} False{} False{}:
1048          {==}
1049        case False{} False{} True{} True{}:
1050          {==}
1051        case False{} False{} True{} False{}:
1052          {==}
1053        case False{} False{} False{} True{}:
1054          {==}
1055        case False{} False{} False{} False{}:
1056          {==}

Uses (8)

Used by (1)