0s autopkgtest [12:40:58]: starting date and time: 2024-03-26 12:40:58+0000 0s autopkgtest [12:40:58]: git checkout: 4a1cd702 l/adt_testbed: don't blame the testbed for unsolvable build deps 0s autopkgtest [12:40:58]: host juju-7f2275-prod-proposed-migration-environment-2; command line: /home/ubuntu/autopkgtest/runner/autopkgtest --output-dir /tmp/autopkgtest-work.43lz3yid/out --timeout-copy=6000 --setup-commands /home/ubuntu/autopkgtest-cloud/worker-config-production/setup-canonical.sh --setup-commands /home/ubuntu/autopkgtest/setup-commands/setup-testbed --apt-pocket=proposed --apt-upgrade paramcoq --timeout-short=300 --timeout-copy=20000 --timeout-build=20000 '--env=ADT_TEST_TRIGGERS=coq/8.18.0+dfsg-1build1 paramcoq/1.1.3+coq8.18-1build1' -- ssh -s /home/ubuntu/autopkgtest/ssh-setup/nova -- --flavor autopkgtest --security-groups autopkgtest-juju-7f2275-prod-proposed-migration-environment-2@bos02-arm64-30.secgroup --name adt-noble-arm64-paramcoq-20240326-124056-juju-7f2275-prod-proposed-migration-environment-2-7ea73e17-6962-4462-b1e4-6b4ed982bb27 --image adt/ubuntu-noble-arm64-server --keyname testbed-juju-7f2275-prod-proposed-migration-environment-2 --net-id=net_prod-proposed-migration -e TERM=linux -e ''"'"'http_proxy=http://squid.internal:3128'"'"'' -e ''"'"'https_proxy=http://squid.internal:3128'"'"'' -e ''"'"'no_proxy=127.0.0.1,127.0.1.1,login.ubuntu.com,localhost,localdomain,novalocal,internal,archive.ubuntu.com,ports.ubuntu.com,security.ubuntu.com,ddebs.ubuntu.com,changelogs.ubuntu.com,launchpadlibrarian.net,launchpadcontent.net,launchpad.net,10.24.0.0/24,keystone.ps5.canonical.com,objectstorage.prodstack5.canonical.com'"'"'' --mirror=http://ftpmaster.internal/ubuntu/ 362s autopkgtest [12:47:00]: testbed dpkg architecture: arm64 363s autopkgtest [12:47:01]: testbed apt version: 2.7.12 363s autopkgtest [12:47:01]: @@@@@@@@@@@@@@@@@@@@ test bed setup 364s Get:1 http://ftpmaster.internal/ubuntu noble-proposed InRelease [117 kB] 365s Get:2 http://ftpmaster.internal/ubuntu noble-proposed/universe Sources [4019 kB] 371s Get:3 http://ftpmaster.internal/ubuntu noble-proposed/main Sources [496 kB] 372s Get:4 http://ftpmaster.internal/ubuntu noble-proposed/restricted Sources [8504 B] 372s Get:5 http://ftpmaster.internal/ubuntu noble-proposed/multiverse Sources [56.0 kB] 372s Get:6 http://ftpmaster.internal/ubuntu noble-proposed/main arm64 Packages [713 kB] 372s Get:7 http://ftpmaster.internal/ubuntu noble-proposed/main arm64 c-n-f Metadata [3144 B] 372s Get:8 http://ftpmaster.internal/ubuntu noble-proposed/restricted arm64 Packages [43.0 kB] 372s Get:9 http://ftpmaster.internal/ubuntu noble-proposed/restricted arm64 c-n-f Metadata [116 B] 372s Get:10 http://ftpmaster.internal/ubuntu noble-proposed/universe arm64 Packages [4305 kB] 373s Get:11 http://ftpmaster.internal/ubuntu noble-proposed/universe arm64 c-n-f Metadata [8528 B] 373s Get:12 http://ftpmaster.internal/ubuntu noble-proposed/multiverse arm64 Packages [70.5 kB] 373s Get:13 http://ftpmaster.internal/ubuntu noble-proposed/multiverse arm64 c-n-f Metadata [116 B] 381s Fetched 9840 kB in 11s (932 kB/s) 382s Reading package lists... 388s Reading package lists... 389s Building dependency tree... 389s Reading state information... 390s Calculating upgrade... 392s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 392s Reading package lists... 393s Building dependency tree... 393s Reading state information... 395s 0 upgraded, 0 newly installed, 0 to remove and 249 not upgraded. 397s sh: Attempting to set up Debian/Ubuntu apt sources automatically 397s sh: Distribution appears to be Ubuntu 400s Reading package lists... 401s Building dependency tree... 401s Reading state information... 403s eatmydata is already the newest version (131-1). 403s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 403s Reading package lists... 403s Building dependency tree... 403s Reading state information... 405s dbus is already the newest version (1.14.10-4ubuntu1). 405s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 405s Reading package lists... 406s Building dependency tree... 406s Reading state information... 408s rng-tools-debian is already the newest version (2.4). 408s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 408s Reading package lists... 409s Building dependency tree... 409s Reading state information... 410s The following packages will be REMOVED: 410s cloud-init* python3-configobj* python3-debconf* 411s 0 upgraded, 0 newly installed, 3 to remove and 0 not upgraded. 411s After this operation, 3256 kB disk space will be freed. 413s (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 75911 files and directories currently installed.) 413s Removing cloud-init (24.1.2-0ubuntu1) ... 415s Removing python3-configobj (5.0.8-3) ... 415s Removing python3-debconf (1.5.86) ... 416s Processing triggers for man-db (2.12.0-3) ... 417s (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 75522 files and directories currently installed.) 417s Purging configuration files for cloud-init (24.1.2-0ubuntu1) ... 420s dpkg: warning: while removing cloud-init, directory '/etc/cloud/cloud.cfg.d' not empty so not removed 420s Processing triggers for rsyslog (8.2312.0-3ubuntu3) ... 420s invoke-rc.d: policy-rc.d denied execution of try-restart. 421s Reading package lists... 421s Building dependency tree... 421s Reading state information... 424s linux-generic is already the newest version (6.8.0-11.11+1). 424s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 424s Hit:1 http://ftpmaster.internal/ubuntu noble InRelease 424s Hit:2 http://ftpmaster.internal/ubuntu noble-updates InRelease 424s Hit:3 http://ftpmaster.internal/ubuntu noble-security InRelease 434s Reading package lists... 434s Reading package lists... 434s Building dependency tree... 434s Reading state information... 436s Calculating upgrade... 437s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 437s Reading package lists... 438s Building dependency tree... 438s Reading state information... 440s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 440s autopkgtest [12:48:18]: rebooting testbed after setup commands that affected boot 612s autopkgtest [12:51:10]: testbed running kernel: Linux 6.8.0-11-generic #11-Ubuntu SMP PREEMPT_DYNAMIC Wed Feb 14 02:53:31 UTC 2024 616s autopkgtest [12:51:14]: @@@@@@@@@@@@@@@@@@@@ apt-source paramcoq 620s Get:1 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (dsc) [2111 B] 620s Get:2 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (tar) [45.8 kB] 620s Get:3 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (diff) [3092 B] 621s gpgv: Signature made Thu Dec 21 15:33:52 2023 UTC 621s gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 621s gpgv: issuer "jpuydt@debian.org" 621s gpgv: Can't check signature: No public key 621s dpkg-source: warning: cannot verify inline signature for ./paramcoq_1.1.3+coq8.18-1.dsc: no acceptable signature found 621s autopkgtest [12:51:19]: testing package paramcoq version 1.1.3+coq8.18-1 621s autopkgtest [12:51:19]: build not needed 622s autopkgtest [12:51:20]: test upstreamtestsuite: preparing testbed 625s Reading package lists... 626s Building dependency tree... 626s Reading state information... 627s Starting pkgProblemResolver with broken count: 0 627s Starting 2 pkgProblemResolver with broken count: 0 627s Done 629s The following additional packages will be installed: 629s coq cpp cpp-13 cpp-13-aarch64-linux-gnu cpp-aarch64-linux-gnu gcc gcc-13 629s gcc-13-aarch64-linux-gnu gcc-aarch64-linux-gnu libasan8 libatomic1 629s libc-dev-bin libc6-dev libcc1-0 libcompiler-libs-ocaml-dev libcoq-core-ocaml 629s libcoq-paramcoq libcoq-stdlib libcrypt-dev libfindlib-ocaml libgcc-13-dev 629s libgomp1 libhwasan0 libisl23 libitm1 liblsan0 libmpc3 libncurses-dev 629s libstdlib-ocaml libstdlib-ocaml-dev libtsan2 libubsan1 libzarith-ocaml 629s linux-libc-dev ocaml ocaml-base ocaml-findlib ocaml-interp rpcsvc-proto 629s Suggested packages: 629s coqide | proofgeneral ledit | readline-editor libcoq-core-ocaml-dev why 629s coq-doc cpp-doc gcc-13-locales cpp-13-doc gcc-multilib manpages-dev autoconf 629s automake libtool flex bison gdb gcc-doc gcc-13-doc gdb-aarch64-linux-gnu 629s glibc-doc ncurses-doc ocaml-doc elpa-tuareg camlp4 629s Recommended packages: 629s manpages manpages-dev libc-devtools ocaml-man libfindlib-ocaml-dev ledit 629s | readline-editor 629s The following NEW packages will be installed: 629s autopkgtest-satdep coq cpp cpp-13 cpp-13-aarch64-linux-gnu 629s cpp-aarch64-linux-gnu gcc gcc-13 gcc-13-aarch64-linux-gnu 629s gcc-aarch64-linux-gnu libasan8 libatomic1 libc-dev-bin libc6-dev libcc1-0 629s libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-paramcoq libcoq-stdlib 629s libcrypt-dev libfindlib-ocaml libgcc-13-dev libgomp1 libhwasan0 libisl23 629s libitm1 liblsan0 libmpc3 libncurses-dev libstdlib-ocaml libstdlib-ocaml-dev 629s libtsan2 libubsan1 libzarith-ocaml linux-libc-dev ocaml ocaml-base 629s ocaml-findlib ocaml-interp rpcsvc-proto 629s 0 upgraded, 40 newly installed, 0 to remove and 0 not upgraded. 629s Need to get 394 MB/394 MB of archives. 629s After this operation, 1251 MB of additional disk space will be used. 629s Get:1 /tmp/autopkgtest.KgeTRG/1-autopkgtest-satdep.deb autopkgtest-satdep arm64 0 [712 B] 630s Get:2 http://ftpmaster.internal/ubuntu noble/universe arm64 libcoq-stdlib arm64 8.18.0+dfsg-1 [35.2 MB] 634s Get:3 http://ftpmaster.internal/ubuntu noble/universe arm64 libstdlib-ocaml arm64 4.14.1-1ubuntu1 [386 kB] 634s Get:4 http://ftpmaster.internal/ubuntu noble/universe arm64 ocaml-base arm64 4.14.1-1ubuntu1 [253 kB] 634s Get:5 http://ftpmaster.internal/ubuntu noble/universe arm64 libfindlib-ocaml arm64 1.9.6-1build3 [206 kB] 634s Get:6 http://ftpmaster.internal/ubuntu noble/universe arm64 libzarith-ocaml arm64 1.13-2build3 [123 kB] 634s Get:7 http://ftpmaster.internal/ubuntu noble/universe arm64 libcoq-core-ocaml arm64 8.18.0+dfsg-1 [35.9 MB] 636s Get:8 http://ftpmaster.internal/ubuntu noble/universe arm64 libstdlib-ocaml-dev arm64 4.14.1-1ubuntu1 [8499 kB] 636s Get:9 http://ftpmaster.internal/ubuntu noble/universe arm64 libcompiler-libs-ocaml-dev arm64 4.14.1-1ubuntu1 [39.0 MB] 638s Get:10 http://ftpmaster.internal/ubuntu noble/universe arm64 ocaml-interp arm64 4.14.1-1ubuntu1 [7825 kB] 639s Get:11 http://ftpmaster.internal/ubuntu noble/main arm64 libc-dev-bin arm64 2.39-0ubuntu6 [19.7 kB] 639s Get:12 http://ftpmaster.internal/ubuntu noble/main arm64 linux-libc-dev arm64 6.8.0-11.11 [1569 kB] 639s Get:13 http://ftpmaster.internal/ubuntu noble/main arm64 libcrypt-dev arm64 1:4.4.36-4 [136 kB] 639s Get:14 http://ftpmaster.internal/ubuntu noble/main arm64 rpcsvc-proto arm64 1.4.2-0ubuntu6 [65.4 kB] 639s Get:15 http://ftpmaster.internal/ubuntu noble/main arm64 libc6-dev arm64 2.39-0ubuntu6 [1596 kB] 639s Get:16 http://ftpmaster.internal/ubuntu noble/main arm64 libncurses-dev arm64 6.4+20240113-1ubuntu1 [385 kB] 639s Get:17 http://ftpmaster.internal/ubuntu noble/main arm64 libisl23 arm64 0.26-3 [713 kB] 639s Get:18 http://ftpmaster.internal/ubuntu noble/main arm64 libmpc3 arm64 1.3.1-1 [55.3 kB] 639s Get:19 http://ftpmaster.internal/ubuntu noble/main arm64 cpp-13-aarch64-linux-gnu arm64 13.2.0-17ubuntu2 [10.3 MB] 640s Get:20 http://ftpmaster.internal/ubuntu noble/main arm64 cpp-13 arm64 13.2.0-17ubuntu2 [1028 B] 640s Get:21 http://ftpmaster.internal/ubuntu noble/main arm64 cpp-aarch64-linux-gnu arm64 4:13.2.0-7ubuntu1 [5316 B] 640s Get:22 http://ftpmaster.internal/ubuntu noble/main arm64 cpp arm64 4:13.2.0-7ubuntu1 [22.4 kB] 640s Get:23 http://ftpmaster.internal/ubuntu noble/main arm64 libcc1-0 arm64 14-20240303-1ubuntu1 [44.7 kB] 640s Get:24 http://ftpmaster.internal/ubuntu noble/main arm64 libgomp1 arm64 14-20240303-1ubuntu1 [144 kB] 640s Get:25 http://ftpmaster.internal/ubuntu noble/main arm64 libitm1 arm64 14-20240303-1ubuntu1 [27.7 kB] 640s Get:26 http://ftpmaster.internal/ubuntu noble/main arm64 libatomic1 arm64 14-20240303-1ubuntu1 [11.4 kB] 640s Get:27 http://ftpmaster.internal/ubuntu noble/main arm64 libasan8 arm64 14-20240303-1ubuntu1 [2919 kB] 640s Get:28 http://ftpmaster.internal/ubuntu noble/main arm64 liblsan0 arm64 14-20240303-1ubuntu1 [1282 kB] 640s Get:29 http://ftpmaster.internal/ubuntu noble/main arm64 libtsan2 arm64 14-20240303-1ubuntu1 [2687 kB] 640s Get:30 http://ftpmaster.internal/ubuntu noble/main arm64 libubsan1 arm64 14-20240303-1ubuntu1 [1151 kB] 640s Get:31 http://ftpmaster.internal/ubuntu noble/main arm64 libhwasan0 arm64 14-20240303-1ubuntu1 [1597 kB] 640s Get:32 http://ftpmaster.internal/ubuntu noble/main arm64 libgcc-13-dev arm64 13.2.0-17ubuntu2 [2464 kB] 640s Get:33 http://ftpmaster.internal/ubuntu noble/main arm64 gcc-13-aarch64-linux-gnu arm64 13.2.0-17ubuntu2 [20.1 MB] 642s Get:34 http://ftpmaster.internal/ubuntu noble/main arm64 gcc-13 arm64 13.2.0-17ubuntu2 [467 kB] 642s Get:35 http://ftpmaster.internal/ubuntu noble/main arm64 gcc-aarch64-linux-gnu arm64 4:13.2.0-7ubuntu1 [1198 B] 642s Get:36 http://ftpmaster.internal/ubuntu noble/main arm64 gcc arm64 4:13.2.0-7ubuntu1 [5018 B] 642s Get:37 http://ftpmaster.internal/ubuntu noble/universe arm64 ocaml arm64 4.14.1-1ubuntu1 [86.0 MB] 646s Get:38 http://ftpmaster.internal/ubuntu noble/universe arm64 ocaml-findlib arm64 1.9.6-1build3 [663 kB] 646s Get:39 http://ftpmaster.internal/ubuntu noble/universe arm64 coq arm64 8.18.0+dfsg-1 [132 MB] 653s Get:40 http://ftpmaster.internal/ubuntu noble/universe arm64 libcoq-paramcoq arm64 1.1.3+coq8.18-1 [178 kB] 654s Fetched 394 MB in 23s (16.9 MB/s) 654s Selecting previously unselected package libcoq-stdlib. 655s (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 75467 files and directories currently installed.) 655s Preparing to unpack .../00-libcoq-stdlib_8.18.0+dfsg-1_arm64.deb ... 655s Unpacking libcoq-stdlib (8.18.0+dfsg-1) ... 662s Selecting previously unselected package libstdlib-ocaml. 662s Preparing to unpack .../01-libstdlib-ocaml_4.14.1-1ubuntu1_arm64.deb ... 662s Unpacking libstdlib-ocaml (4.14.1-1ubuntu1) ... 662s Selecting previously unselected package ocaml-base. 662s Preparing to unpack .../02-ocaml-base_4.14.1-1ubuntu1_arm64.deb ... 662s Unpacking ocaml-base (4.14.1-1ubuntu1) ... 662s Selecting previously unselected package libfindlib-ocaml. 662s Preparing to unpack .../03-libfindlib-ocaml_1.9.6-1build3_arm64.deb ... 662s Unpacking libfindlib-ocaml (1.9.6-1build3) ... 662s Selecting previously unselected package libzarith-ocaml. 662s Preparing to unpack .../04-libzarith-ocaml_1.13-2build3_arm64.deb ... 662s Unpacking libzarith-ocaml (1.13-2build3) ... 662s Selecting previously unselected package libcoq-core-ocaml. 662s Preparing to unpack .../05-libcoq-core-ocaml_8.18.0+dfsg-1_arm64.deb ... 662s Unpacking libcoq-core-ocaml (8.18.0+dfsg-1) ... 665s Selecting previously unselected package libstdlib-ocaml-dev. 665s Preparing to unpack .../06-libstdlib-ocaml-dev_4.14.1-1ubuntu1_arm64.deb ... 665s Unpacking libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... 667s Selecting previously unselected package libcompiler-libs-ocaml-dev. 667s Preparing to unpack .../07-libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1_arm64.deb ... 667s Unpacking libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... 672s Selecting previously unselected package ocaml-interp. 672s Preparing to unpack .../08-ocaml-interp_4.14.1-1ubuntu1_arm64.deb ... 672s Unpacking ocaml-interp (4.14.1-1ubuntu1) ... 672s Selecting previously unselected package libc-dev-bin. 672s Preparing to unpack .../09-libc-dev-bin_2.39-0ubuntu6_arm64.deb ... 672s Unpacking libc-dev-bin (2.39-0ubuntu6) ... 672s Selecting previously unselected package linux-libc-dev:arm64. 672s Preparing to unpack .../10-linux-libc-dev_6.8.0-11.11_arm64.deb ... 672s Unpacking linux-libc-dev:arm64 (6.8.0-11.11) ... 673s Selecting previously unselected package libcrypt-dev:arm64. 673s Preparing to unpack .../11-libcrypt-dev_1%3a4.4.36-4_arm64.deb ... 673s Unpacking libcrypt-dev:arm64 (1:4.4.36-4) ... 673s Selecting previously unselected package rpcsvc-proto. 673s Preparing to unpack .../12-rpcsvc-proto_1.4.2-0ubuntu6_arm64.deb ... 673s Unpacking rpcsvc-proto (1.4.2-0ubuntu6) ... 674s Selecting previously unselected package libc6-dev:arm64. 674s Preparing to unpack .../13-libc6-dev_2.39-0ubuntu6_arm64.deb ... 674s Unpacking libc6-dev:arm64 (2.39-0ubuntu6) ... 674s Selecting previously unselected package libncurses-dev:arm64. 674s Preparing to unpack .../14-libncurses-dev_6.4+20240113-1ubuntu1_arm64.deb ... 674s Unpacking libncurses-dev:arm64 (6.4+20240113-1ubuntu1) ... 674s Selecting previously unselected package libisl23:arm64. 674s Preparing to unpack .../15-libisl23_0.26-3_arm64.deb ... 674s Unpacking libisl23:arm64 (0.26-3) ... 674s Selecting previously unselected package libmpc3:arm64. 675s Preparing to unpack .../16-libmpc3_1.3.1-1_arm64.deb ... 675s Unpacking libmpc3:arm64 (1.3.1-1) ... 675s Selecting previously unselected package cpp-13-aarch64-linux-gnu. 675s Preparing to unpack .../17-cpp-13-aarch64-linux-gnu_13.2.0-17ubuntu2_arm64.deb ... 675s Unpacking cpp-13-aarch64-linux-gnu (13.2.0-17ubuntu2) ... 675s Selecting previously unselected package cpp-13. 675s Preparing to unpack .../18-cpp-13_13.2.0-17ubuntu2_arm64.deb ... 675s Unpacking cpp-13 (13.2.0-17ubuntu2) ... 675s Selecting previously unselected package cpp-aarch64-linux-gnu. 676s Preparing to unpack .../19-cpp-aarch64-linux-gnu_4%3a13.2.0-7ubuntu1_arm64.deb ... 676s Unpacking cpp-aarch64-linux-gnu (4:13.2.0-7ubuntu1) ... 676s Selecting previously unselected package cpp. 676s Preparing to unpack .../20-cpp_4%3a13.2.0-7ubuntu1_arm64.deb ... 676s Unpacking cpp (4:13.2.0-7ubuntu1) ... 676s Selecting previously unselected package libcc1-0:arm64. 676s Preparing to unpack .../21-libcc1-0_14-20240303-1ubuntu1_arm64.deb ... 676s Unpacking libcc1-0:arm64 (14-20240303-1ubuntu1) ... 676s Selecting previously unselected package libgomp1:arm64. 676s Preparing to unpack .../22-libgomp1_14-20240303-1ubuntu1_arm64.deb ... 676s Unpacking libgomp1:arm64 (14-20240303-1ubuntu1) ... 676s Selecting previously unselected package libitm1:arm64. 676s Preparing to unpack .../23-libitm1_14-20240303-1ubuntu1_arm64.deb ... 676s Unpacking libitm1:arm64 (14-20240303-1ubuntu1) ... 676s Selecting previously unselected package libatomic1:arm64. 676s Preparing to unpack .../24-libatomic1_14-20240303-1ubuntu1_arm64.deb ... 676s Unpacking libatomic1:arm64 (14-20240303-1ubuntu1) ... 676s Selecting previously unselected package libasan8:arm64. 676s Preparing to unpack .../25-libasan8_14-20240303-1ubuntu1_arm64.deb ... 676s Unpacking libasan8:arm64 (14-20240303-1ubuntu1) ... 677s Selecting previously unselected package liblsan0:arm64. 677s Preparing to unpack .../26-liblsan0_14-20240303-1ubuntu1_arm64.deb ... 677s Unpacking liblsan0:arm64 (14-20240303-1ubuntu1) ... 677s Selecting previously unselected package libtsan2:arm64. 677s Preparing to unpack .../27-libtsan2_14-20240303-1ubuntu1_arm64.deb ... 677s Unpacking libtsan2:arm64 (14-20240303-1ubuntu1) ... 677s Selecting previously unselected package libubsan1:arm64. 677s Preparing to unpack .../28-libubsan1_14-20240303-1ubuntu1_arm64.deb ... 677s Unpacking libubsan1:arm64 (14-20240303-1ubuntu1) ... 677s Selecting previously unselected package libhwasan0:arm64. 677s Preparing to unpack .../29-libhwasan0_14-20240303-1ubuntu1_arm64.deb ... 677s Unpacking libhwasan0:arm64 (14-20240303-1ubuntu1) ... 678s Selecting previously unselected package libgcc-13-dev:arm64. 678s Preparing to unpack .../30-libgcc-13-dev_13.2.0-17ubuntu2_arm64.deb ... 678s Unpacking libgcc-13-dev:arm64 (13.2.0-17ubuntu2) ... 678s Selecting previously unselected package gcc-13-aarch64-linux-gnu. 678s Preparing to unpack .../31-gcc-13-aarch64-linux-gnu_13.2.0-17ubuntu2_arm64.deb ... 678s Unpacking gcc-13-aarch64-linux-gnu (13.2.0-17ubuntu2) ... 680s Selecting previously unselected package gcc-13. 680s Preparing to unpack .../32-gcc-13_13.2.0-17ubuntu2_arm64.deb ... 680s Unpacking gcc-13 (13.2.0-17ubuntu2) ... 680s Selecting previously unselected package gcc-aarch64-linux-gnu. 680s Preparing to unpack .../33-gcc-aarch64-linux-gnu_4%3a13.2.0-7ubuntu1_arm64.deb ... 680s Unpacking gcc-aarch64-linux-gnu (4:13.2.0-7ubuntu1) ... 680s Selecting previously unselected package gcc. 680s Preparing to unpack .../34-gcc_4%3a13.2.0-7ubuntu1_arm64.deb ... 680s Unpacking gcc (4:13.2.0-7ubuntu1) ... 680s Selecting previously unselected package ocaml. 680s Preparing to unpack .../35-ocaml_4.14.1-1ubuntu1_arm64.deb ... 680s Unpacking ocaml (4.14.1-1ubuntu1) ... 686s Selecting previously unselected package ocaml-findlib. 686s Preparing to unpack .../36-ocaml-findlib_1.9.6-1build3_arm64.deb ... 686s Unpacking ocaml-findlib (1.9.6-1build3) ... 686s Selecting previously unselected package coq. 686s Preparing to unpack .../37-coq_8.18.0+dfsg-1_arm64.deb ... 686s Unpacking coq (8.18.0+dfsg-1) ... 694s Selecting previously unselected package libcoq-paramcoq. 694s Preparing to unpack .../38-libcoq-paramcoq_1.1.3+coq8.18-1_arm64.deb ... 694s Unpacking libcoq-paramcoq (1.1.3+coq8.18-1) ... 694s Selecting previously unselected package autopkgtest-satdep. 694s Preparing to unpack .../39-1-autopkgtest-satdep.deb ... 694s Unpacking autopkgtest-satdep (0) ... 694s Setting up linux-libc-dev:arm64 (6.8.0-11.11) ... 694s Setting up libgomp1:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libcoq-stdlib (8.18.0+dfsg-1) ... 694s Setting up rpcsvc-proto (1.4.2-0ubuntu6) ... 694s Setting up libstdlib-ocaml (4.14.1-1ubuntu1) ... 694s Setting up libmpc3:arm64 (1.3.1-1) ... 694s Setting up libatomic1:arm64 (14-20240303-1ubuntu1) ... 694s Setting up ocaml-base (4.14.1-1ubuntu1) ... 694s Setting up libubsan1:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libhwasan0:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libcrypt-dev:arm64 (1:4.4.36-4) ... 694s Setting up libasan8:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libtsan2:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libisl23:arm64 (0.26-3) ... 694s Setting up libc-dev-bin (2.39-0ubuntu6) ... 694s Setting up libcc1-0:arm64 (14-20240303-1ubuntu1) ... 694s Setting up liblsan0:arm64 (14-20240303-1ubuntu1) ... 694s Setting up libitm1:arm64 (14-20240303-1ubuntu1) ... 694s Setting up cpp-13-aarch64-linux-gnu (13.2.0-17ubuntu2) ... 694s Setting up libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... 694s Setting up libcoq-paramcoq (1.1.3+coq8.18-1) ... 694s Setting up libfindlib-ocaml (1.9.6-1build3) ... 694s Setting up libzarith-ocaml (1.13-2build3) ... 694s Setting up libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... 694s Setting up cpp-aarch64-linux-gnu (4:13.2.0-7ubuntu1) ... 694s Setting up ocaml-interp (4.14.1-1ubuntu1) ... 694s Setting up ocaml-findlib (1.9.6-1build3) ... 694s Setting up libgcc-13-dev:arm64 (13.2.0-17ubuntu2) ... 694s Setting up libcoq-core-ocaml (8.18.0+dfsg-1) ... 694s Setting up libc6-dev:arm64 (2.39-0ubuntu6) ... 694s Setting up libncurses-dev:arm64 (6.4+20240113-1ubuntu1) ... 694s Setting up cpp-13 (13.2.0-17ubuntu2) ... 694s Setting up gcc-13-aarch64-linux-gnu (13.2.0-17ubuntu2) ... 694s Setting up gcc-13 (13.2.0-17ubuntu2) ... 694s Setting up cpp (4:13.2.0-7ubuntu1) ... 694s Setting up gcc-aarch64-linux-gnu (4:13.2.0-7ubuntu1) ... 694s Setting up gcc (4:13.2.0-7ubuntu1) ... 694s Setting up ocaml (4.14.1-1ubuntu1) ... 694s Setting up coq (8.18.0+dfsg-1) ... 694s Setting up autopkgtest-satdep (0) ... 694s Processing triggers for man-db (2.12.0-3) ... 696s Processing triggers for libc-bin (2.39-0ubuntu6) ... 704s (Reading database ... 83215 files and directories currently installed.) 704s Removing autopkgtest-satdep (0) ... 705s autopkgtest [12:52:43]: test upstreamtestsuite: [----------------------- 760s Inductive nat_R : nat -> nat -> Set := 760s nat_R_O_R : nat_R 0 0 760s | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0). 760s 760s Arguments nat_R (_ _)%nat_scope 760s Arguments nat_R_S_R (_ _)%nat_scope _ 760s Variant Queue_R : Queue -> Queue -> Type := 760s Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 760s (t_R : t₁ -> t₂ -> Type) 760s (empty₁ : t₁) (empty₂ : t₂), 760s t_R empty₁ empty₂ -> 760s forall (push₁ : nat -> t₁ -> t₁) 760s (push₂ : nat -> t₂ -> t₂), 760s (forall H H0 : nat, 760s nat_R H H0 -> 760s forall (H1 : t₁) (H2 : t₂), 760s t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) -> 760s forall (pop₁ : t₁ -> option (nat * t₁)) 760s (pop₂ : t₂ -> option (nat * t₂)), 760s (forall (H : t₁) (H0 : t₂), 760s t_R H H0 -> 760s option_R (nat * t₁) (nat * t₂) 760s (prod_R nat nat nat_R t₁ t₂ t_R) 760s (pop₁ H) (pop₂ H0)) -> 760s Queue_R 760s {| 760s t := t₁; 760s empty := empty₁; 760s push := push₁; 760s pop := pop₁ 760s |} 760s {| 760s t := t₂; 760s empty := empty₂; 760s push := push₂; 760s pop := pop₂ 760s |}. 760s 760s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 760s t_R%function_scope empty₁ empty₂ empty_R 760s (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope 760s Queue_R 760s : Queue -> Queue -> Type 760s Variant Queue_R : Queue -> Queue -> Type := 760s Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 760s (t_R : t₁ -> t₂ -> Type) 760s (empty₁ : t₁) (empty₂ : t₂), 760s t_R empty₁ empty₂ -> 760s forall (push₁ : nat -> t₁ -> t₁) 760s (push₂ : nat -> t₂ -> t₂), 760s (forall H H0 : nat, 760s nat_R H H0 -> 760s forall (H1 : t₁) (H2 : t₂), 760s t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) -> 760s forall (pop₁ : t₁ -> option (nat * t₁)) 760s (pop₂ : t₂ -> option (nat * t₂)), 760s (forall (H : t₁) (H0 : t₂), 760s t_R H H0 -> 760s option_R (nat * t₁) (nat * t₂) 760s (prod_R nat nat nat_R t₁ t₂ t_R) 760s (pop₁ H) (pop₂ H0)) -> 760s Bisimilar 760s {| 760s t := t₁; 760s empty := empty₁; 760s push := push₁; 760s pop := pop₁ 760s |} 760s {| 760s t := t₂; 760s empty := empty₂; 760s push := push₂; 760s pop := pop₂ 760s |}. 760s 760s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 760s t_R%function_scope empty₁ empty₂ empty_R 760s (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope 760s File "./ListQueue.v", line 127, characters 36-43: 760s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 760s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 760s File "./ListQueue.v", line 127, characters 36-43: 760s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 760s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 760s File "./ListQueue.v", line 127, characters 36-43: 760s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 760s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 760s program = 760s fun (Q : Queue) (n : nat) => 760s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in 760s let q0 := 760s nat_rect (fun _ : nat => option Q) (Some q) 760s (fun (_ : nat) (q0 : option Q) => 760s do q1 <- q0 760s in do x, q2 <- pop Q q1 760s in do y, q3 <- pop Q q2 in Some (push Q (x + y) q3)) n in 760s do q1 <- q0 in option_map fst (pop Q q1) 760s : Queue -> nat -> option nat 760s 760s Arguments program Q n%nat_scope 760s program 760s : Queue -> nat -> option nat 760s program_R 760s : forall Q₁ Q₂ : Queue, 760s Bisimilar Q₁ Q₂ -> 760s forall n₁ n₂ : nat, 760s nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂) 760s program = 760s fun (Q : Queue) (n : nat) => 760s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in 760s let q0 := 760s nat_rect (fun _ : nat => option Q) (Some q) 760s (fun (_ : nat) (q0 : option Q) => 760s do q1 <- q0 760s in do x, q2 <- pop Q q1 760s in do y, q3 <- pop Q q2 in Some (push Q (x + y) q3)) n in 760s do q1 <- q0 in option_map fst (pop Q q1) 760s : Queue -> nat -> option nat 760s 760s Arguments program Q n%nat_scope 760s program_R = 760s fun (Q₁ Q₂ : Queue) (Q_R : Bisimilar Q₁ Q₂) (n₁ n₂ : nat) (n_R : nat_R n₁ n₂) 760s => 760s let q₁ := nat_rect (fun _ : nat => Q₁) (empty Q₁) (push Q₁) (S n₁) in 760s let q₂ := nat_rect (fun _ : nat => Q₂) (empty Q₂) (push Q₂) (S n₂) in 760s let q_R := 760s nat_rect_R (fun _ : nat => Q₁) (fun _ : nat => Q₂) 760s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) => t_R Q₁ Q₂ Q_R) 760s (empty Q₁) (empty Q₂) (empty_R Q₁ Q₂ Q_R) (push Q₁) 760s (push Q₂) (push_R Q₁ Q₂ Q_R) (S n₁) (S n₂) (nat_R_S_R n₁ n₂ n_R) in 760s let q₁0 := 760s nat_rect (fun _ : nat => option Q₁) (Some q₁) 760s (fun (_ : nat) (q : option Q₁) => 760s do q0 <- q 760s in do x, q1 <- pop Q₁ q0 760s in do y, q2 <- pop Q₁ q1 in Some (push Q₁ (x + y) q2)) n₁ in 760s let q₂0 := 760s nat_rect (fun _ : nat => option Q₂) (Some q₂) 760s (fun (_ : nat) (q : option Q₂) => 760s do q0 <- q 760s in do x, q1 <- pop Q₂ q0 760s in do y, q2 <- pop Q₂ q1 in Some (push Q₂ (x + y) q2)) n₂ in 760s let q_R0 := 760s nat_rect_R (fun _ : nat => option Q₁) (fun _ : nat => option Q₂) 760s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) => 760s option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (Some q₁) (Some q₂) 760s (option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁ q₂ q_R) 760s (fun (_ : nat) (q : option Q₁) => 760s do q0 <- q 760s in do x, q1 <- pop Q₁ q0 760s in do y, q2 <- pop Q₁ q1 in Some (push Q₁ (x + y) q2)) 760s (fun (_ : nat) (q : option Q₂) => 760s do q0 <- q 760s in do x, q1 <- pop Q₂ q0 760s in do y, q2 <- pop Q₂ q1 in Some (push Q₂ (x + y) q2)) 760s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) (q₁1 : option Q₁) 760s (q₂1 : option Q₂) (q_R0 : option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁1 q₂1) => 760s bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ (t_R Q₁ Q₂ Q_R) 760s (fun q : Q₁ => 760s do x, q0 <- pop Q₁ q 760s in do y, q1 <- pop Q₁ q0 in Some (push Q₁ (x + y) q1)) 760s (fun q : Q₂ => 760s do x, q0 <- pop Q₂ q 760s in do y, q1 <- pop Q₂ q0 in Some (push Q₂ (x + y) q1)) 760s (fun (q₁2 : Q₁) (q₂2 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁2 q₂2) => 760s bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ 760s (t_R Q₁ Q₂ Q_R) 760s (fun (x : nat) (q : Q₁) => 760s do y, q0 <- pop Q₁ q in Some (push Q₁ (x + y) q0)) 760s (fun (x : nat) (q : Q₂) => 760s do y, q0 <- pop Q₂ q in Some (push Q₂ (x + y) q0)) 760s (fun (x₁ x₂ : nat) (x_R : nat_R x₁ x₂) (q₁3 : Q₁) 760s (q₂3 : Q₂) (q_R2 : t_R Q₁ Q₂ Q_R q₁3 q₂3) => 760s bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ 760s (t_R Q₁ Q₂ Q_R) 760s (fun (y : nat) (q : Q₁) => Some (push Q₁ (x₁ + y) q)) 760s (fun (y : nat) (q : Q₂) => Some (push Q₂ (x₂ + y) q)) 760s (fun (y₁ y₂ : nat) (y_R : nat_R y₁ y₂) 760s (q₁4 : Q₁) (q₂4 : Q₂) (q_R3 : t_R Q₁ Q₂ Q_R q₁4 q₂4) => 760s option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) 760s (push Q₁ (x₁ + y₁) q₁4) (push Q₂ (x₂ + y₂) q₂4) 760s (push_R Q₁ Q₂ Q_R (x₁ + y₁) (x₂ + y₂) 760s (add_R x₁ x₂ x_R y₁ y₂ y_R) q₁4 q₂4 q_R3)) 760s (pop Q₁ q₁3) (pop Q₂ q₂3) (pop_R Q₁ Q₂ Q_R q₁3 q₂3 q_R2)) 760s (pop Q₁ q₁2) (pop Q₂ q₂2) (pop_R Q₁ Q₂ Q_R q₁2 q₂2 q_R1)) q₁1 q₂1 760s q_R0) n₁ n₂ n_R in 760s bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) nat nat nat_R 760s (fun q : Q₁ => option_map fst (pop Q₁ q)) 760s (fun q : Q₂ => option_map fst (pop Q₂ q)) 760s (fun (q₁1 : Q₁) (q₂1 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁1 q₂1) => 760s option_map_R (nat * Q₁) (nat * Q₂) 760s (prod_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) nat nat nat_R fst fst 760s (fst_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (pop Q₁ q₁1) 760s (pop Q₂ q₂1) (pop_R Q₁ Q₂ Q_R q₁1 q₂1 q_R1)) q₁0 q₂0 q_R0 760s : forall Q₁ Q₂ : Queue, 760s Bisimilar Q₁ Q₂ -> 760s forall n₁ n₂ : nat, 760s nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂) 760s 760s Arguments program_R Q₁ Q₂ Q_R (n₁ n₂)%nat_scope n_R 816s declare_abstraction, evd = SHELF: 816s FUTURE GOALS STACK: 816s 816s declare_abstraction, a = 816s 816s |-n1 816s declare_abstraction, b = 816s 816s |-nat 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-3 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-2 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-1 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-0 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-0 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_O_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 0 0 nat_R_O_R) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-3 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s ---> output has cast : false 816s a_R = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s abstraction, evar_map = SHELF: 816s FUTURE GOALS STACK: 816s 816s add_definition, term = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s add_definition, typ = 816s 816s |-(nat_R n1 n1) 816s add_definition, evd = SHELF: 816s FUTURE GOALS STACK: 816s 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-n1 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-3 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-2 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-1 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-0 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-0 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_O_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 0 0 nat_R_O_R) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-3 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-n1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s ---> output has cast : false 816s a_R = 816s 816s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 816s abstraction, evar_map = EVARS: 816s ?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s declare_abstraction, evd = SHELF: 816s FUTURE GOALS STACK: 816s 816s declare_abstraction, a = 816s 816s |-n2 816s declare_abstraction, b = 816s 816s |-nat 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n2 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-2 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-1 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-0 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-0 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_O_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 0 0 nat_R_O_R) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s a_R = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s abstraction, evar_map = SHELF: 816s FUTURE GOALS STACK: 816s 816s add_definition, term = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s add_definition, typ = 816s 816s |-(nat_R n2 n2) 816s add_definition, evd = SHELF: 816s FUTURE GOALS STACK: 816s 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-n2 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-2 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-1 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-0 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-0 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_O_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-1 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 0 0 nat_R_O_R) 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-S 816s ---> input has cast : false 816s output = 816s 816s |-nat_R_S_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s input = 816s 816s |-n2 816s ---> input has cast : false 816s output = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s ---> output has cast : false 816s a_R = 816s 816s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 816s abstraction, evar_map = EVARS: 816s ?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 816s 816s SHELF:|| 816s FUTURE GOALS STACK:|||| 816s 816s ---> Translating mind body ... 816s ---> computing envs ... 816s translate_mind, env = 816s 816s translate_mind, evd = 816s SHELF: 816s FUTURE GOALS STACK: 816s 816s ---> Adding 'I1' to the environment. 816s ---> translatation of params ... 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> input has cast : false 816s output = 816s 816s |-n1_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-n2 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-n2 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-n2_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-n 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-n 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-n_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translatation of inductive ... 816s ---> mind_nparams = 1 816s ---> mind_nparams_rec = 4 816s ---> mind_nparams_ctxt = 4 816s Arity: 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-Prop 816s ---> Computing arity 816s ---> Substitution: 816s 816s 816s |-(I1 _UNBOUND_REL_5) 816s 816s 816s |-(I1 _UNBOUND_REL_6) 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-n1 816s ---> input has cast : false 816s output = 816s 816s |-n1_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-n2 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-n2 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-n2_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-n 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-n 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-n_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-nat 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s 816s |-nat 816s ---> input has cast : false 816s output = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-nat_R 816s ---> output has cast : false 816s Arity_R after substitution: 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s r_R := n_R : nat_R r₁ r₂ 816s 816s |-(I1 n₁ -> I1 n₂ -> Prop) 816s ---> Computing constructors 816s ---> before translation : 816s 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s 816s |-(let p := n1 in let q := n2 in forall n : nat, let r := n in I1 n) 816s ---> remove uniform parameters : 816s 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-(I1 n) 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-(I1 n) 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-n 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-n 816s ---> input has cast : false 816s output = 816s I1₁ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1₂ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1_R : 816s (let p₁ := n1 in 816s let p₂ := n1 in 816s let p_R := n1_R in 816s let q₁ := n2 in 816s let q₂ := n2 in 816s let q_R := n2_R in 816s fun H H0 : forall n : nat, let r := n in Prop => 816s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 816s (let r₁ := n₁ in 816s let r₂ := n₂ in 816s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 816s (H n₁) (H0 n₂)) I1₁ I1₂ 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s r_R := n_R : nat_R r₁ r₂ 816s 816s |-n_R 816s ---> output has cast : false 816s ---> translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-I1 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-I1 816s ---> input has cast : false 816s output = 816s I1₁ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1₂ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1_R : 816s (let p₁ := n1 in 816s let p₂ := n1 in 816s let p_R := n1_R in 816s let q₁ := n2 in 816s let q₂ := n2 in 816s let q_R := n2_R in 816s fun H H0 : forall n : nat, let r := n in Prop => 816s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 816s (let r₁ := n₁ in 816s let r₂ := n₂ in 816s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 816s (H n₁) (H0 n₂)) I1₁ I1₂ 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s r_R := n_R : nat_R r₁ r₂ 816s 816s |-I1_R 816s ---> output has cast : false 816s ---> exit translate 2 evd env t 816s evd =SHELF: 816s FUTURE GOALS STACK: 816s 816s input = 816s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s p := n1 : nat 816s q := n2 : nat 816s n : nat 816s r := n : nat 816s 816s |-(I1 n) 816s ---> input has cast : false 816s output = 816s I1₁ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1₂ : 816s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 816s I1_R : 816s (let p₁ := n1 in 816s let p₂ := n1 in 816s let p_R := n1_R in 816s let q₁ := n2 in 816s let q₂ := n2 in 816s let q_R := n2_R in 816s fun H H0 : forall n : nat, let r := n in Prop => 816s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 816s (let r₁ := n₁ in 816s let r₂ := n₂ in 816s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 816s (H n₁) (H0 n₂)) I1₁ I1₂ 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s r_R := n_R : nat_R r₁ r₂ 816s 816s |-(I1_R n₁ n₂ n_R) 816s ---> output has cast : false 816s ---> before substitution: 816s 816s 816s |-(_UNBOUND_REL_15 _UNBOUND_REL_8 _UNBOUND_REL_7 _UNBOUND_REL_6 816s _UNBOUND_REL_2 _UNBOUND_REL_1) 816s ---> constructor n°0 816s ---> substitution : 816s 816s 816s |-(c1 _UNBOUND_REL_5) 816s 816s 816s |-(c1 _UNBOUND_REL_6) 816s 816s 816s |-_UNBOUND_REL_1 816s 816s 816s |-_UNBOUND_REL_2 816s 816s 816s |-_UNBOUND_REL_3 816s 816s 816s |-_UNBOUND_REL_4 816s 816s 816s |-_UNBOUND_REL_5 816s 816s 816s |-_UNBOUND_REL_6 816s 816s 816s |-_UNBOUND_REL_7 816s 816s 816s |-_UNBOUND_REL_8 816s 816s 816s |-_UNBOUND_REL_9 816s 816s 816s |-_UNBOUND_REL_10 816s 816s 816s |-_UNBOUND_REL_11 816s 816s 816s |-_UNBOUND_REL_12 816s 816s 816s |-_UNBOUND_REL_13 816s 816s 816s |-I1 816s 816s 816s |-I1 816s ---> after substitution: 816s 816s 816s |-(_UNBOUND_REL_13 _UNBOUND_REL_6 _UNBOUND_REL_5 _UNBOUND_REL_4 816s (c1 _UNBOUND_REL_6) (c1 _UNBOUND_REL_5)) 816s translate_mind, evd = 816s SHELF: 816s FUTURE GOALS STACK: 816s 816s ---> env_params: 816s acc = 816s def = 816s 816s |-n1 816s typ = 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s def = 816s p₁ := n1 : nat 816s 816s |-n1 816s typ = 816s p₁ := n1 : nat 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s 816s |-n1_R 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s 816s |-(nat_R p₁ p₂) 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-n2 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s 816s |-n2 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s 816s |-n2_R 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s 816s |-(nat_R q₁ q₂) 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s 816s |-(nat_R n₁ n₂) 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-n₁ 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s 816s |-n₂ 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s 816s |-nat 816s acc = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s def = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s 816s |-n_R 816s typ = 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s 816s |-(nat_R r₁ r₂) 816s ---> arities: 816s {mind_entry_record : None 816s mind_entry_finite : Finite 816s 816s mind_entry_params : 816s p₁ := n1 : nat 816s p₂ := n1 : nat 816s p_R := n1_R : nat_R p₁ p₂ 816s q₁ := n2 : nat 816s q₂ := n2 : nat 816s q_R := n2_R : nat_R q₁ q₂ 816s n₁ : nat 816s n₂ : nat 816s n_R : nat_R n₁ n₂ 816s r₁ := n₁ : nat 816s r₂ := n₂ : nat 816s r_R := n_R : nat_R r₁ r₂ 816s 816s mind_entry_inds : { 816s mind_entry_lc : (I1_R n₁ n₂ 816s n_R (c1 n₁) (c1 n₂)) 816s 816s mind_entry_consnames : I1_R_c1_R 816s 816s mind_entry_arity : (I1 n₁ -> 816s I1 n₂ -> Prop) 816s mind_entry_typename : I1_R 816s } 816s 816s mind_entry_polymorphic : false 816s mind_entry_universes : 816s 816s mind_entry_cumulative : false 816s mind_entry_private : None 816s } 816s Prop 816s 816s ---> Translating mind body ... done. 816s evar_map inductive SHELF: 816s FUTURE GOALS STACK: 816s 818s File "./bug3.v", line 20, characters 41-47: 818s Warning: Notation divmod is deprecated since 8.16. 818s The NPeano file is obsolete. Use Nat.divmod instead. 818s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] 819s BinPosDef.Pos.sub_mask = 819s fix sub_mask (x y : positive) {struct y} : BinPosDef.Pos.mask := 819s match x with 819s | (p~1)%positive => 819s match y with 819s | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 819s | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask p q) 819s | 1%positive => BinPosDef.Pos.IsPos p~0 819s end 819s | (p~0)%positive => 819s match y with 819s | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 819s | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 819s | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p) 819s end 819s | 1%positive => 819s match y with 819s | 1%positive => BinPosDef.Pos.IsNul 819s | _ => BinPosDef.Pos.IsNeg 819s end 819s end 819s with sub_mask_carry (x y : positive) {struct y} : BinPosDef.Pos.mask := 819s match x with 819s | (p~1)%positive => 819s match y with 819s | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 819s | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 819s | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p) 819s end 819s | (p~0)%positive => 819s match y with 819s | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask_carry p q) 819s | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 819s | 1%positive => BinPosDef.Pos.double_pred_mask p 819s end 819s | 1%positive => BinPosDef.Pos.IsNeg 819s end 819s for 819s sub_mask 819s : positive -> positive -> BinPosDef.Pos.mask 819s 819s Arguments BinPosDef.Pos.sub_mask (x y)%positive_scope 820s File "./bug5.v", line 24, characters 41-47: 820s Warning: Notation divmod is deprecated since 8.16. 820s The NPeano file is obsolete. Use Nat.divmod instead. 820s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] 820s T_R = 820s fun H H0 : forall a b : nat, b <> 0 -> modS a b < b => 820s forall (a₁ a₂ : nat) (a_R : nat_R a₁ a₂) (b₁ b₂ : nat) 820s (b_R : nat_R b₁ b₂) (H1 : b₁ <> 0) (H2 : b₂ <> 0), 820s not_R (eq_R nat_R b_R nat_R_O_R) H1 H2 -> 820s lt_R (modS_R a_R b_R) b_R (H a₁ b₁ H1) (H0 a₂ b₂ H2) 820s : T -> T -> Prop 820s 'NNmod_upper_boundA_RR' is now a registered translation. 834s File "./dummyFix.v", line 6, characters 0-59: 834s Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] 834s Inductive bool_P : bool -> Set := 834s bool_P_true_P : bool_P true | bool_P_false_P : bool_P false. 834s boolfun_P = 834s fun H : bool -> bool => forall H0 : bool, bool_P H0 -> bool_P (H H0) 834s : boolfun -> Set 834s myneg_P = 834s fun (b : bool) (b_P : bool_P b) => 834s match 834s b_P in (bool_P b0) 834s return (bool_P match b0 with 834s | true => false 834s | false => true 834s end) 834s with 834s | bool_P_true_P => bool_P_false_P 834s | bool_P_false_P => bool_P_true_P 834s end 834s : forall b : bool, bool_P b -> bool_P (myneg b) 834s 834s Arguments myneg_P b b_P 834s boolfun_R = 834s fun H H0 : bool -> bool => 834s forall H1 H2 : bool, bool_R H1 H2 -> bool_R (H H1) (H0 H2) 834s : boolfun -> boolfun -> Set 834s File "./example.v", line 64, characters 5-9: 834s Warning: Unused variable fale might be a misspelled constructor. Use _ or 834s _fale to silence this warning. [unused-pattern-matching-variable,default] 834s negb_R 834s : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂) 834s negb_R = 834s fun (x₁ x₂ : bool) (x_R : bool_R x₁ x₂) => 834s match 834s x_R in (bool_R x₁0 x₂0) 834s return 834s (bool_R match x₁0 with 834s | true => false 834s | false => true 834s end match x₂0 with 834s | true => false 834s | false => true 834s end) 834s with 834s | bool_R_true_R => bool_R_false_R 834s | bool_R_false_R => bool_R_true_R 834s end 834s : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂) 834s 834s Arguments negb_R x₁ x₂ x_R 834s Type_R = fun H H0 : Type => H -> H0 -> Type 834s : Type -> Type -> Type 834s 834s Arguments Type_R (_ _)%type_scope 834s bool_R : Type_R bool bool 834s : Type_R bool bool 834s boolfun_R : Type_R boolfun boolfun 834s : Type_R boolfun boolfun 834s pType_R : pType_R pType pType 834s : pType_R pType pType 834s arrow_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 834s (B_R : B₁ -> B₂ -> Type) (H : A₁ -> B₁) (H0 : A₂ -> B₂) => 834s forall (H1 : A₁) (H2 : A₂), A_R H1 H2 -> B_R (H H1) (H0 H2) 834s : forall A₁ A₂ : Type, 834s (A₁ -> A₂ -> Type) -> 834s forall B₁ B₂ : Type, 834s (B₁ -> B₂ -> Type) -> arrow A₁ B₁ -> arrow A₂ B₂ -> Type 834s 834s Arguments arrow_R (A₁ A₂)%type_scope A_R%function_scope 834s (B₁ B₂)%type_scope B_R%function_scope _ _ 834s lambda_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 834s (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 834s (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 834s (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) 834s (f₂ : arrow A₂ B₂), 834s arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ -> 834s forall (x₁ : A₁) (x₂ : A₂), 834s A_R x₁ x₂ -> B_R (lambda A₁ B₁ f₁ x₁) (lambda A₂ B₂ f₂ x₂) 834s 834s Arguments lambda_R (A₁ A₂)%type_scope A_R%function_scope 834s (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 834s x₁ x₂ x_R 834s application_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 834s (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 834s (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 834s (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) 834s (f₂ : arrow A₂ B₂), 834s arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ -> 834s forall (x₁ : A₁) (x₂ : A₂), 834s A_R x₁ x₂ -> B_R (application A₁ B₁ f₁ x₁) (application A₂ B₂ f₂ x₂) 834s 834s Arguments application_R (A₁ A₂)%type_scope A_R%function_scope 834s (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 834s x₁ x₂ x_R 834s for_all_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ : A₁ -> Type) 834s (B₂ : A₂ -> Type) 834s (B_R : forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type) 834s (H : forall x : A₁, B₁ x) (H0 : forall x : A₂, B₂ x) => 834s forall (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂), B_R x₁ x₂ x_R (H x₁) (H0 x₂) 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (B₁ : A₁ -> Type) (B₂ : A₂ -> Type), 834s (forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type) -> 834s for_all A₁ B₁ -> for_all A₂ B₂ -> Type 834s 834s Arguments for_all_R (A₁ A₂)%type_scope (A_R B₁ B₂ B_R)%function_scope _ _ 834s Inductive nat_R : nat -> nat -> Set := 834s nat_R_O_R : nat_R O O 834s | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0). 834s Inductive 834s list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s : list A₁ -> list A₂ -> Type := 834s list_R_nil_R : list_R A₁ A₂ A_R (nil A₁) (nil A₂) 834s | list_R_cons_R : forall (H : A₁) (H0 : A₂), 834s A_R H H0 -> 834s forall (H1 : list A₁) (H2 : list A₂), 834s list_R A₁ A₂ A_R H1 H2 -> 834s list_R A₁ A₂ A_R (cons A₁ H H1) (cons A₂ H0 H2). 834s 834s Arguments list_R (A₁ A₂)%type_scope A_R%function_scope _ _ 834s Arguments list_R_nil_R (A₁ A₂)%type_scope A_R%function_scope 834s Arguments list_R_cons_R (A₁ A₂)%type_scope A_R%function_scope _ _ _ _ _ _ 834s length_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂) 834s length_R = 834s let fix_length_1 := 834s fix length (A : Type) (l : list A) {struct l} : nat := 834s match l with 834s | nil _ => O 834s | cons _ _ tl => S (length A tl) 834s end in 834s let fix_length_2 := 834s fix length (A : Type) (l : list A) {struct l} : nat := 834s match l with 834s | nil _ => O 834s | cons _ _ tl => S (length A tl) 834s end in 834s fix length_R 834s (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 834s (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) {struct l_R} : 834s nat_R (fix_length_1 A₁ l₁) (fix_length_2 A₂ l₂) := 834s match 834s l_R in (list_R _ _ _ l₁0 l₂0) 834s return (nat_R (fix_length_1 A₁ l₁0) (fix_length_2 A₂ l₂0)) 834s with 834s | list_R_nil_R _ _ _ => nat_R_O_R 834s | list_R_cons_R _ _ _ _ _ _ tl₁ tl₂ tl_R => 834s nat_R_S_R (fix_length_1 A₁ tl₁) (fix_length_2 A₂ tl₂) 834s (length_R A₁ A₂ A_R tl₁ tl₂ tl_R) 834s end 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂) 834s 834s Arguments length_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R 834s list_rec_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (P₁ : list A₁ -> Set) 834s (P₂ : list A₂ -> Set) 834s (P_R : forall (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set) => 834s (fun (A₁0 A₂0 : Type) (A_R0 : A₁0 -> A₂0 -> Type) 834s (P₁0 : list A₁0 -> Type) (P₂0 : list A₂0 -> Type) 834s (P_R0 : forall (l₁ : list A₁0) (l₂ : list A₂0), 834s list_R A₁0 A₂0 A_R0 l₁ l₂ -> P₁0 l₁ -> P₂0 l₂ -> Type) 834s (f₁ : P₁0 (nil A₁0)) (f₂ : P₂0 (nil A₂0)) 834s (f_R : P_R0 (nil A₁0) (nil A₂0) (list_R_nil_R A₁0 A₂0 A_R0) f₁ f₂) 834s (f0₁ : forall (a : A₁0) (l : list A₁0), P₁0 l -> P₁0 (cons A₁0 a l)) 834s (f0₂ : forall (a : A₂0) (l : list A₂0), P₂0 l -> P₂0 (cons A₂0 a l)) 834s (f0_R : forall (a₁ : A₁0) (a₂ : A₂0) (a_R : A_R0 a₁ a₂) 834s (l₁ : list A₁0) (l₂ : list A₂0) 834s (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) (H : P₁0 l₁) 834s (H0 : P₂0 l₂), 834s P_R0 l₁ l₂ l_R H H0 -> 834s P_R0 (cons A₁0 a₁ l₁) (cons A₂0 a₂ l₂) 834s (list_R_cons_R A₁0 A₂0 A_R0 a₁ a₂ a_R l₁ l₂ l_R) 834s (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) => 834s let fix_F_1 := 834s fix F (l : list A₁0) : P₁0 l := 834s match l as l0 return (P₁0 l0) with 834s | nil _ => f₁ 834s | cons _ y l0 => f0₁ y l0 (F l0) 834s end in 834s let fix_F_2 := 834s fix F (l : list A₂0) : P₂0 l := 834s match l as l0 return (P₂0 l0) with 834s | nil _ => f₂ 834s | cons _ y l0 => f0₂ y l0 (F l0) 834s end in 834s fix F_R 834s (l₁ : list A₁0) (l₂ : list A₂0) (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) {struct 834s l_R} : P_R0 l₁ l₂ l_R (fix_F_1 l₁) (fix_F_2 l₂) := 834s match 834s l_R as l_R0 in (list_R _ _ _ l₁0 l₂0) 834s return (P_R0 l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0)) 834s with 834s | list_R_nil_R _ _ _ => f_R 834s | list_R_cons_R _ _ _ y₁ y₂ y_R l₁0 l₂0 l_R0 => 834s f0_R y₁ y₂ y_R l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0) 834s (F_R l₁0 l₂0 l_R0) 834s end) A₁ A₂ A_R P₁ P₂ P_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (P₁ : list A₁ -> Set) (P₂ : list A₂ -> Set) 834s (P_R : forall (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set) 834s (f₁ : P₁ (nil A₁)) (f₂ : P₂ (nil A₂)), 834s P_R (nil A₁) (nil A₂) (list_R_nil_R A₁ A₂ A_R) f₁ f₂ -> 834s forall (f0₁ : forall (a : A₁) (l : list A₁), P₁ l -> P₁ (cons A₁ a l)) 834s (f0₂ : forall (a : A₂) (l : list A₂), P₂ l -> P₂ (cons A₂ a l)), 834s (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂) 834s (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) 834s (H : P₁ l₁) (H0 : P₂ l₂), 834s P_R l₁ l₂ l_R H H0 -> 834s P_R (cons A₁ a₁ l₁) (cons A₂ a₂ l₂) 834s (list_R_cons_R A₁ A₂ A_R a₁ a₂ a_R l₁ l₂ l_R) 834s (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) -> 834s forall (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂), 834s P_R l₁ l₂ l_R (list_rec A₁ P₁ f₁ f0₁ l₁) (list_rec A₂ P₂ f₂ f0₂ l₂) 834s 834s Arguments list_rec_R (A₁ A₂)%type_scope (A_R P₁ P₂ P_R)%function_scope 834s f₁ f₂ f_R (f0₁ f0₂ f0_R)%function_scope l₁ l₂ l_R 834s length2_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂) 834s length2_R = 834s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 834s (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) => 834s list_rec_R A₁ A₂ A_R (fun _ : list A₁ => nat) (fun _ : list A₂ => nat) 834s (fun (l₁0 : list A₁) (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) => 834s nat_R) O O nat_R_O_R (fun (_ : A₁) (_ : list A₁) => S) 834s (fun (_ : A₂) (_ : list A₂) => S) 834s (fun (a₁ : A₁) (a₂ : A₂) (_ : A_R a₁ a₂) (l₁0 : list A₁) 834s (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) => nat_R_S_R) l₁ l₂ l_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (l₁ : list A₁) (l₂ : list A₂), 834s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂) 834s 834s Arguments length2_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R 834s sum_rect = 834s fun (A B : Type) (P : A + B -> Type) (f : forall a : A, P (inl a)) 834s (f0 : forall b : B, P (inr b)) (s : A + B) => 834s match s as s0 return (P s0) with 834s | inl a => f a 834s | inr b => f0 b 834s end 834s : forall (A B : Type) (P : A + B -> Type), 834s (forall a : A, P (inl a)) -> 834s (forall b : B, P (inr b)) -> forall s : A + B, P s 834s 834s Arguments sum_rect [A B]%type_scope (P f f0)%function_scope s 834s sum_rect 834s : forall (A B : Type) (P : A + B -> Type), 834s (forall a : A, P (inl a)) -> 834s (forall b : B, P (inr b)) -> forall s : A + B, P s 834s sum_rect_R 834s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 834s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (P₁ : A₁ + B₁ -> Type) 834s (P₂ : A₂ + B₂ -> Type) 834s (P_R : forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂), 834s sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂ -> P₁ s₁ -> P₂ s₂ -> Type) 834s (f₁ : forall a : A₁, P₁ (inl a)) (f₂ : forall a : A₂, P₂ (inl a)), 834s (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂), 834s P_R (inl a₁) (inl a₂) (sum_R_inl_R A₁ A₂ A_R B₁ B₂ B_R a₁ a₂ a_R) 834s (f₁ a₁) (f₂ a₂)) -> 834s forall (f0₁ : forall b : B₁, P₁ (inr b)) 834s (f0₂ : forall b : B₂, P₂ (inr b)), 834s (forall (b₁ : B₁) (b₂ : B₂) (b_R : B_R b₁ b₂), 834s P_R (inr b₁) (inr b₂) (sum_R_inr_R A₁ A₂ A_R B₁ B₂ B_R b₁ b₂ b_R) 834s (f0₁ b₁) (f0₂ b₂)) -> 834s forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂) 834s (s_R : sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂), 834s P_R s₁ s₂ s_R (sum_rect P₁ f₁ f0₁ s₁) (sum_rect P₂ f₂ f0₂ s₂) 836s rev_R 836s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 836s (l₁ : list A₁) (l₂ : list A₂), 836s list_R A₁ A₂ A_R l₁ l₂ -> list_R A₁ A₂ A_R (List.rev l₁) (List.rev l₂) 836s Module A_R := Struct Definition t_R : A.t -> A.t -> Set. Module B_R End 836s 836s Module A_R.B_R := Struct Definition t_R : A.B.t -> A.B.t -> Set. End 836s 836s Inductive 836s nat_R_10 836s : nat -> 836s nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Set := 836s nat_R_10_O_R_10 : nat_R_10 0 0 0 0 0 0 0 0 0 0 836s | nat_R_10_S_R_10 : forall H H0 H1 H2 H3 H4 H5 H6 H7 H8 : nat, 836s nat_R_10 H H0 H1 H2 H3 H4 H5 H6 H7 H8 -> 836s nat_R_10 (S H) (S H0) (S H1) 836s (S H2) (S H3) (S H4) (S H5) 836s (S H6) (S H7) (S H8). 836s 836s Arguments nat_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope 836s Arguments nat_R_10_S_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope _ 836s 'A_R' is now a registered translation. 836s = opaque 836s : True 836s = opaque_R 836s : True_R opaque opaque 838s autopkgtest [12:54:56]: test upstreamtestsuite: -----------------------] 839s upstreamtestsuite PASS 839s autopkgtest [12:54:57]: test upstreamtestsuite: - - - - - - - - - - results - - - - - - - - - - 839s autopkgtest [12:54:57]: @@@@@@@@@@@@@@@@@@@@ summary 839s upstreamtestsuite PASS 858s Creating nova instance adt-noble-arm64-paramcoq-20240326-124056-juju-7f2275-prod-proposed-migration-environment-2-7ea73e17-6962-4462-b1e4-6b4ed982bb27 from image adt/ubuntu-noble-arm64-server-20240326.img (UUID 0221ee4c-7186-4bac-9e7d-f1a20b702f58)...