def sp_nib_4_t

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

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

799def sp_nib_4_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp4{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp4{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp4{}, True{}, n))}) : P.LcSpNib}:
800  match n:
801    case P.LcSpNib{a, b, c, d}:
802      match a b c d:
803        case True{} True{} True{} True{}:
804          {==}
805        case True{} True{} True{} False{}:
806          {==}
807        case True{} True{} False{} True{}:
808          {==}
809        case True{} True{} False{} False{}:
810          {==}
811        case True{} False{} True{} True{}:
812          {==}
813        case True{} False{} True{} False{}:
814          {==}
815        case True{} False{} False{} True{}:
816          {==}
817        case True{} False{} False{} False{}:
818          {==}
819        case False{} True{} True{} True{}:
820          {==}
821        case False{} True{} True{} False{}:
822          {==}
823        case False{} True{} False{} True{}:
824          {==}
825        case False{} True{} False{} False{}:
826          {==}
827        case False{} False{} True{} True{}:
828          {==}
829        case False{} False{} True{} False{}:
830          {==}
831        case False{} False{} False{} True{}:
832          {==}
833        case False{} False{} False{} False{}:
834          {==}