def pk.u8.c5
import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
509# the values 160 to 191
510def pk.u8.c5(r: Nat) -> {Nat.is_le(160n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(160n+r))) == 160n+r : Nat}:
511 match r:
512 case 0n:
513 h => {==}
514 case 1n+r1:
515 match r1:
516 case 0n:
517 h => {==}
518 case 1n+r2:
519 match r2:
520 case 0n:
521 h => {==}
522 case 1n+r3:
523 match r3:
524 case 0n:
525 h => {==}
526 case 1n+r4:
527 match r4:
528 case 0n:
529 h => {==}
530 case 1n+r5:
531 match r5:
532 case 0n:
533 h => {==}
534 case 1n+r6:
535 match r6:
536 case 0n:
537 h => {==}
538 case 1n+r7:
539 match r7:
540 case 0n:
541 h => {==}
542 case 1n+r8:
543 match r8:
544 case 0n:
545 h => {==}
546 case 1n+r9:
547 match r9:
548 case 0n:
549 h => {==}
550 case 1n+r10:
551 match r10:
552 case 0n:
553 h => {==}
554 case 1n+r11:
555 match r11:
556 case 0n:
557 h => {==}
558 case 1n+r12:
559 match r12:
560 case 0n:
561 h => {==}
562 case 1n+r13:
563 match r13:
564 case 0n:
565 h => {==}
566 case 1n+r14:
567 match r14:
568 case 0n:
569 h => {==}
570 case 1n+r15:
571 match r15:
572 case 0n:
573 h => {==}
574 case 1n+r16:
575 match r16:
576 case 0n:
577 h => {==}
578 case 1n+r17:
579 match r17:
580 case 0n:
581 h => {==}
582 case 1n+r18:
583 match r18:
584 case 0n:
585 h => {==}
586 case 1n+r19:
587 match r19:
588 case 0n:
589 h => {==}
590 case 1n+r20:
591 match r20:
592 case 0n:
593 h => {==}
594 case 1n+r21:
595 match r21:
596 case 0n:
597 h => {==}
598 case 1n+r22:
599 match r22:
600 case 0n:
601 h => {==}
602 case 1n+r23:
603 match r23:
604 case 0n:
605 h => {==}
606 case 1n+r24:
607 match r24:
608 case 0n:
609 h => {==}
610 case 1n+r25:
611 match r25:
612 case 0n:
613 h => {==}
614 case 1n+r26:
615 match r26:
616 case 0n:
617 h => {==}
618 case 1n+r27:
619 match r27:
620 case 0n:
621 h => {==}
622 case 1n+r28:
623 match r28:
624 case 0n:
625 h => {==}
626 case 1n+r29:
627 match r29:
628 case 0n:
629 h => {==}
630 case 1n+r30:
631 match r30:
632 case 0n:
633 h => {==}
634 case 1n+r31:
635 match r31:
636 case 0n:
637 h => {==}
638 case 1n+r32:
639 pk.u8.c6(r32)