{"diffoscope-json-version": 1, "source1": "/srv/reproducible-results/rbuild-debian/r-b-build.oSWLUAXn/b1/why3_1.8.1-1_amd64.changes", "source2": "/srv/reproducible-results/rbuild-debian/r-b-build.oSWLUAXn/b2/why3_1.8.1-1_amd64.changes", "unified_diff": null, "details": [{"source1": "Files", "source2": "Files", "unified_diff": "@@ -1,8 +1,8 @@\n \n 69320da20209ab252f480f2a9d13b23d 870212 debug optional libwhy3-ocaml-dev-dbgsym_1.8.1-1_amd64.deb\n 62cdcb3a92ea4361e29bb54305ee72cf 13053452 ocaml optional libwhy3-ocaml-dev_1.8.1-1_amd64.deb\n bebfe6e244e3f05c2eb2715fc28f00e3 2626404 debug optional why3-dbgsym_1.8.1-1_amd64.deb\n 62386c38ba036d3e6bec2bd0417372a0 1295052 math optional why3-doc-html_1.8.1-1_all.deb\n- 9fbad9c7228e0504c99c3cb090d96c3e 1393624 math optional why3-doc-pdf_1.8.1-1_all.deb\n+ ec10c591bfc5d4684f00ea84da1547ed 1393616 math optional why3-doc-pdf_1.8.1-1_all.deb\n b7e02859b7daa733fda754765b34072d 4273116 math optional why3-examples_1.8.1-1_all.deb\n 15b275cc66ebf59924b666a88dcdf8ba 12389216 math optional why3_1.8.1-1_amd64.deb\n"}, {"source1": "why3-doc-pdf_1.8.1-1_all.deb", "source2": "why3-doc-pdf_1.8.1-1_all.deb", "unified_diff": null, "details": [{"source1": "file list", "source2": "file list", "unified_diff": "@@ -1,3 +1,3 @@\n -rw-r--r-- 0 0 0 4 2025-09-12 12:59:57.000000 debian-binary\n -rw-r--r-- 0 0 0 1292 2025-09-12 12:59:57.000000 control.tar.xz\n--rw-r--r-- 0 0 0 1392140 2025-09-12 12:59:57.000000 data.tar.xz\n+-rw-r--r-- 0 0 0 1392132 2025-09-12 12:59:57.000000 data.tar.xz\n"}, {"source1": "control.tar.xz", "source2": "control.tar.xz", "unified_diff": null, "details": [{"source1": "control.tar", "source2": "control.tar", "unified_diff": null, "details": [{"source1": "./md5sums", "source2": "./md5sums", "unified_diff": null, "details": [{"source1": "./md5sums", "source2": "./md5sums", "comments": ["Files differ"], "unified_diff": null}]}]}]}, {"source1": "data.tar.xz", "source2": "data.tar.xz", "unified_diff": null, "details": [{"source1": "data.tar", "source2": "data.tar", "unified_diff": null, "details": [{"source1": "file list", "source2": "file list", "unified_diff": "@@ -3,10 +3,10 @@\n drwxr-xr-x 0 root (0) root (0) 0 2025-09-12 12:59:57.000000 ./usr/share/\n drwxr-xr-x 0 root (0) root (0) 0 2025-09-12 12:59:57.000000 ./usr/share/doc/\n drwxr-xr-x 0 root (0) root (0) 0 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/\n -rw-r--r-- 0 root (0) root (0) 155 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/NEWS.Debian.gz\n -rw-r--r-- 0 root (0) root (0) 3472 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/changelog.Debian.gz\n -rw-r--r-- 0 root (0) root (0) 18007 2025-06-04 08:59:28.000000 ./usr/share/doc/why3-doc-pdf/changelog.gz\n -rw-r--r-- 0 root (0) root (0) 21606 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/copyright\n--rw-r--r-- 0 root (0) root (0) 1415091 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/manual.pdf\n+-rw-r--r-- 0 root (0) root (0) 1415089 2025-09-12 12:59:57.000000 ./usr/share/doc/why3-doc-pdf/manual.pdf\n drwxr-xr-x 0 root (0) root (0) 0 2025-09-12 12:59:57.000000 ./usr/share/doc-base/\n -rw-r--r-- 0 root (0) root (0) 990 2025-09-12 12:59:57.000000 ./usr/share/doc-base/why3-doc-pdf.why3-manual-pdf\n"}, {"source1": "./usr/share/doc/why3-doc-pdf/manual.pdf", "source2": "./usr/share/doc/why3-doc-pdf/manual.pdf", "unified_diff": null, "details": [{"source1": "dumppdf -at {}", "source2": "dumppdf -at {}", "unified_diff": "@@ -60429,20 +60429,20 @@\n Type\n ObjStm\n N\n 100\n First\n 1004\n Length\n-2951\n+2952\n Filter\n FlateDecode\n \n \n-2602 0 2603 158 2604 293 2605 429 2606 595 2607 731 2609 867 2610 1039 2611 1224 2612 1408
2613 1585 2614 1753 2615 1889 2617 2025 2621 2200 462 2241 466 2278 470 2319 2618 2360 2627 2455
2630 2569 2631 2628 2632 2728 2633 3439 2636 3664 2637 3668 2629 3673 2624 3714 2626 3755 2639 3866
2642 3980 2643 4039 2644 4139 2645 4786 2648 5011 2649 5015 2641 5020 2625 5061 2638 5102 2651 5213
2653 5311 2650 5352 2671 5407 2654 5661 2655 5798 2656 5935 2657 6073 2658 6211 2659 6348 2660 6486
2661 6624 2662 6762 2663 6900 2664 7038 2665 7176 2666 7314 2667 7451 2668 7587 2669 7723 2673 7859
474 7900 478 7937 482 7978 2674 8019 2675 8060 2676 8101 2677 8142 2678 8183 2679 8224 2680 8265
2681 8306 2670 8347 2736 8442 2685 9002 2686 9140 2687 9278 2688 9416 2689 9554 2690 9692 2691 9828
2692 9966 2693 10104 2694 10242 2695 10380 2696 10518 2697 10655 2698 10793 2699 10931 2700 11069 2701 11207
2702 11345 2703 11482 2704 11620 2705 11758 2706 11895 2707 12033 2708 12170 2709 12308 2710 12446 2711 12584
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [111.029 669.35 230.182 680.249]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [226.68 506.361 273.504 517.26]
/A << /S /GoTo /D (section.9.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [259.058 506.361 273.504 517.26]
/A << /S /GoTo /D (section.9.2) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [88.986 460.088 101.499 470.987]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [412.902 460.088 445.469 470.987]
/A << /S /GoTo /D (figure.6.1) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [431.024 460.088 445.469 470.987]
/A << /S /GoTo /D (figure.6.1) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [152.917 442.165 178.989 453.054]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#Int_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [71.004 412.267 160.169 423.166]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#EuclideanDivision_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [85.698 400.312 174.874 411.211]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#ComputerDivision_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [251.763 376.402 301.755 387.301]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/mach.int.html#Int_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [88.986 318.174 111.392 329.073]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/array.html)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [422.794 318.174 455.362 329.073]
/A << /S /GoTo /D (figure.6.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [440.916 318.174 455.362 329.073]
/A << /S /GoTo /D (figure.6.2) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [156.871 300.241 204.204 311.14]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/array.html#Array_)>>
>>
<<
/D [2619 0 R /XYZ 71 757.862 null]
>>
<<
/D [2619 0 R /XYZ 72 720 null]
>>
<<
/D [2619 0 R /XYZ 72 499.397 null]
>>
<<
/D [2619 0 R /XYZ 72 357.483 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R /F76 1168 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2628 0 R
/Resources 2626 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Group 2630 0 R
>>
<<
/Type /Group
/S /Transparency
/I true
/CS /DeviceRGB
>>
<<
/Producer (cairo 1.18.4 \(https://cairographics.org\))
/CreationDate (D:20250912093424-12'00)
>>
<<
/Type /Font
/Subtype /TrueType
/BaseFont /HHRMUP+DejaVuSerif
/FirstChar 32
/LastChar 121
/FontDescriptor 2633 0 R
/Encoding /WinAnsiEncoding
/Widths [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 317.871094 0 0 0 636.230469 0 0 0 0 0 0 0 0 0 0 0 0 0 0 722.167969 0 765.136719 801.757812 729.980469 693.847656 0 872.070312 395.019531 0 0 664.0625 1023.925781 875 819.824219 672.851562 0 752.929688 685.058594 666.992188 842.773438 0 1027.832031 0 0 0 0 0 0 0 0 0 596.191406 640.136719 560.058594 640.136719 591.796875 370.117188 640.136719 0 319.824219 0 0 319.824219 948.242188 644.042969 602.050781 640.136719 0 478.027344 513.183594 401.855469 644.042969 564.941406 855.957031 563.964844 564.941406]
/ToUnicode 2634 0 R
>>
<<
/Type /FontDescriptor
/FontName /HHRMUP+DejaVuSerif
/FontFamily (DejaVu Serif)
/Flags 32
/FontBBox [ -769 -346 2105 1109]
/ItalicAngle 0
/Ascent 928
/Descent -235
/CapHeight 1109
/StemV 80
/StemH 80
/FontFile2 2635 0 R
>>
401
8691
<<
/D [2627 0 R /XYZ 71 757.862 null]
>>
<<
/D [2627 0 R /XYZ 72 669.572 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R >>
/XObject << /Im10 2608 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2640 0 R
/Resources 2638 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Group 2642 0 R
>>
<<
/Type /Group
/S /Transparency
/I true
/CS /DeviceRGB
>>
<<
/Producer (cairo 1.18.4 \(https://cairographics.org\))
/CreationDate (D:20250912093424-12'00)
>>
<<
/Type /Font
/Subtype /TrueType
/BaseFont /UJTOHX+DejaVuSerif
/FirstChar 32
/LastChar 121
/FontDescriptor 2645 0 R
/Encoding /WinAnsiEncoding
/Widths [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 317.871094 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 722.167969 0 0 0 729.980469 0 0 0 395.019531 0 0 664.0625 1023.925781 875 819.824219 672.851562 0 0 685.058594 666.992188 0 0 0 0 0 0 0 0 0 0 0 0 596.191406 0 560.058594 640.136719 591.796875 370.117188 640.136719 644.042969 319.824219 0 0 319.824219 948.242188 644.042969 602.050781 640.136719 640.136719 478.027344 513.183594 401.855469 644.042969 564.941406 855.957031 563.964844 564.941406]
/ToUnicode 2646 0 R
>>
<<
/Type /FontDescriptor
/FontName /UJTOHX+DejaVuSerif
/FontFamily (DejaVu Serif)
/Flags 32
/FontBBox [ -769 -346 2105 1109]
/ItalicAngle 0
/Ascent 928
/Descent -235
/CapHeight 1109
/StemV 80
/StemH 80
/FontFile2 2647 0 R
>>
373
7493
<<
/D [2639 0 R /XYZ 71 757.862 null]
>>
<<
/D [2639 0 R /XYZ 72 697.776 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R >>
/XObject << /Im11 2616 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2652 0 R
/Resources 2650 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
>>
<<
/D [2651 0 R /XYZ 71 757.862 null]
>>
<<
/Font << /F45 876 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2672 0 R
/Resources 2670 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Annots [ 2654 0 R 2655 0 R 2656 0 R 2657 0 R 2658 0 R 2659 0 R 2660 0 R 2661 0 R 2662 0 R 2663 0 R 2664 0 R 2665 0 R 2666 0 R 2667 0 R 2668 0 R 2669 0 R ]
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [139.277 438.874 193.778 449.773]
/A << /S /GoTo /D (section.5.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [197.214 438.874 241.254 449.773]
/A << /S /GoTo /D (section.5.3) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [154.192 290.936 177.489 299.763]
/A << /S /GoTo /D (section*.236) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [154.192 277.317 203.462 287.808]
/A << /S /GoTo /D (section*.237) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [217.16 277.317 272.134 287.808]
/A << /S /GoTo /D (section*.238) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [285.833 277.317 377.419 287.808]
/A << /S /GoTo /D (section*.250) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [164.652 185.316 224.383 195.707]
/A << /S /GoTo /D (section*.239) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [306.077 185.316 339.695 195.707]
/A << /S /GoTo /D (section*.240) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [369.085 185.316 392.203 195.707]
/A << /S /GoTo /D (section*.242) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [400.672 185.316 429.732 195.707]
/A << /S /GoTo /D (section*.245) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [164.652 161.406 193.643 171.797]
/A << /S /GoTo /D (section*.241) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [223.033 161.406 252.024 171.797]
/A << /S /GoTo /D (section*.241) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 99.193 240.717 109.584]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [227.417 87.546 251.178 97.629]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [227.417 75.591 251.178 85.673]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [280.567 75.591 304.328 85.673]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/D [2671 0 R /XYZ 71 757.862 null]
>>
<<
/D [2671 0 R /XYZ 72 720 null]
>>
<<
/D [2671 0 R /XYZ 72 418.883 null]
>>
<<
/D [2671 0 R /XYZ 72 364.049 null]
>>
<<
/D [2671 0 R /XYZ 72 301.816 null]
>>
<<
/D [2671 0 R /XYZ 72 291.933 null]
>>
<<
/D [2671 0 R /XYZ 72 278.314 null]
>>
<<
/D [2671 0 R /XYZ 72 196.345 null]
>>
<<
/D [2671 0 R /XYZ 72 186.312 null]
>>
<<
/D [2671 0 R /XYZ 72 174.357 null]
>>
<<
/D [2671 0 R /XYZ 72 162.402 null]
>>
<<
/D [2671 0 R /XYZ 72 110.221 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F78 1170 0 R /F74 926 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2737 0 R
/Resources 2735 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Annots [ 2685 0 R 2686 0 R 2687 0 R 2688 0 R 2689 0 R 2690 0 R 2691 0 R 2692 0 R 2693 0 R 2694 0 R 2695 0 R 2696 0 R 2697 0 R 2698 0 R 2699 0 R 2700 0 R 2701 0 R 2702 0 R 2703 0 R 2704 0 R 2705 0 R 2706 0 R 2707 0 R 2708 0 R 2709 0 R 2710 0 R 2711 0 R 2712 0 R 2713 0 R 2714 0 R 2715 0 R 2716 0 R 2717 0 R 2718 0 R 2719 0 R 2720 0 R 2721 0 R 2722 0 R 2723 0 R 2724 0 R 2725 0 R 2726 0 R 2727 0 R 2728 0 R 2729 0 R 2730 0 R 2731 0 R 2732 0 R 2733 0 R 2734 0 R ]
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 659.102 240.269 669.493]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 647.146 240.269 657.537]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [295.412 635.191 318.724 645.582]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [159.422 623.236 182.734 633.627]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [217.355 623.236 240.667 633.627]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [138.5 611.281 161.813 621.672]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [614.863 611.281 638.175 621.672]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [222.186 599.326 245.499 609.717]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [274.889 599.326 298.201 609.717]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [159.422 575.415 182.734 585.806]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 513.202 240.269 523.593]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [279.72 489.292 303.033 499.683]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 465.382 240.269 475.773]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [264.428 465.382 287.691 475.773]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 453.426 240.269 463.818]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [264.428 453.426 287.691 463.818]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [327.541 453.426 350.804 463.818]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [232.647 441.471 255.96 451.862]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [280.119 441.471 329.703 451.862]
/A << /S /GoTo /D (section*.248) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [222.186 429.516 271.601 439.907]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [295.76 429.516 319.073 439.907]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [343.232 429.516 392.647 439.907]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [416.806 429.516 466.39 439.907]
/A << /S /GoTo /D (section*.248) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [169.883 417.561 219.297 427.952]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [169.883 406.024 198.944 415.997]
/A << /S /GoTo /D (section*.245) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [379.098 382.004 402.858 392.087]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [180.343 370.159 203.606 380.131]
/A << /S /GoTo /D (section*.244) >>
>>
\n+2602 0 2603 158 2604 293 2605 429 2606 595 2607 731 2609 867 2610 1039 2611 1224 2612 1408
2613 1585 2614 1753 2615 1889 2617 2025 2621 2200 462 2241 466 2278 470 2319 2618 2360 2627 2455
2630 2569 2631 2628 2632 2728 2633 3439 2636 3664 2637 3668 2629 3673 2624 3714 2626 3755 2639 3866
2642 3980 2643 4039 2644 4139 2645 4786 2648 5011 2649 5015 2641 5020 2625 5061 2638 5102 2651 5213
2653 5311 2650 5352 2671 5407 2654 5661 2655 5798 2656 5935 2657 6073 2658 6211 2659 6348 2660 6486
2661 6624 2662 6762 2663 6900 2664 7038 2665 7176 2666 7314 2667 7451 2668 7587 2669 7723 2673 7859
474 7900 478 7937 482 7978 2674 8019 2675 8060 2676 8101 2677 8142 2678 8183 2679 8224 2680 8265
2681 8306 2670 8347 2736 8442 2685 9002 2686 9140 2687 9278 2688 9416 2689 9554 2690 9692 2691 9828
2692 9966 2693 10104 2694 10242 2695 10380 2696 10518 2697 10655 2698 10793 2699 10931 2700 11069 2701 11207
2702 11345 2703 11482 2704 11620 2705 11758 2706 11895 2707 12033 2708 12170 2709 12308 2710 12446 2711 12584
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [111.029 669.35 230.182 680.249]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [226.68 506.361 273.504 517.26]
/A << /S /GoTo /D (section.9.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [259.058 506.361 273.504 517.26]
/A << /S /GoTo /D (section.9.2) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [88.986 460.088 101.499 470.987]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [412.902 460.088 445.469 470.987]
/A << /S /GoTo /D (figure.6.1) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [431.024 460.088 445.469 470.987]
/A << /S /GoTo /D (figure.6.1) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [152.917 442.165 178.989 453.054]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#Int_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [71.004 412.267 160.169 423.166]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#EuclideanDivision_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [85.698 400.312 174.874 411.211]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/int.html#ComputerDivision_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [251.763 376.402 301.755 387.301]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/mach.int.html#Int_)>>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [88.986 318.174 111.392 329.073]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/array.html)>>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [422.794 318.174 455.362 329.073]
/A << /S /GoTo /D (figure.6.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [440.916 318.174 455.362 329.073]
/A << /S /GoTo /D (figure.6.2) >>
>>
<<
/Type /Annot
/Border[0 0 0]/H/I/C[0 1 1]
/Rect [156.871 300.241 204.204 311.14]
/Subtype/Link/A<</Type/Action/S/URI/URI(https://www.why3.org/stdlib/array.html#Array_)>>
>>
<<
/D [2619 0 R /XYZ 71 757.862 null]
>>
<<
/D [2619 0 R /XYZ 72 720 null]
>>
<<
/D [2619 0 R /XYZ 72 499.397 null]
>>
<<
/D [2619 0 R /XYZ 72 357.483 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R /F76 1168 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2628 0 R
/Resources 2626 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Group 2630 0 R
>>
<<
/Type /Group
/S /Transparency
/I true
/CS /DeviceRGB
>>
<<
/Producer (cairo 1.18.4 \(https://cairographics.org\))
/CreationDate (D:20261016181307+14'00)
>>
<<
/Type /Font
/Subtype /TrueType
/BaseFont /HHRMUP+DejaVuSerif
/FirstChar 32
/LastChar 121
/FontDescriptor 2633 0 R
/Encoding /WinAnsiEncoding
/Widths [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 317.871094 0 0 0 636.230469 0 0 0 0 0 0 0 0 0 0 0 0 0 0 722.167969 0 765.136719 801.757812 729.980469 693.847656 0 872.070312 395.019531 0 0 664.0625 1023.925781 875 819.824219 672.851562 0 752.929688 685.058594 666.992188 842.773438 0 1027.832031 0 0 0 0 0 0 0 0 0 596.191406 640.136719 560.058594 640.136719 591.796875 370.117188 640.136719 0 319.824219 0 0 319.824219 948.242188 644.042969 602.050781 640.136719 0 478.027344 513.183594 401.855469 644.042969 564.941406 855.957031 563.964844 564.941406]
/ToUnicode 2634 0 R
>>
<<
/Type /FontDescriptor
/FontName /HHRMUP+DejaVuSerif
/FontFamily (DejaVu Serif)
/Flags 32
/FontBBox [ -769 -346 2105 1109]
/ItalicAngle 0
/Ascent 928
/Descent -235
/CapHeight 1109
/StemV 80
/StemH 80
/FontFile2 2635 0 R
>>
401
8691
<<
/D [2627 0 R /XYZ 71 757.862 null]
>>
<<
/D [2627 0 R /XYZ 72 669.572 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R >>
/XObject << /Im10 2608 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2640 0 R
/Resources 2638 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Group 2642 0 R
>>
<<
/Type /Group
/S /Transparency
/I true
/CS /DeviceRGB
>>
<<
/Producer (cairo 1.18.4 \(https://cairographics.org\))
/CreationDate (D:20261016181307+14'00)
>>
<<
/Type /Font
/Subtype /TrueType
/BaseFont /UJTOHX+DejaVuSerif
/FirstChar 32
/LastChar 121
/FontDescriptor 2645 0 R
/Encoding /WinAnsiEncoding
/Widths [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 317.871094 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 722.167969 0 0 0 729.980469 0 0 0 395.019531 0 0 664.0625 1023.925781 875 819.824219 672.851562 0 0 685.058594 666.992188 0 0 0 0 0 0 0 0 0 0 0 0 596.191406 0 560.058594 640.136719 591.796875 370.117188 640.136719 644.042969 319.824219 0 0 319.824219 948.242188 644.042969 602.050781 640.136719 640.136719 478.027344 513.183594 401.855469 644.042969 564.941406 855.957031 563.964844 564.941406]
/ToUnicode 2646 0 R
>>
<<
/Type /FontDescriptor
/FontName /UJTOHX+DejaVuSerif
/FontFamily (DejaVu Serif)
/Flags 32
/FontBBox [ -769 -346 2105 1109]
/ItalicAngle 0
/Ascent 928
/Descent -235
/CapHeight 1109
/StemV 80
/StemH 80
/FontFile2 2647 0 R
>>
373
7493
<<
/D [2639 0 R /XYZ 71 757.862 null]
>>
<<
/D [2639 0 R /XYZ 72 697.776 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F74 926 0 R >>
/XObject << /Im11 2616 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2652 0 R
/Resources 2650 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
>>
<<
/D [2651 0 R /XYZ 71 757.862 null]
>>
<<
/Font << /F45 876 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2672 0 R
/Resources 2670 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Annots [ 2654 0 R 2655 0 R 2656 0 R 2657 0 R 2658 0 R 2659 0 R 2660 0 R 2661 0 R 2662 0 R 2663 0 R 2664 0 R 2665 0 R 2666 0 R 2667 0 R 2668 0 R 2669 0 R ]
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [139.277 438.874 193.778 449.773]
/A << /S /GoTo /D (section.5.2) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [197.214 438.874 241.254 449.773]
/A << /S /GoTo /D (section.5.3) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [154.192 290.936 177.489 299.763]
/A << /S /GoTo /D (section*.236) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [154.192 277.317 203.462 287.808]
/A << /S /GoTo /D (section*.237) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [217.16 277.317 272.134 287.808]
/A << /S /GoTo /D (section*.238) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [285.833 277.317 377.419 287.808]
/A << /S /GoTo /D (section*.250) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [164.652 185.316 224.383 195.707]
/A << /S /GoTo /D (section*.239) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [306.077 185.316 339.695 195.707]
/A << /S /GoTo /D (section*.240) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [369.085 185.316 392.203 195.707]
/A << /S /GoTo /D (section*.242) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [400.672 185.316 429.732 195.707]
/A << /S /GoTo /D (section*.245) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [164.652 161.406 193.643 171.797]
/A << /S /GoTo /D (section*.241) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [223.033 161.406 252.024 171.797]
/A << /S /GoTo /D (section*.241) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 99.193 240.717 109.584]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [227.417 87.546 251.178 97.629]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [227.417 75.591 251.178 85.673]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [280.567 75.591 304.328 85.673]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/D [2671 0 R /XYZ 71 757.862 null]
>>
<<
/D [2671 0 R /XYZ 72 720 null]
>>
<<
/D [2671 0 R /XYZ 72 418.883 null]
>>
<<
/D [2671 0 R /XYZ 72 364.049 null]
>>
<<
/D [2671 0 R /XYZ 72 301.816 null]
>>
<<
/D [2671 0 R /XYZ 72 291.933 null]
>>
<<
/D [2671 0 R /XYZ 72 278.314 null]
>>
<<
/D [2671 0 R /XYZ 72 196.345 null]
>>
<<
/D [2671 0 R /XYZ 72 186.312 null]
>>
<<
/D [2671 0 R /XYZ 72 174.357 null]
>>
<<
/D [2671 0 R /XYZ 72 162.402 null]
>>
<<
/D [2671 0 R /XYZ 72 110.221 null]
>>
<<
/Font << /F45 876 0 R /F42 925 0 R /F78 1170 0 R /F74 926 0 R >>
/ProcSet [ /PDF /Text ]
>>
<<
/Type /Page
/Contents 2737 0 R
/Resources 2735 0 R
/MediaBox [0 0 612 792]
/Parent 2622 0 R
/Annots [ 2685 0 R 2686 0 R 2687 0 R 2688 0 R 2689 0 R 2690 0 R 2691 0 R 2692 0 R 2693 0 R 2694 0 R 2695 0 R 2696 0 R 2697 0 R 2698 0 R 2699 0 R 2700 0 R 2701 0 R 2702 0 R 2703 0 R 2704 0 R 2705 0 R 2706 0 R 2707 0 R 2708 0 R 2709 0 R 2710 0 R 2711 0 R 2712 0 R 2713 0 R 2714 0 R 2715 0 R 2716 0 R 2717 0 R 2718 0 R 2719 0 R 2720 0 R 2721 0 R 2722 0 R 2723 0 R 2724 0 R 2725 0 R 2726 0 R 2727 0 R 2728 0 R 2729 0 R 2730 0 R 2731 0 R 2732 0 R 2733 0 R 2734 0 R ]
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 659.102 240.269 669.493]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 647.146 240.269 657.537]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [295.412 635.191 318.724 645.582]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [159.422 623.236 182.734 633.627]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [217.355 623.236 240.667 633.627]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [138.5 611.281 161.813 621.672]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [614.863 611.281 638.175 621.672]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [222.186 599.326 245.499 609.717]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [274.889 599.326 298.201 609.717]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [159.422 575.415 182.734 585.806]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 513.202 240.269 523.593]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [279.72 489.292 303.033 499.683]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 465.382 240.269 475.773]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [264.428 465.382 287.691 475.773]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [216.956 453.426 240.269 463.818]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [264.428 453.426 287.691 463.818]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [327.541 453.426 350.804 463.818]
/A << /S /GoTo /D (section*.244) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [232.647 441.471 255.96 451.862]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [280.119 441.471 329.703 451.862]
/A << /S /GoTo /D (section*.248) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [222.186 429.516 271.601 439.907]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [295.76 429.516 319.073 439.907]
/A << /S /GoTo /D (section*.243) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [343.232 429.516 392.647 439.907]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [416.806 429.516 466.39 439.907]
/A << /S /GoTo /D (section*.248) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [169.883 417.561 219.297 427.952]
/A << /S /GoTo /D (section*.246) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [169.883 406.024 198.944 415.997]
/A << /S /GoTo /D (section*.245) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [379.098 382.004 402.858 392.087]
/A << /S /GoTo /D (section*.251) >>
>>
<<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [180.343 370.159 203.606 380.131]
/A << /S /GoTo /D (section*.244) >>
>>
\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n Type\n XRef\n@@ -127435,14 +127435,14 @@\n \n ID\n \n ZßÞ·EÊ/[S·ôì\n ZßÞ·EÊ/[S·ôì\n
\n Length\n-11985\n+11982\n Filter\n FlateDecode\n \n \n \n \n"}]}]}]}]}]}