def sp_nib_5_t

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

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

873def sp_nib_5_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp5{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp5{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp5{}, True{}, n))}) : P.LcSpNib}:
874  match n:
875    case P.LcSpNib{a, b, c, d}:
876      match a b c d:
877        case True{} True{} True{} True{}:
878          {==}
879        case True{} True{} True{} False{}:
880          {==}
881        case True{} True{} False{} True{}:
882          {==}
883        case True{} True{} False{} False{}:
884          {==}
885        case True{} False{} True{} True{}:
886          {==}
887        case True{} False{} True{} False{}:
888          {==}
889        case True{} False{} False{} True{}:
890          {==}
891        case True{} False{} False{} False{}:
892          {==}
893        case False{} True{} True{} True{}:
894          {==}
895        case False{} True{} True{} False{}:
896          {==}
897        case False{} True{} False{} True{}:
898          {==}
899        case False{} True{} False{} False{}:
900          {==}
901        case False{} False{} True{} True{}:
902          {==}
903        case False{} False{} True{} False{}:
904          {==}
905        case False{} False{} False{} True{}:
906          {==}
907        case False{} False{} False{} False{}:
908          {==}