def sp_nib_3_f

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

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

762def sp_nib_3_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp3{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp3{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp3{}, False{}, n))}) : P.LcSpNib}:
763  match n:
764    case P.LcSpNib{a, b, c, d}:
765      match a b c d:
766        case True{} True{} True{} True{}:
767          {==}
768        case True{} True{} True{} False{}:
769          {==}
770        case True{} True{} False{} True{}:
771          {==}
772        case True{} True{} False{} False{}:
773          {==}
774        case True{} False{} True{} True{}:
775          {==}
776        case True{} False{} True{} False{}:
777          {==}
778        case True{} False{} False{} True{}:
779          {==}
780        case True{} False{} False{} False{}:
781          {==}
782        case False{} True{} True{} True{}:
783          {==}
784        case False{} True{} True{} False{}:
785          {==}
786        case False{} True{} False{} True{}:
787          {==}
788        case False{} True{} False{} False{}:
789          {==}
790        case False{} False{} True{} True{}:
791          {==}
792        case False{} False{} True{} False{}:
793          {==}
794        case False{} False{} False{} True{}:
795          {==}
796        case False{} False{} False{} False{}:
797          {==}