def sp_nib_1_f

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

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

614def sp_nib_1_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp1{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp1{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp1{}, False{}, n))}) : P.LcSpNib}:
615  match n:
616    case P.LcSpNib{a, b, c, d}:
617      match a b c d:
618        case True{} True{} True{} True{}:
619          {==}
620        case True{} True{} True{} False{}:
621          {==}
622        case True{} True{} False{} True{}:
623          {==}
624        case True{} True{} False{} False{}:
625          {==}
626        case True{} False{} True{} True{}:
627          {==}
628        case True{} False{} True{} False{}:
629          {==}
630        case True{} False{} False{} True{}:
631          {==}
632        case True{} False{} False{} False{}:
633          {==}
634        case False{} True{} True{} True{}:
635          {==}
636        case False{} True{} True{} False{}:
637          {==}
638        case False{} True{} False{} True{}:
639          {==}
640        case False{} True{} False{} False{}:
641          {==}
642        case False{} False{} True{} True{}:
643          {==}
644        case False{} False{} True{} False{}:
645          {==}
646        case False{} False{} False{} True{}:
647          {==}
648        case False{} False{} False{} False{}:
649          {==}