def pk.u8.c6
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
377# the values 192 to 223
378def pk.u8.c6(r: Nat) -> {Nat.is_le(192n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(192n+r))) == 192n+r : Nat}:
379 match r:
380 case 0n:
381 h => {==}
382 case 1n+r1:
383 match r1:
384 case 0n:
385 h => {==}
386 case 1n+r2:
387 match r2:
388 case 0n:
389 h => {==}
390 case 1n+r3:
391 match r3:
392 case 0n:
393 h => {==}
394 case 1n+r4:
395 match r4:
396 case 0n:
397 h => {==}
398 case 1n+r5:
399 match r5:
400 case 0n:
401 h => {==}
402 case 1n+r6:
403 match r6:
404 case 0n:
405 h => {==}
406 case 1n+r7:
407 match r7:
408 case 0n:
409 h => {==}
410 case 1n+r8:
411 match r8:
412 case 0n:
413 h => {==}
414 case 1n+r9:
415 match r9:
416 case 0n:
417 h => {==}
418 case 1n+r10:
419 match r10:
420 case 0n:
421 h => {==}
422 case 1n+r11:
423 match r11:
424 case 0n:
425 h => {==}
426 case 1n+r12:
427 match r12:
428 case 0n:
429 h => {==}
430 case 1n+r13:
431 match r13:
432 case 0n:
433 h => {==}
434 case 1n+r14:
435 match r14:
436 case 0n:
437 h => {==}
438 case 1n+r15:
439 match r15:
440 case 0n:
441 h => {==}
442 case 1n+r16:
443 match r16:
444 case 0n:
445 h => {==}
446 case 1n+r17:
447 match r17:
448 case 0n:
449 h => {==}
450 case 1n+r18:
451 match r18:
452 case 0n:
453 h => {==}
454 case 1n+r19:
455 match r19:
456 case 0n:
457 h => {==}
458 case 1n+r20:
459 match r20:
460 case 0n:
461 h => {==}
462 case 1n+r21:
463 match r21:
464 case 0n:
465 h => {==}
466 case 1n+r22:
467 match r22:
468 case 0n:
469 h => {==}
470 case 1n+r23:
471 match r23:
472 case 0n:
473 h => {==}
474 case 1n+r24:
475 match r24:
476 case 0n:
477 h => {==}
478 case 1n+r25:
479 match r25:
480 case 0n:
481 h => {==}
482 case 1n+r26:
483 match r26:
484 case 0n:
485 h => {==}
486 case 1n+r27:
487 match r27:
488 case 0n:
489 h => {==}
490 case 1n+r28:
491 match r28:
492 case 0n:
493 h => {==}
494 case 1n+r29:
495 match r29:
496 case 0n:
497 h => {==}
498 case 1n+r30:
499 match r30:
500 case 0n:
501 h => {==}
502 case 1n+r31:
503 match r31:
504 case 0n:
505 h => {==}
506 case 1n+r32:
507 pk.u8.c7(r32)