def sp_nib_2_t

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

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

651def sp_nib_2_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp2{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp2{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp2{}, True{}, n))}) : P.LcSpNib}:
652  match n:
653    case P.LcSpNib{a, b, c, d}:
654      match a b c d:
655        case True{} True{} True{} True{}:
656          {==}
657        case True{} True{} True{} False{}:
658          {==}
659        case True{} True{} False{} True{}:
660          {==}
661        case True{} True{} False{} False{}:
662          {==}
663        case True{} False{} True{} True{}:
664          {==}
665        case True{} False{} True{} False{}:
666          {==}
667        case True{} False{} False{} True{}:
668          {==}
669        case True{} False{} False{} False{}:
670          {==}
671        case False{} True{} True{} True{}:
672          {==}
673        case False{} True{} True{} False{}:
674          {==}
675        case False{} True{} False{} True{}:
676          {==}
677        case False{} True{} False{} False{}:
678          {==}
679        case False{} False{} True{} True{}:
680          {==}
681        case False{} False{} True{} False{}:
682          {==}
683        case False{} False{} False{} True{}:
684          {==}
685        case False{} False{} False{} False{}:
686          {==}