def pk.u8.c2
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
905# the values 64 to 95
906def pk.u8.c2(r: Nat) -> {Nat.is_le(64n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(64n+r))) == 64n+r : Nat}:
907 match r:
908 case 0n:
909 h => {==}
910 case 1n+r1:
911 match r1:
912 case 0n:
913 h => {==}
914 case 1n+r2:
915 match r2:
916 case 0n:
917 h => {==}
918 case 1n+r3:
919 match r3:
920 case 0n:
921 h => {==}
922 case 1n+r4:
923 match r4:
924 case 0n:
925 h => {==}
926 case 1n+r5:
927 match r5:
928 case 0n:
929 h => {==}
930 case 1n+r6:
931 match r6:
932 case 0n:
933 h => {==}
934 case 1n+r7:
935 match r7:
936 case 0n:
937 h => {==}
938 case 1n+r8:
939 match r8:
940 case 0n:
941 h => {==}
942 case 1n+r9:
943 match r9:
944 case 0n:
945 h => {==}
946 case 1n+r10:
947 match r10:
948 case 0n:
949 h => {==}
950 case 1n+r11:
951 match r11:
952 case 0n:
953 h => {==}
954 case 1n+r12:
955 match r12:
956 case 0n:
957 h => {==}
958 case 1n+r13:
959 match r13:
960 case 0n:
961 h => {==}
962 case 1n+r14:
963 match r14:
964 case 0n:
965 h => {==}
966 case 1n+r15:
967 match r15:
968 case 0n:
969 h => {==}
970 case 1n+r16:
971 match r16:
972 case 0n:
973 h => {==}
974 case 1n+r17:
975 match r17:
976 case 0n:
977 h => {==}
978 case 1n+r18:
979 match r18:
980 case 0n:
981 h => {==}
982 case 1n+r19:
983 match r19:
984 case 0n:
985 h => {==}
986 case 1n+r20:
987 match r20:
988 case 0n:
989 h => {==}
990 case 1n+r21:
991 match r21:
992 case 0n:
993 h => {==}
994 case 1n+r22:
995 match r22:
996 case 0n:
997 h => {==}
998 case 1n+r23:
999 match r23:
1000 case 0n:
1001 h => {==}
1002 case 1n+r24:
1003 match r24:
1004 case 0n:
1005 h => {==}
1006 case 1n+r25:
1007 match r25:
1008 case 0n:
1009 h => {==}
1010 case 1n+r26:
1011 match r26:
1012 case 0n:
1013 h => {==}
1014 case 1n+r27:
1015 match r27:
1016 case 0n:
1017 h => {==}
1018 case 1n+r28:
1019 match r28:
1020 case 0n:
1021 h => {==}
1022 case 1n+r29:
1023 match r29:
1024 case 0n:
1025 h => {==}
1026 case 1n+r30:
1027 match r30:
1028 case 0n:
1029 h => {==}
1030 case 1n+r31:
1031 match r31:
1032 case 0n:
1033 h => {==}
1034 case 1n+r32:
1035 pk.u8.c3(r32)