def sp_nib_0_t

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

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

503def sp_nib_0_t(+n: P.LcSpNib) -> {n == P.sp.nib(P.LcSp0{}, False{}, P.LcSpNib{P.sp.na(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nb(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nc(P.sp.nib(P.LcSp0{}, True{}, n)), P.sp.nd(P.sp.nib(P.LcSp0{}, True{}, n))}) : P.LcSpNib}:
504  match n:
505    case P.LcSpNib{a, b, c, d}:
506      match a b c d:
507        case True{} True{} True{} True{}:
508          {==}
509        case True{} True{} True{} False{}:
510          {==}
511        case True{} True{} False{} True{}:
512          {==}
513        case True{} True{} False{} False{}:
514          {==}
515        case True{} False{} True{} True{}:
516          {==}
517        case True{} False{} True{} False{}:
518          {==}
519        case True{} False{} False{} True{}:
520          {==}
521        case True{} False{} False{} False{}:
522          {==}
523        case False{} True{} True{} True{}:
524          {==}
525        case False{} True{} True{} False{}:
526          {==}
527        case False{} True{} False{} True{}:
528          {==}
529        case False{} True{} False{} False{}:
530          {==}
531        case False{} False{} True{} True{}:
532          {==}
533        case False{} False{} True{} False{}:
534          {==}
535        case False{} False{} False{} True{}:
536          {==}
537        case False{} False{} False{} False{}:
538          {==}