def sp_nib_5_f

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

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

910def sp_nib_5_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp5{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp5{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp5{}, False{}, n))}) : P.LcSpNib}:
911  match n:
912    case P.LcSpNib{a, b, c, d}:
913      match a b c d:
914        case True{} True{} True{} True{}:
915          {==}
916        case True{} True{} True{} False{}:
917          {==}
918        case True{} True{} False{} True{}:
919          {==}
920        case True{} True{} False{} False{}:
921          {==}
922        case True{} False{} True{} True{}:
923          {==}
924        case True{} False{} True{} False{}:
925          {==}
926        case True{} False{} False{} True{}:
927          {==}
928        case True{} False{} False{} False{}:
929          {==}
930        case False{} True{} True{} True{}:
931          {==}
932        case False{} True{} True{} False{}:
933          {==}
934        case False{} True{} False{} True{}:
935          {==}
936        case False{} True{} False{} False{}:
937          {==}
938        case False{} False{} True{} True{}:
939          {==}
940        case False{} False{} True{} False{}:
941          {==}
942        case False{} False{} False{} True{}:
943          {==}
944        case False{} False{} False{} False{}:
945          {==}