def pk.u8.c3
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
773# the values 96 to 127
774def pk.u8.c3(r: Nat) -> {Nat.is_le(96n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(96n+r))) == 96n+r : Nat}:
775 match r:
776 case 0n:
777 h => {==}
778 case 1n+r1:
779 match r1:
780 case 0n:
781 h => {==}
782 case 1n+r2:
783 match r2:
784 case 0n:
785 h => {==}
786 case 1n+r3:
787 match r3:
788 case 0n:
789 h => {==}
790 case 1n+r4:
791 match r4:
792 case 0n:
793 h => {==}
794 case 1n+r5:
795 match r5:
796 case 0n:
797 h => {==}
798 case 1n+r6:
799 match r6:
800 case 0n:
801 h => {==}
802 case 1n+r7:
803 match r7:
804 case 0n:
805 h => {==}
806 case 1n+r8:
807 match r8:
808 case 0n:
809 h => {==}
810 case 1n+r9:
811 match r9:
812 case 0n:
813 h => {==}
814 case 1n+r10:
815 match r10:
816 case 0n:
817 h => {==}
818 case 1n+r11:
819 match r11:
820 case 0n:
821 h => {==}
822 case 1n+r12:
823 match r12:
824 case 0n:
825 h => {==}
826 case 1n+r13:
827 match r13:
828 case 0n:
829 h => {==}
830 case 1n+r14:
831 match r14:
832 case 0n:
833 h => {==}
834 case 1n+r15:
835 match r15:
836 case 0n:
837 h => {==}
838 case 1n+r16:
839 match r16:
840 case 0n:
841 h => {==}
842 case 1n+r17:
843 match r17:
844 case 0n:
845 h => {==}
846 case 1n+r18:
847 match r18:
848 case 0n:
849 h => {==}
850 case 1n+r19:
851 match r19:
852 case 0n:
853 h => {==}
854 case 1n+r20:
855 match r20:
856 case 0n:
857 h => {==}
858 case 1n+r21:
859 match r21:
860 case 0n:
861 h => {==}
862 case 1n+r22:
863 match r22:
864 case 0n:
865 h => {==}
866 case 1n+r23:
867 match r23:
868 case 0n:
869 h => {==}
870 case 1n+r24:
871 match r24:
872 case 0n:
873 h => {==}
874 case 1n+r25:
875 match r25:
876 case 0n:
877 h => {==}
878 case 1n+r26:
879 match r26:
880 case 0n:
881 h => {==}
882 case 1n+r27:
883 match r27:
884 case 0n:
885 h => {==}
886 case 1n+r28:
887 match r28:
888 case 0n:
889 h => {==}
890 case 1n+r29:
891 match r29:
892 case 0n:
893 h => {==}
894 case 1n+r30:
895 match r30:
896 case 0n:
897 h => {==}
898 case 1n+r31:
899 match r31:
900 case 0n:
901 h => {==}
902 case 1n+r32:
903 pk.u8.c4(r32)