def sp_nib_6_f

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

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

984def sp_nib_6_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp6{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp6{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp6{}, False{}, n))}) : P.LcSpNib}:
985  match n:
986    case P.LcSpNib{a, b, c, d}:
987      match a b c d:
988        case True{} True{} True{} True{}:
989          {==}
990        case True{} True{} True{} False{}:
991          {==}
992        case True{} True{} False{} True{}:
993          {==}
994        case True{} True{} False{} False{}:
995          {==}
996        case True{} False{} True{} True{}:
997          {==}
998        case True{} False{} True{} False{}:
999          {==}
1000        case True{} False{} False{} True{}:
1001          {==}
1002        case True{} False{} False{} False{}:
1003          {==}
1004        case False{} True{} True{} True{}:
1005          {==}
1006        case False{} True{} True{} False{}:
1007          {==}
1008        case False{} True{} False{} True{}:
1009          {==}
1010        case False{} True{} False{} False{}:
1011          {==}
1012        case False{} False{} True{} True{}:
1013          {==}
1014        case False{} False{} True{} False{}:
1015          {==}
1016        case False{} False{} False{} True{}:
1017          {==}
1018        case False{} False{} False{} False{}:
1019          {==}