def sp_nib_2_f

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

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

688def sp_nib_2_f(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp2{}, True{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nb(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nc(P.sp.nib(P.LcSp2{}, False{}, n)), P.sp.nd(P.sp.nib(P.LcSp2{}, False{}, n))}) : P.LcSpNib}:
689  match n:
690    case P.LcSpNib{a, b, c, d}:
691      match a b c d:
692        case True{} True{} True{} True{}:
693          {==}
694        case True{} True{} True{} False{}:
695          {==}
696        case True{} True{} False{} True{}:
697          {==}
698        case True{} True{} False{} False{}:
699          {==}
700        case True{} False{} True{} True{}:
701          {==}
702        case True{} False{} True{} False{}:
703          {==}
704        case True{} False{} False{} True{}:
705          {==}
706        case True{} False{} False{} False{}:
707          {==}
708        case False{} True{} True{} True{}:
709          {==}
710        case False{} True{} True{} False{}:
711          {==}
712        case False{} True{} False{} True{}:
713          {==}
714        case False{} True{} False{} False{}:
715          {==}
716        case False{} False{} True{} True{}:
717          {==}
718        case False{} False{} True{} False{}:
719          {==}
720        case False{} False{} False{} True{}:
721          {==}
722        case False{} False{} False{} False{}:
723          {==}