def sp_nib_4_f

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

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

836def sp_nib_4_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp4{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp4{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp4{}, False{}, n))}) : P.LcSpNib}:
837  match n:
838    case P.LcSpNib{a, b, c, d}:
839      match a b c d:
840        case True{} True{} True{} True{}:
841          {==}
842        case True{} True{} True{} False{}:
843          {==}
844        case True{} True{} False{} True{}:
845          {==}
846        case True{} True{} False{} False{}:
847          {==}
848        case True{} False{} True{} True{}:
849          {==}
850        case True{} False{} True{} False{}:
851          {==}
852        case True{} False{} False{} True{}:
853          {==}
854        case True{} False{} False{} False{}:
855          {==}
856        case False{} True{} True{} True{}:
857          {==}
858        case False{} True{} True{} False{}:
859          {==}
860        case False{} True{} False{} True{}:
861          {==}
862        case False{} True{} False{} False{}:
863          {==}
864        case False{} False{} True{} True{}:
865          {==}
866        case False{} False{} True{} False{}:
867          {==}
868        case False{} False{} False{} True{}:
869          {==}
870        case False{} False{} False{} False{}:
871          {==}