0s autopkgtest [00:15:13]: starting date and time: 2024-03-26 00:15:13+0000 0s autopkgtest [00:15:13]: git checkout: 4a1cd702 l/adt_testbed: don't blame the testbed for unsolvable build deps 0s autopkgtest [00:15:13]: host juju-7f2275-prod-proposed-migration-environment-3; command line: /home/ubuntu/autopkgtest/runner/autopkgtest --output-dir /tmp/autopkgtest-work.4i6ooly7/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=paramcoq/1.1.3+coq8.18-1build1 coq/8.18.0+dfsg-1build1' -- ssh -s /home/ubuntu/autopkgtest/ssh-setup/nova -- --flavor autopkgtest --security-groups autopkgtest-juju-7f2275-prod-proposed-migration-environment-3@bos02-ppc64el-13.secgroup --name adt-noble-ppc64el-paramcoq-20240326-001513-juju-7f2275-prod-proposed-migration-environment-3 --image adt/ubuntu-noble-ppc64el-server --keyname testbed-juju-7f2275-prod-proposed-migration-environment-3 --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/ 152s autopkgtest [00:17:45]: testbed dpkg architecture: ppc64el 152s autopkgtest [00:17:45]: testbed apt version: 2.7.12 152s autopkgtest [00:17:45]: @@@@@@@@@@@@@@@@@@@@ test bed setup 153s Get:1 http://ftpmaster.internal/ubuntu noble-proposed InRelease [117 kB] 153s Get:2 http://ftpmaster.internal/ubuntu noble-proposed/restricted Sources [7592 B] 153s Get:3 http://ftpmaster.internal/ubuntu noble-proposed/universe Sources [3976 kB] 155s Get:4 http://ftpmaster.internal/ubuntu noble-proposed/multiverse Sources [56.0 kB] 155s Get:5 http://ftpmaster.internal/ubuntu noble-proposed/main Sources [497 kB] 155s Get:6 http://ftpmaster.internal/ubuntu noble-proposed/main ppc64el Packages [700 kB] 155s Get:7 http://ftpmaster.internal/ubuntu noble-proposed/main ppc64el c-n-f Metadata [3116 B] 155s Get:8 http://ftpmaster.internal/ubuntu noble-proposed/restricted ppc64el Packages [1372 B] 155s Get:9 http://ftpmaster.internal/ubuntu noble-proposed/restricted ppc64el c-n-f Metadata [116 B] 155s Get:10 http://ftpmaster.internal/ubuntu noble-proposed/universe ppc64el Packages [4227 kB] 156s Get:11 http://ftpmaster.internal/ubuntu noble-proposed/universe ppc64el c-n-f Metadata [8652 B] 156s Get:12 http://ftpmaster.internal/ubuntu noble-proposed/multiverse ppc64el Packages [61.7 kB] 156s Get:13 http://ftpmaster.internal/ubuntu noble-proposed/multiverse ppc64el c-n-f Metadata [116 B] 159s Fetched 9655 kB in 4s (2551 kB/s) 159s Reading package lists... 161s Reading package lists... 161s Building dependency tree... 161s Reading state information... 162s Calculating upgrade... 162s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 162s Reading package lists... 162s Building dependency tree... 162s Reading state information... 162s 0 upgraded, 0 newly installed, 0 to remove and 246 not upgraded. 163s sh: Attempting to set up Debian/Ubuntu apt sources automatically 163s sh: Distribution appears to be Ubuntu 165s Reading package lists... 165s Building dependency tree... 165s Reading state information... 165s eatmydata is already the newest version (131-1). 165s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 165s Reading package lists... 166s Building dependency tree... 166s Reading state information... 166s dbus is already the newest version (1.14.10-4ubuntu1). 166s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 166s Reading package lists... 166s Building dependency tree... 166s Reading state information... 166s rng-tools-debian is already the newest version (2.4). 166s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 166s Reading package lists... 166s Building dependency tree... 166s Reading state information... 167s The following packages will be REMOVED: 167s cloud-init* python3-configobj* python3-debconf* 167s 0 upgraded, 0 newly installed, 3 to remove and 0 not upgraded. 167s After this operation, 3256 kB disk space will be freed. 167s (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 ... 70156 files and directories currently installed.) 167s Removing cloud-init (24.1.2-0ubuntu1) ... 167s Removing python3-configobj (5.0.8-3) ... 168s Removing python3-debconf (1.5.86) ... 168s Processing triggers for man-db (2.12.0-3) ... 168s (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 ... 69767 files and directories currently installed.) 168s Purging configuration files for cloud-init (24.1.2-0ubuntu1) ... 169s dpkg: warning: while removing cloud-init, directory '/etc/cloud/cloud.cfg.d' not empty so not removed 169s Processing triggers for rsyslog (8.2312.0-3ubuntu3) ... 169s invoke-rc.d: policy-rc.d denied execution of try-restart. 169s Reading package lists... 169s Building dependency tree... 169s Reading state information... 169s linux-generic is already the newest version (6.8.0-11.11+1). 169s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 170s Hit:1 http://ftpmaster.internal/ubuntu noble InRelease 170s Hit:2 http://ftpmaster.internal/ubuntu noble-updates InRelease 170s Hit:3 http://ftpmaster.internal/ubuntu noble-security InRelease 173s Reading package lists... 173s Reading package lists... 173s Building dependency tree... 173s Reading state information... 173s Calculating upgrade... 173s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 173s Reading package lists... 173s Building dependency tree... 173s Reading state information... 174s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. 174s autopkgtest [00:18:07]: rebooting testbed after setup commands that affected boot 345s autopkgtest [00:20:58]: testbed running kernel: Linux 6.8.0-11-generic #11-Ubuntu SMP Wed Feb 14 00:33:03 UTC 2024 348s autopkgtest [00:21:01]: @@@@@@@@@@@@@@@@@@@@ apt-source paramcoq 350s Get:1 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (dsc) [2111 B] 350s Get:2 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (tar) [45.8 kB] 350s Get:3 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (diff) [3092 B] 350s gpgv: Signature made Thu Dec 21 15:33:52 2023 UTC 350s gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 350s gpgv: issuer "jpuydt@debian.org" 350s gpgv: Can't check signature: No public key 350s dpkg-source: warning: cannot verify inline signature for ./paramcoq_1.1.3+coq8.18-1.dsc: no acceptable signature found 350s autopkgtest [00:21:03]: testing package paramcoq version 1.1.3+coq8.18-1 350s autopkgtest [00:21:03]: build not needed 350s autopkgtest [00:21:03]: test upstreamtestsuite: preparing testbed 353s Reading package lists... 353s Building dependency tree... 353s Reading state information... 353s Starting pkgProblemResolver with broken count: 0 353s Starting 2 pkgProblemResolver with broken count: 0 353s Done 354s The following additional packages will be installed: 354s coq cpp cpp-13 cpp-13-powerpc64le-linux-gnu cpp-powerpc64le-linux-gnu gcc 354s gcc-13 gcc-13-powerpc64le-linux-gnu gcc-powerpc64le-linux-gnu libasan8 354s libatomic1 libc-dev-bin libc6-dev libcc1-0 libcompiler-libs-ocaml-dev 354s libcoq-core-ocaml libcoq-paramcoq libcoq-stdlib libcrypt-dev 354s libfindlib-ocaml libgcc-13-dev libgomp1 libisl23 libitm1 liblsan0 libmpc3 354s libncurses-dev libquadmath0 libstdlib-ocaml libstdlib-ocaml-dev libtsan2 354s libubsan1 libzarith-ocaml linux-libc-dev ocaml ocaml-base ocaml-findlib 354s ocaml-interp rpcsvc-proto 354s Suggested packages: 354s coqide | proofgeneral ledit | readline-editor libcoq-core-ocaml-dev why 354s coq-doc cpp-doc gcc-13-locales cpp-13-doc gcc-multilib manpages-dev autoconf 354s automake libtool flex bison gdb gcc-doc gcc-13-doc gdb-powerpc64le-linux-gnu 354s glibc-doc ncurses-doc ocaml-doc elpa-tuareg camlp4 354s Recommended packages: 354s manpages manpages-dev libc-devtools ocaml-man libfindlib-ocaml-dev ledit 354s | readline-editor 354s The following NEW packages will be installed: 354s autopkgtest-satdep coq cpp cpp-13 cpp-13-powerpc64le-linux-gnu 354s cpp-powerpc64le-linux-gnu gcc gcc-13 gcc-13-powerpc64le-linux-gnu 354s gcc-powerpc64le-linux-gnu libasan8 libatomic1 libc-dev-bin libc6-dev 354s libcc1-0 libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-paramcoq 354s libcoq-stdlib libcrypt-dev libfindlib-ocaml libgcc-13-dev libgomp1 libisl23 354s libitm1 liblsan0 libmpc3 libncurses-dev libquadmath0 libstdlib-ocaml 354s libstdlib-ocaml-dev libtsan2 libubsan1 libzarith-ocaml linux-libc-dev ocaml 354s ocaml-base ocaml-findlib ocaml-interp rpcsvc-proto 354s 0 upgraded, 40 newly installed, 0 to remove and 0 not upgraded. 354s Need to get 379 MB/379 MB of archives. 354s After this operation, 1231 MB of additional disk space will be used. 354s Get:1 /tmp/autopkgtest.zRvCyS/1-autopkgtest-satdep.deb autopkgtest-satdep ppc64el 0 [716 B] 354s Get:2 http://ftpmaster.internal/ubuntu noble/universe ppc64el libcoq-stdlib ppc64el 8.18.0+dfsg-1 [35.2 MB] 355s Get:3 http://ftpmaster.internal/ubuntu noble/universe ppc64el libstdlib-ocaml ppc64el 4.14.1-1ubuntu1 [416 kB] 355s Get:4 http://ftpmaster.internal/ubuntu noble/universe ppc64el ocaml-base ppc64el 4.14.1-1ubuntu1 [315 kB] 356s Get:5 http://ftpmaster.internal/ubuntu noble/universe ppc64el libfindlib-ocaml ppc64el 1.9.6-1build3 [201 kB] 356s Get:6 http://ftpmaster.internal/ubuntu noble/universe ppc64el libzarith-ocaml ppc64el 1.13-2build3 [131 kB] 356s Get:7 http://ftpmaster.internal/ubuntu noble/universe ppc64el libcoq-core-ocaml ppc64el 8.18.0+dfsg-1 [34.5 MB] 356s Get:8 http://ftpmaster.internal/ubuntu noble/universe ppc64el libstdlib-ocaml-dev ppc64el 4.14.1-1ubuntu1 [8533 kB] 357s Get:9 http://ftpmaster.internal/ubuntu noble/universe ppc64el libcompiler-libs-ocaml-dev ppc64el 4.14.1-1ubuntu1 [38.4 MB] 358s Get:10 http://ftpmaster.internal/ubuntu noble/universe ppc64el ocaml-interp ppc64el 4.14.1-1ubuntu1 [7826 kB] 358s Get:11 http://ftpmaster.internal/ubuntu noble/main ppc64el libc-dev-bin ppc64el 2.39-0ubuntu6 [21.3 kB] 358s Get:12 http://ftpmaster.internal/ubuntu noble/main ppc64el linux-libc-dev ppc64el 6.8.0-11.11 [1585 kB] 358s Get:13 http://ftpmaster.internal/ubuntu noble/main ppc64el libcrypt-dev ppc64el 1:4.4.36-4 [167 kB] 358s Get:14 http://ftpmaster.internal/ubuntu noble/main ppc64el rpcsvc-proto ppc64el 1.4.2-0ubuntu6 [82.3 kB] 358s Get:15 http://ftpmaster.internal/ubuntu noble/main ppc64el libc6-dev ppc64el 2.39-0ubuntu6 [2102 kB] 358s Get:16 http://ftpmaster.internal/ubuntu noble/main ppc64el libncurses-dev ppc64el 6.4+20240113-1ubuntu1 [485 kB] 358s Get:17 http://ftpmaster.internal/ubuntu noble/main ppc64el libisl23 ppc64el 0.26-3 [864 kB] 358s Get:18 http://ftpmaster.internal/ubuntu noble/main ppc64el libmpc3 ppc64el 1.3.1-1 [61.2 kB] 358s Get:19 http://ftpmaster.internal/ubuntu noble/main ppc64el cpp-13-powerpc64le-linux-gnu ppc64el 13.2.0-17ubuntu2 [10.7 MB] 358s Get:20 http://ftpmaster.internal/ubuntu noble/main ppc64el cpp-13 ppc64el 13.2.0-17ubuntu2 [1038 B] 358s Get:21 http://ftpmaster.internal/ubuntu noble/main ppc64el cpp-powerpc64le-linux-gnu ppc64el 4:13.2.0-7ubuntu1 [5330 B] 358s Get:22 http://ftpmaster.internal/ubuntu noble/main ppc64el cpp ppc64el 4:13.2.0-7ubuntu1 [22.5 kB] 358s Get:23 http://ftpmaster.internal/ubuntu noble/main ppc64el libcc1-0 ppc64el 14-20240303-1ubuntu1 [48.1 kB] 358s Get:24 http://ftpmaster.internal/ubuntu noble/main ppc64el libgomp1 ppc64el 14-20240303-1ubuntu1 [161 kB] 358s Get:25 http://ftpmaster.internal/ubuntu noble/main ppc64el libitm1 ppc64el 14-20240303-1ubuntu1 [32.4 kB] 358s Get:26 http://ftpmaster.internal/ubuntu noble/main ppc64el libatomic1 ppc64el 14-20240303-1ubuntu1 [10.7 kB] 358s Get:27 http://ftpmaster.internal/ubuntu noble/main ppc64el libasan8 ppc64el 14-20240303-1ubuntu1 [2973 kB] 358s Get:28 http://ftpmaster.internal/ubuntu noble/main ppc64el liblsan0 ppc64el 14-20240303-1ubuntu1 [1325 kB] 358s Get:29 http://ftpmaster.internal/ubuntu noble/main ppc64el libtsan2 ppc64el 14-20240303-1ubuntu1 [2734 kB] 359s Get:30 http://ftpmaster.internal/ubuntu noble/main ppc64el libubsan1 ppc64el 14-20240303-1ubuntu1 [1194 kB] 359s Get:31 http://ftpmaster.internal/ubuntu noble/main ppc64el libquadmath0 ppc64el 14-20240303-1ubuntu1 [158 kB] 359s Get:32 http://ftpmaster.internal/ubuntu noble/main ppc64el libgcc-13-dev ppc64el 13.2.0-17ubuntu2 [1581 kB] 359s Get:33 http://ftpmaster.internal/ubuntu noble/main ppc64el gcc-13-powerpc64le-linux-gnu ppc64el 13.2.0-17ubuntu2 [20.6 MB] 359s Get:34 http://ftpmaster.internal/ubuntu noble/main ppc64el gcc-13 ppc64el 13.2.0-17ubuntu2 [477 kB] 359s Get:35 http://ftpmaster.internal/ubuntu noble/main ppc64el gcc-powerpc64le-linux-gnu ppc64el 4:13.2.0-7ubuntu1 [1224 B] 359s Get:36 http://ftpmaster.internal/ubuntu noble/main ppc64el gcc ppc64el 4:13.2.0-7ubuntu1 [5022 B] 359s Get:37 http://ftpmaster.internal/ubuntu noble/universe ppc64el ocaml ppc64el 4.14.1-1ubuntu1 [82.9 MB] 361s Get:38 http://ftpmaster.internal/ubuntu noble/universe ppc64el ocaml-findlib ppc64el 1.9.6-1build3 [616 kB] 361s Get:39 http://ftpmaster.internal/ubuntu noble/universe ppc64el coq ppc64el 8.18.0+dfsg-1 [122 MB] 364s Get:40 http://ftpmaster.internal/ubuntu noble/universe ppc64el libcoq-paramcoq ppc64el 1.1.3+coq8.18-1 [157 kB] 365s Fetched 379 MB in 11s (35.6 MB/s) 365s Selecting previously unselected package libcoq-stdlib. 365s (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 ... 69712 files and directories currently installed.) 365s Preparing to unpack .../00-libcoq-stdlib_8.18.0+dfsg-1_ppc64el.deb ... 365s Unpacking libcoq-stdlib (8.18.0+dfsg-1) ... 366s Selecting previously unselected package libstdlib-ocaml. 366s Preparing to unpack .../01-libstdlib-ocaml_4.14.1-1ubuntu1_ppc64el.deb ... 366s Unpacking libstdlib-ocaml (4.14.1-1ubuntu1) ... 366s Selecting previously unselected package ocaml-base. 366s Preparing to unpack .../02-ocaml-base_4.14.1-1ubuntu1_ppc64el.deb ... 366s Unpacking ocaml-base (4.14.1-1ubuntu1) ... 366s Selecting previously unselected package libfindlib-ocaml. 366s Preparing to unpack .../03-libfindlib-ocaml_1.9.6-1build3_ppc64el.deb ... 366s Unpacking libfindlib-ocaml (1.9.6-1build3) ... 366s Selecting previously unselected package libzarith-ocaml. 366s Preparing to unpack .../04-libzarith-ocaml_1.13-2build3_ppc64el.deb ... 366s Unpacking libzarith-ocaml (1.13-2build3) ... 366s Selecting previously unselected package libcoq-core-ocaml. 366s Preparing to unpack .../05-libcoq-core-ocaml_8.18.0+dfsg-1_ppc64el.deb ... 366s Unpacking libcoq-core-ocaml (8.18.0+dfsg-1) ... 367s Selecting previously unselected package libstdlib-ocaml-dev. 367s Preparing to unpack .../06-libstdlib-ocaml-dev_4.14.1-1ubuntu1_ppc64el.deb ... 367s Unpacking libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... 367s Selecting previously unselected package libcompiler-libs-ocaml-dev. 367s Preparing to unpack .../07-libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1_ppc64el.deb ... 367s Unpacking libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... 369s Selecting previously unselected package ocaml-interp. 369s Preparing to unpack .../08-ocaml-interp_4.14.1-1ubuntu1_ppc64el.deb ... 369s Unpacking ocaml-interp (4.14.1-1ubuntu1) ... 369s Selecting previously unselected package libc-dev-bin. 369s Preparing to unpack .../09-libc-dev-bin_2.39-0ubuntu6_ppc64el.deb ... 369s Unpacking libc-dev-bin (2.39-0ubuntu6) ... 369s Selecting previously unselected package linux-libc-dev:ppc64el. 369s Preparing to unpack .../10-linux-libc-dev_6.8.0-11.11_ppc64el.deb ... 369s Unpacking linux-libc-dev:ppc64el (6.8.0-11.11) ... 369s Selecting previously unselected package libcrypt-dev:ppc64el. 369s Preparing to unpack .../11-libcrypt-dev_1%3a4.4.36-4_ppc64el.deb ... 369s Unpacking libcrypt-dev:ppc64el (1:4.4.36-4) ... 369s Selecting previously unselected package rpcsvc-proto. 369s Preparing to unpack .../12-rpcsvc-proto_1.4.2-0ubuntu6_ppc64el.deb ... 369s Unpacking rpcsvc-proto (1.4.2-0ubuntu6) ... 369s Selecting previously unselected package libc6-dev:ppc64el. 369s Preparing to unpack .../13-libc6-dev_2.39-0ubuntu6_ppc64el.deb ... 369s Unpacking libc6-dev:ppc64el (2.39-0ubuntu6) ... 369s Selecting previously unselected package libncurses-dev:ppc64el. 369s Preparing to unpack .../14-libncurses-dev_6.4+20240113-1ubuntu1_ppc64el.deb ... 369s Unpacking libncurses-dev:ppc64el (6.4+20240113-1ubuntu1) ... 369s Selecting previously unselected package libisl23:ppc64el. 369s Preparing to unpack .../15-libisl23_0.26-3_ppc64el.deb ... 369s Unpacking libisl23:ppc64el (0.26-3) ... 369s Selecting previously unselected package libmpc3:ppc64el. 369s Preparing to unpack .../16-libmpc3_1.3.1-1_ppc64el.deb ... 369s Unpacking libmpc3:ppc64el (1.3.1-1) ... 369s Selecting previously unselected package cpp-13-powerpc64le-linux-gnu. 369s Preparing to unpack .../17-cpp-13-powerpc64le-linux-gnu_13.2.0-17ubuntu2_ppc64el.deb ... 369s Unpacking cpp-13-powerpc64le-linux-gnu (13.2.0-17ubuntu2) ... 370s Selecting previously unselected package cpp-13. 370s Preparing to unpack .../18-cpp-13_13.2.0-17ubuntu2_ppc64el.deb ... 370s Unpacking cpp-13 (13.2.0-17ubuntu2) ... 370s Selecting previously unselected package cpp-powerpc64le-linux-gnu. 370s Preparing to unpack .../19-cpp-powerpc64le-linux-gnu_4%3a13.2.0-7ubuntu1_ppc64el.deb ... 370s Unpacking cpp-powerpc64le-linux-gnu (4:13.2.0-7ubuntu1) ... 370s Selecting previously unselected package cpp. 370s Preparing to unpack .../20-cpp_4%3a13.2.0-7ubuntu1_ppc64el.deb ... 370s Unpacking cpp (4:13.2.0-7ubuntu1) ... 370s Selecting previously unselected package libcc1-0:ppc64el. 370s Preparing to unpack .../21-libcc1-0_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libcc1-0:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libgomp1:ppc64el. 370s Preparing to unpack .../22-libgomp1_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libgomp1:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libitm1:ppc64el. 370s Preparing to unpack .../23-libitm1_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libitm1:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libatomic1:ppc64el. 370s Preparing to unpack .../24-libatomic1_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libatomic1:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libasan8:ppc64el. 370s Preparing to unpack .../25-libasan8_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libasan8:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package liblsan0:ppc64el. 370s Preparing to unpack .../26-liblsan0_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking liblsan0:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libtsan2:ppc64el. 370s Preparing to unpack .../27-libtsan2_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libtsan2:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libubsan1:ppc64el. 370s Preparing to unpack .../28-libubsan1_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libubsan1:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libquadmath0:ppc64el. 370s Preparing to unpack .../29-libquadmath0_14-20240303-1ubuntu1_ppc64el.deb ... 370s Unpacking libquadmath0:ppc64el (14-20240303-1ubuntu1) ... 370s Selecting previously unselected package libgcc-13-dev:ppc64el. 370s Preparing to unpack .../30-libgcc-13-dev_13.2.0-17ubuntu2_ppc64el.deb ... 370s Unpacking libgcc-13-dev:ppc64el (13.2.0-17ubuntu2) ... 370s Selecting previously unselected package gcc-13-powerpc64le-linux-gnu. 370s Preparing to unpack .../31-gcc-13-powerpc64le-linux-gnu_13.2.0-17ubuntu2_ppc64el.deb ... 370s Unpacking gcc-13-powerpc64le-linux-gnu (13.2.0-17ubuntu2) ... 371s Selecting previously unselected package gcc-13. 371s Preparing to unpack .../32-gcc-13_13.2.0-17ubuntu2_ppc64el.deb ... 371s Unpacking gcc-13 (13.2.0-17ubuntu2) ... 371s Selecting previously unselected package gcc-powerpc64le-linux-gnu. 371s Preparing to unpack .../33-gcc-powerpc64le-linux-gnu_4%3a13.2.0-7ubuntu1_ppc64el.deb ... 371s Unpacking gcc-powerpc64le-linux-gnu (4:13.2.0-7ubuntu1) ... 371s Selecting previously unselected package gcc. 371s Preparing to unpack .../34-gcc_4%3a13.2.0-7ubuntu1_ppc64el.deb ... 371s Unpacking gcc (4:13.2.0-7ubuntu1) ... 371s Selecting previously unselected package ocaml. 371s Preparing to unpack .../35-ocaml_4.14.1-1ubuntu1_ppc64el.deb ... 371s Unpacking ocaml (4.14.1-1ubuntu1) ... 373s Selecting previously unselected package ocaml-findlib. 373s Preparing to unpack .../36-ocaml-findlib_1.9.6-1build3_ppc64el.deb ... 373s Unpacking ocaml-findlib (1.9.6-1build3) ... 373s Selecting previously unselected package coq. 373s Preparing to unpack .../37-coq_8.18.0+dfsg-1_ppc64el.deb ... 373s Unpacking coq (8.18.0+dfsg-1) ... 375s Selecting previously unselected package libcoq-paramcoq. 375s Preparing to unpack .../38-libcoq-paramcoq_1.1.3+coq8.18-1_ppc64el.deb ... 375s Unpacking libcoq-paramcoq (1.1.3+coq8.18-1) ... 375s Selecting previously unselected package autopkgtest-satdep. 375s Preparing to unpack .../39-1-autopkgtest-satdep.deb ... 375s Unpacking autopkgtest-satdep (0) ... 375s Setting up linux-libc-dev:ppc64el (6.8.0-11.11) ... 375s Setting up libgomp1:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libcoq-stdlib (8.18.0+dfsg-1) ... 375s Setting up rpcsvc-proto (1.4.2-0ubuntu6) ... 375s Setting up libquadmath0:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libstdlib-ocaml (4.14.1-1ubuntu1) ... 375s Setting up libmpc3:ppc64el (1.3.1-1) ... 375s Setting up libatomic1:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up ocaml-base (4.14.1-1ubuntu1) ... 375s Setting up libubsan1:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libcrypt-dev:ppc64el (1:4.4.36-4) ... 375s Setting up libasan8:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libtsan2:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libisl23:ppc64el (0.26-3) ... 375s Setting up libc-dev-bin (2.39-0ubuntu6) ... 375s Setting up cpp-13-powerpc64le-linux-gnu (13.2.0-17ubuntu2) ... 375s Setting up libcc1-0:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up liblsan0:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up libitm1:ppc64el (14-20240303-1ubuntu1) ... 375s Setting up cpp-powerpc64le-linux-gnu (4:13.2.0-7ubuntu1) ... 375s Setting up cpp-13 (13.2.0-17ubuntu2) ... 375s Setting up libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... 375s Setting up libcoq-paramcoq (1.1.3+coq8.18-1) ... 375s Setting up libfindlib-ocaml (1.9.6-1build3) ... 375s Setting up libzarith-ocaml (1.13-2build3) ... 375s Setting up libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... 375s Setting up ocaml-interp (4.14.1-1ubuntu1) ... 375s Setting up ocaml-findlib (1.9.6-1build3) ... 375s Setting up libgcc-13-dev:ppc64el (13.2.0-17ubuntu2) ... 375s Setting up libcoq-core-ocaml (8.18.0+dfsg-1) ... 375s Setting up cpp (4:13.2.0-7ubuntu1) ... 375s Setting up libc6-dev:ppc64el (2.39-0ubuntu6) ... 375s Setting up libncurses-dev:ppc64el (6.4+20240113-1ubuntu1) ... 375s Setting up gcc-13-powerpc64le-linux-gnu (13.2.0-17ubuntu2) ... 375s Setting up gcc-13 (13.2.0-17ubuntu2) ... 375s Setting up gcc-powerpc64le-linux-gnu (4:13.2.0-7ubuntu1) ... 375s Setting up gcc (4:13.2.0-7ubuntu1) ... 375s Setting up ocaml (4.14.1-1ubuntu1) ... 375s Setting up coq (8.18.0+dfsg-1) ... 375s Setting up autopkgtest-satdep (0) ... 375s Processing triggers for man-db (2.12.0-3) ... 376s Processing triggers for libc-bin (2.39-0ubuntu6) ... 378s (Reading database ... 77495 files and directories currently installed.) 378s Removing autopkgtest-satdep (0) ... 379s autopkgtest [00:21:32]: test upstreamtestsuite: [----------------------- 395s Inductive nat_R : nat -> nat -> Set := 395s nat_R_O_R : nat_R 0 0 395s | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0). 395s 395s Arguments nat_R (_ _)%nat_scope 395s Arguments nat_R_S_R (_ _)%nat_scope _ 395s Variant Queue_R : Queue -> Queue -> Type := 395s Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 395s (t_R : t₁ -> t₂ -> Type) 395s (empty₁ : t₁) (empty₂ : t₂), 395s t_R empty₁ empty₂ -> 395s forall (push₁ : nat -> t₁ -> t₁) 395s (push₂ : nat -> t₂ -> t₂), 395s (forall H H0 : nat, 395s nat_R H H0 -> 395s forall (H1 : t₁) (H2 : t₂), 395s t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) -> 395s forall (pop₁ : t₁ -> option (nat * t₁)) 395s (pop₂ : t₂ -> option (nat * t₂)), 395s (forall (H : t₁) (H0 : t₂), 395s t_R H H0 -> 395s option_R (nat * t₁) (nat * t₂) 395s (prod_R nat nat nat_R t₁ t₂ t_R) 395s (pop₁ H) (pop₂ H0)) -> 395s Queue_R 395s {| 395s t := t₁; 395s empty := empty₁; 395s push := push₁; 395s pop := pop₁ 395s |} 395s {| 395s t := t₂; 395s empty := empty₂; 395s push := push₂; 395s pop := pop₂ 395s |}. 395s 395s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 395s t_R%function_scope empty₁ empty₂ empty_R 395s (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope 395s Queue_R 395s : Queue -> Queue -> Type 395s Variant Queue_R : Queue -> Queue -> Type := 395s Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 395s (t_R : t₁ -> t₂ -> Type) 395s (empty₁ : t₁) (empty₂ : t₂), 395s t_R empty₁ empty₂ -> 395s forall (push₁ : nat -> t₁ -> t₁) 395s (push₂ : nat -> t₂ -> t₂), 395s (forall H H0 : nat, 395s nat_R H H0 -> 395s forall (H1 : t₁) (H2 : t₂), 395s t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) -> 395s forall (pop₁ : t₁ -> option (nat * t₁)) 395s (pop₂ : t₂ -> option (nat * t₂)), 395s (forall (H : t₁) (H0 : t₂), 395s t_R H H0 -> 395s option_R (nat * t₁) (nat * t₂) 395s (prod_R nat nat nat_R t₁ t₂ t_R) 395s (pop₁ H) (pop₂ H0)) -> 395s Bisimilar 395s {| 395s t := t₁; 395s empty := empty₁; 395s push := push₁; 395s pop := pop₁ 395s |} 395s {| 395s t := t₂; 395s empty := empty₂; 395s push := push₂; 395s pop := pop₂ 395s |}. 395s 395s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 395s t_R%function_scope empty₁ empty₂ empty_R 395s (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope 395s File "./ListQueue.v", line 127, characters 36-43: 395s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 395s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 395s File "./ListQueue.v", line 127, characters 36-43: 395s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 395s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 395s File "./ListQueue.v", line 127, characters 36-43: 395s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. 395s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] 395s program = 395s fun (Q : Queue) (n : nat) => 395s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in 395s let q0 := 395s nat_rect (fun _ : nat => option Q) (Some q) 395s (fun (_ : nat) (q0 : option Q) => 395s do q1 <- q0 395s in do x, q2 <- pop Q q1 395s in do y, q3 <- pop Q q2 in Some (push Q (x + y) q3)) n in 395s do q1 <- q0 in option_map fst (pop Q q1) 395s : Queue -> nat -> option nat 395s 395s Arguments program Q n%nat_scope 395s program 395s : Queue -> nat -> option nat 395s program_R 395s : forall Q₁ Q₂ : Queue, 395s Bisimilar Q₁ Q₂ -> 395s forall n₁ n₂ : nat, 395s nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂) 395s program = 395s fun (Q : Queue) (n : nat) => 395s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in 395s let q0 := 395s nat_rect (fun _ : nat => option Q) (Some q) 395s (fun (_ : nat) (q0 : option Q) => 395s do q1 <- q0 395s in do x, q2 <- pop Q q1 395s in do y, q3 <- pop Q q2 in Some (push Q (x + y) q3)) n in 395s do q1 <- q0 in option_map fst (pop Q q1) 395s : Queue -> nat -> option nat 395s 395s Arguments program Q n%nat_scope 395s program_R = 395s fun (Q₁ Q₂ : Queue) (Q_R : Bisimilar Q₁ Q₂) (n₁ n₂ : nat) (n_R : nat_R n₁ n₂) 395s => 395s let q₁ := nat_rect (fun _ : nat => Q₁) (empty Q₁) (push Q₁) (S n₁) in 395s let q₂ := nat_rect (fun _ : nat => Q₂) (empty Q₂) (push Q₂) (S n₂) in 395s let q_R := 395s nat_rect_R (fun _ : nat => Q₁) (fun _ : nat => Q₂) 395s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) => t_R Q₁ Q₂ Q_R) 395s (empty Q₁) (empty Q₂) (empty_R Q₁ Q₂ Q_R) (push Q₁) 395s (push Q₂) (push_R Q₁ Q₂ Q_R) (S n₁) (S n₂) (nat_R_S_R n₁ n₂ n_R) in 395s let q₁0 := 395s nat_rect (fun _ : nat => option Q₁) (Some q₁) 395s (fun (_ : nat) (q : option Q₁) => 395s do q0 <- q 395s in do x, q1 <- pop Q₁ q0 395s in do y, q2 <- pop Q₁ q1 in Some (push Q₁ (x + y) q2)) n₁ in 395s let q₂0 := 395s nat_rect (fun _ : nat => option Q₂) (Some q₂) 395s (fun (_ : nat) (q : option Q₂) => 395s do q0 <- q 395s in do x, q1 <- pop Q₂ q0 395s in do y, q2 <- pop Q₂ q1 in Some (push Q₂ (x + y) q2)) n₂ in 395s let q_R0 := 395s nat_rect_R (fun _ : nat => option Q₁) (fun _ : nat => option Q₂) 395s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) => 395s option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (Some q₁) (Some q₂) 395s (option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁ q₂ q_R) 395s (fun (_ : nat) (q : option Q₁) => 395s do q0 <- q 395s in do x, q1 <- pop Q₁ q0 395s in do y, q2 <- pop Q₁ q1 in Some (push Q₁ (x + y) q2)) 395s (fun (_ : nat) (q : option Q₂) => 395s do q0 <- q 395s in do x, q1 <- pop Q₂ q0 395s in do y, q2 <- pop Q₂ q1 in Some (push Q₂ (x + y) q2)) 395s (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) (q₁1 : option Q₁) 395s (q₂1 : option Q₂) (q_R0 : option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁1 q₂1) => 395s bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ (t_R Q₁ Q₂ Q_R) 395s (fun q : Q₁ => 395s do x, q0 <- pop Q₁ q 395s in do y, q1 <- pop Q₁ q0 in Some (push Q₁ (x + y) q1)) 395s (fun q : Q₂ => 395s do x, q0 <- pop Q₂ q 395s in do y, q1 <- pop Q₂ q0 in Some (push Q₂ (x + y) q1)) 395s (fun (q₁2 : Q₁) (q₂2 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁2 q₂2) => 395s bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ 395s (t_R Q₁ Q₂ Q_R) 395s (fun (x : nat) (q : Q₁) => 395s do y, q0 <- pop Q₁ q in Some (push Q₁ (x + y) q0)) 395s (fun (x : nat) (q : Q₂) => 395s do y, q0 <- pop Q₂ q in Some (push Q₂ (x + y) q0)) 395s (fun (x₁ x₂ : nat) (x_R : nat_R x₁ x₂) (q₁3 : Q₁) 395s (q₂3 : Q₂) (q_R2 : t_R Q₁ Q₂ Q_R q₁3 q₂3) => 395s bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ 395s (t_R Q₁ Q₂ Q_R) 395s (fun (y : nat) (q : Q₁) => Some (push Q₁ (x₁ + y) q)) 395s (fun (y : nat) (q : Q₂) => Some (push Q₂ (x₂ + y) q)) 395s (fun (y₁ y₂ : nat) (y_R : nat_R y₁ y₂) 395s (q₁4 : Q₁) (q₂4 : Q₂) (q_R3 : t_R Q₁ Q₂ Q_R q₁4 q₂4) => 395s option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) 395s (push Q₁ (x₁ + y₁) q₁4) (push Q₂ (x₂ + y₂) q₂4) 395s (push_R Q₁ Q₂ Q_R (x₁ + y₁) (x₂ + y₂) 395s (add_R x₁ x₂ x_R y₁ y₂ y_R) q₁4 q₂4 q_R3)) 395s (pop Q₁ q₁3) (pop Q₂ q₂3) (pop_R Q₁ Q₂ Q_R q₁3 q₂3 q_R2)) 395s (pop Q₁ q₁2) (pop Q₂ q₂2) (pop_R Q₁ Q₂ Q_R q₁2 q₂2 q_R1)) q₁1 q₂1 395s q_R0) n₁ n₂ n_R in 395s bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) nat nat nat_R 395s (fun q : Q₁ => option_map fst (pop Q₁ q)) 395s (fun q : Q₂ => option_map fst (pop Q₂ q)) 395s (fun (q₁1 : Q₁) (q₂1 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁1 q₂1) => 395s option_map_R (nat * Q₁) (nat * Q₂) 395s (prod_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) nat nat nat_R fst fst 395s (fst_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (pop Q₁ q₁1) 395s (pop Q₂ q₂1) (pop_R Q₁ Q₂ Q_R q₁1 q₂1 q_R1)) q₁0 q₂0 q_R0 395s : forall Q₁ Q₂ : Queue, 395s Bisimilar Q₁ Q₂ -> 395s forall n₁ n₂ : nat, 395s nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂) 395s 395s Arguments program_R Q₁ Q₂ Q_R (n₁ n₂)%nat_scope n_R 412s declare_abstraction, evd = SHELF: 412s FUTURE GOALS STACK: 412s 412s declare_abstraction, a = 412s 412s |-n1 412s declare_abstraction, b = 412s 412s |-nat 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-3 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-2 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-1 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-0 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-0 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_O_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 0 0 nat_R_O_R) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-3 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s ---> output has cast : false 412s a_R = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s abstraction, evar_map = SHELF: 412s FUTURE GOALS STACK: 412s 412s add_definition, term = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s add_definition, typ = 412s 412s |-(nat_R n1 n1) 412s add_definition, evd = SHELF: 412s FUTURE GOALS STACK: 412s 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-n1 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-3 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-2 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-1 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-0 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-0 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_O_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 0 0 nat_R_O_R) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-3 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-n1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s ---> output has cast : false 412s a_R = 412s 412s |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))) 412s abstraction, evar_map = EVARS: 412s ?X9==[ |- nat_R n1 n1] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s declare_abstraction, evd = SHELF: 412s FUTURE GOALS STACK: 412s 412s declare_abstraction, a = 412s 412s |-n2 412s declare_abstraction, b = 412s 412s |-nat 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n2 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-2 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-1 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-0 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-0 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_O_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 0 0 nat_R_O_R) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s a_R = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s abstraction, evar_map = SHELF: 412s FUTURE GOALS STACK: 412s 412s add_definition, term = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s add_definition, typ = 412s 412s |-(nat_R n2 n2) 412s add_definition, evd = SHELF: 412s FUTURE GOALS STACK: 412s 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-n2 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-2 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-1 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-0 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-0 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_O_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-1 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 0 0 nat_R_O_R) 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-S 412s ---> input has cast : false 412s output = 412s 412s |-nat_R_S_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s input = 412s 412s |-n2 412s ---> input has cast : false 412s output = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s ---> output has cast : false 412s a_R = 412s 412s |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)) 412s abstraction, evar_map = EVARS: 412s ?X10==[ |- nat_R n2 n2] (goal evar) {?Goal} 412s 412s SHELF:|| 412s FUTURE GOALS STACK:|||| 412s 412s ---> Translating mind body ... 412s ---> computing envs ... 412s translate_mind, env = 412s 412s translate_mind, evd = 412s SHELF: 412s FUTURE GOALS STACK: 412s 412s ---> Adding 'I1' to the environment. 412s ---> translatation of params ... 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> input has cast : false 412s output = 412s 412s |-n1_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-n2 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-n2 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-n2_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-n 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-n 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-n_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translatation of inductive ... 412s ---> mind_nparams = 1 412s ---> mind_nparams_rec = 4 412s ---> mind_nparams_ctxt = 4 412s Arity: 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-Prop 412s ---> Computing arity 412s ---> Substitution: 412s 412s 412s |-(I1 _UNBOUND_REL_5) 412s 412s 412s |-(I1 _UNBOUND_REL_6) 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-n1 412s ---> input has cast : false 412s output = 412s 412s |-n1_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-n2 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-n2 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-n2_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-n 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-n 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-n_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-nat 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s 412s |-nat 412s ---> input has cast : false 412s output = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-nat_R 412s ---> output has cast : false 412s Arity_R after substitution: 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s r_R := n_R : nat_R r₁ r₂ 412s 412s |-(I1 n₁ -> I1 n₂ -> Prop) 412s ---> Computing constructors 412s ---> before translation : 412s 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s 412s |-(let p := n1 in let q := n2 in forall n : nat, let r := n in I1 n) 412s ---> remove uniform parameters : 412s 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-(I1 n) 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-(I1 n) 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-n 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-n 412s ---> input has cast : false 412s output = 412s I1₁ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1₂ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1_R : 412s (let p₁ := n1 in 412s let p₂ := n1 in 412s let p_R := n1_R in 412s let q₁ := n2 in 412s let q₂ := n2 in 412s let q_R := n2_R in 412s fun H H0 : forall n : nat, let r := n in Prop => 412s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 412s (let r₁ := n₁ in 412s let r₂ := n₂ in 412s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 412s (H n₁) (H0 n₂)) I1₁ I1₂ 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s r_R := n_R : nat_R r₁ r₂ 412s 412s |-n_R 412s ---> output has cast : false 412s ---> translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-I1 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-I1 412s ---> input has cast : false 412s output = 412s I1₁ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1₂ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1_R : 412s (let p₁ := n1 in 412s let p₂ := n1 in 412s let p_R := n1_R in 412s let q₁ := n2 in 412s let q₂ := n2 in 412s let q_R := n2_R in 412s fun H H0 : forall n : nat, let r := n in Prop => 412s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 412s (let r₁ := n₁ in 412s let r₂ := n₂ in 412s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 412s (H n₁) (H0 n₂)) I1₁ I1₂ 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s r_R := n_R : nat_R r₁ r₂ 412s 412s |-I1_R 412s ---> output has cast : false 412s ---> exit translate 2 evd env t 412s evd =SHELF: 412s FUTURE GOALS STACK: 412s 412s input = 412s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s p := n1 : nat 412s q := n2 : nat 412s n : nat 412s r := n : nat 412s 412s |-(I1 n) 412s ---> input has cast : false 412s output = 412s I1₁ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1₂ : 412s let p := n1 in let q := n2 in forall n : nat, let r := n in Prop 412s I1_R : 412s (let p₁ := n1 in 412s let p₂ := n1 in 412s let p_R := n1_R in 412s let q₁ := n2 in 412s let q₂ := n2 in 412s let q_R := n2_R in 412s fun H H0 : forall n : nat, let r := n in Prop => 412s forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂), 412s (let r₁ := n₁ in 412s let r₂ := n₂ in 412s let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 412s (H n₁) (H0 n₂)) I1₁ I1₂ 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s r_R := n_R : nat_R r₁ r₂ 412s 412s |-(I1_R n₁ n₂ n_R) 412s ---> output has cast : false 412s ---> before substitution: 412s 412s 412s |-(_UNBOUND_REL_15 _UNBOUND_REL_8 _UNBOUND_REL_7 _UNBOUND_REL_6 412s _UNBOUND_REL_2 _UNBOUND_REL_1) 412s ---> constructor n°0 412s ---> substitution : 412s 412s 412s |-(c1 _UNBOUND_REL_5) 412s 412s 412s |-(c1 _UNBOUND_REL_6) 412s 412s 412s |-_UNBOUND_REL_1 412s 412s 412s |-_UNBOUND_REL_2 412s 412s 412s |-_UNBOUND_REL_3 412s 412s 412s |-_UNBOUND_REL_4 412s 412s 412s |-_UNBOUND_REL_5 412s 412s 412s |-_UNBOUND_REL_6 412s 412s 412s |-_UNBOUND_REL_7 412s 412s 412s |-_UNBOUND_REL_8 412s 412s 412s |-_UNBOUND_REL_9 412s 412s 412s |-_UNBOUND_REL_10 412s 412s 412s |-_UNBOUND_REL_11 412s 412s 412s |-_UNBOUND_REL_12 412s 412s 412s |-_UNBOUND_REL_13 412s 412s 412s |-I1 412s 412s 412s |-I1 412s ---> after substitution: 412s 412s 412s |-(_UNBOUND_REL_13 _UNBOUND_REL_6 _UNBOUND_REL_5 _UNBOUND_REL_4 412s (c1 _UNBOUND_REL_6) (c1 _UNBOUND_REL_5)) 412s translate_mind, evd = 412s SHELF: 412s FUTURE GOALS STACK: 412s 412s ---> env_params: 412s acc = 412s def = 412s 412s |-n1 412s typ = 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s def = 412s p₁ := n1 : nat 412s 412s |-n1 412s typ = 412s p₁ := n1 : nat 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s 412s |-n1_R 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s 412s |-(nat_R p₁ p₂) 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-n2 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s 412s |-n2 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s 412s |-n2_R 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s 412s |-(nat_R q₁ q₂) 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s 412s |-(nat_R n₁ n₂) 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-n₁ 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s 412s |-n₂ 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s 412s |-nat 412s acc = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s def = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s 412s |-n_R 412s typ = 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s 412s |-(nat_R r₁ r₂) 412s ---> arities: 412s {mind_entry_record : None 412s mind_entry_finite : Finite 412s 412s mind_entry_params : 412s p₁ := n1 : nat 412s p₂ := n1 : nat 412s p_R := n1_R : nat_R p₁ p₂ 412s q₁ := n2 : nat 412s q₂ := n2 : nat 412s q_R := n2_R : nat_R q₁ q₂ 412s n₁ : nat 412s n₂ : nat 412s n_R : nat_R n₁ n₂ 412s r₁ := n₁ : nat 412s r₂ := n₂ : nat 412s r_R := n_R : nat_R r₁ r₂ 412s 412s mind_entry_inds : { 412s mind_entry_lc : (I1_R n₁ n₂ 412s n_R (c1 n₁) (c1 n₂)) 412s 412s mind_entry_consnames : I1_R_c1_R 412s 412s mind_entry_arity : (I1 n₁ -> 412s I1 n₂ -> Prop) 412s mind_entry_typename : I1_R 412s } 412s 412s mind_entry_polymorphic : false 412s mind_entry_universes : 412s 412s mind_entry_cumulative : false 412s mind_entry_private : None 412s } 412s Prop 412s 412s ---> Translating mind body ... done. 412s evar_map inductive SHELF: 412s FUTURE GOALS STACK: 412s 412s File "./bug3.v", line 20, characters 41-47: 412s Warning: Notation divmod is deprecated since 8.16. 412s The NPeano file is obsolete. Use Nat.divmod instead. 412s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] 413s BinPosDef.Pos.sub_mask = 413s fix sub_mask (x y : positive) {struct y} : BinPosDef.Pos.mask := 413s match x with 413s | (p~1)%positive => 413s match y with 413s | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 413s | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask p q) 413s | 1%positive => BinPosDef.Pos.IsPos p~0 413s end 413s | (p~0)%positive => 413s match y with 413s | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 413s | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 413s | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p) 413s end 413s | 1%positive => 413s match y with 413s | 1%positive => BinPosDef.Pos.IsNul 413s | _ => BinPosDef.Pos.IsNeg 413s end 413s end 413s with sub_mask_carry (x y : positive) {struct y} : BinPosDef.Pos.mask := 413s match x with 413s | (p~1)%positive => 413s match y with 413s | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 413s | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q) 413s | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p) 413s end 413s | (p~0)%positive => 413s match y with 413s | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask_carry p q) 413s | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q) 413s | 1%positive => BinPosDef.Pos.double_pred_mask p 413s end 413s | 1%positive => BinPosDef.Pos.IsNeg 413s end 413s for 413s sub_mask 413s : positive -> positive -> BinPosDef.Pos.mask 413s 413s Arguments BinPosDef.Pos.sub_mask (x y)%positive_scope 413s File "./bug5.v", line 24, characters 41-47: 413s Warning: Notation divmod is deprecated since 8.16. 413s The NPeano file is obsolete. Use Nat.divmod instead. 413s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] 413s T_R = 413s fun H H0 : forall a b : nat, b <> 0 -> modS a b < b => 413s forall (a₁ a₂ : nat) (a_R : nat_R a₁ a₂) (b₁ b₂ : nat) 413s (b_R : nat_R b₁ b₂) (H1 : b₁ <> 0) (H2 : b₂ <> 0), 413s not_R (eq_R nat_R b_R nat_R_O_R) H1 H2 -> 413s lt_R (modS_R a_R b_R) b_R (H a₁ b₁ H1) (H0 a₂ b₂ H2) 413s : T -> T -> Prop 413s 'NNmod_upper_boundA_RR' is now a registered translation. 417s File "./dummyFix.v", line 6, characters 0-59: 417s Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] 417s Inductive bool_P : bool -> Set := 417s bool_P_true_P : bool_P true | bool_P_false_P : bool_P false. 417s boolfun_P = 417s fun H : bool -> bool => forall H0 : bool, bool_P H0 -> bool_P (H H0) 417s : boolfun -> Set 417s myneg_P = 417s fun (b : bool) (b_P : bool_P b) => 417s match 417s b_P in (bool_P b0) 417s return (bool_P match b0 with 417s | true => false 417s | false => true 417s end) 417s with 417s | bool_P_true_P => bool_P_false_P 417s | bool_P_false_P => bool_P_true_P 417s end 417s : forall b : bool, bool_P b -> bool_P (myneg b) 417s 417s Arguments myneg_P b b_P 417s boolfun_R = 417s fun H H0 : bool -> bool => 417s forall H1 H2 : bool, bool_R H1 H2 -> bool_R (H H1) (H0 H2) 417s : boolfun -> boolfun -> Set 417s File "./example.v", line 64, characters 5-9: 417s Warning: Unused variable fale might be a misspelled constructor. Use _ or 417s _fale to silence this warning. [unused-pattern-matching-variable,default] 417s negb_R 417s : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂) 417s negb_R = 417s fun (x₁ x₂ : bool) (x_R : bool_R x₁ x₂) => 417s match 417s x_R in (bool_R x₁0 x₂0) 417s return 417s (bool_R match x₁0 with 417s | true => false 417s | false => true 417s end match x₂0 with 417s | true => false 417s | false => true 417s end) 417s with 417s | bool_R_true_R => bool_R_false_R 417s | bool_R_false_R => bool_R_true_R 417s end 417s : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂) 417s 417s Arguments negb_R x₁ x₂ x_R 417s Type_R = fun H H0 : Type => H -> H0 -> Type 417s : Type -> Type -> Type 417s 417s Arguments Type_R (_ _)%type_scope 417s bool_R : Type_R bool bool 417s : Type_R bool bool 417s boolfun_R : Type_R boolfun boolfun 417s : Type_R boolfun boolfun 417s pType_R : pType_R pType pType 417s : pType_R pType pType 417s arrow_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 417s (B_R : B₁ -> B₂ -> Type) (H : A₁ -> B₁) (H0 : A₂ -> B₂) => 417s forall (H1 : A₁) (H2 : A₂), A_R H1 H2 -> B_R (H H1) (H0 H2) 417s : forall A₁ A₂ : Type, 417s (A₁ -> A₂ -> Type) -> 417s forall B₁ B₂ : Type, 417s (B₁ -> B₂ -> Type) -> arrow A₁ B₁ -> arrow A₂ B₂ -> Type 417s 417s Arguments arrow_R (A₁ A₂)%type_scope A_R%function_scope 417s (B₁ B₂)%type_scope B_R%function_scope _ _ 417s lambda_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 417s (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 417s (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 417s (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) 417s (f₂ : arrow A₂ B₂), 417s arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ -> 417s forall (x₁ : A₁) (x₂ : A₂), 417s A_R x₁ x₂ -> B_R (lambda A₁ B₁ f₁ x₁) (lambda A₂ B₂ f₂ x₂) 417s 417s Arguments lambda_R (A₁ A₂)%type_scope A_R%function_scope 417s (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 417s x₁ x₂ x_R 417s application_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type) 417s (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 417s (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 417s (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) 417s (f₂ : arrow A₂ B₂), 417s arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ -> 417s forall (x₁ : A₁) (x₂ : A₂), 417s A_R x₁ x₂ -> B_R (application A₁ B₁ f₁ x₁) (application A₂ B₂ f₂ x₂) 417s 417s Arguments application_R (A₁ A₂)%type_scope A_R%function_scope 417s (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 417s x₁ x₂ x_R 417s for_all_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ : A₁ -> Type) 417s (B₂ : A₂ -> Type) 417s (B_R : forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type) 417s (H : forall x : A₁, B₁ x) (H0 : forall x : A₂, B₂ x) => 417s forall (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂), B_R x₁ x₂ x_R (H x₁) (H0 x₂) 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (B₁ : A₁ -> Type) (B₂ : A₂ -> Type), 417s (forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type) -> 417s for_all A₁ B₁ -> for_all A₂ B₂ -> Type 417s 417s Arguments for_all_R (A₁ A₂)%type_scope (A_R B₁ B₂ B_R)%function_scope _ _ 417s Inductive nat_R : nat -> nat -> Set := 417s nat_R_O_R : nat_R O O 417s | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0). 417s Inductive 417s list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s : list A₁ -> list A₂ -> Type := 417s list_R_nil_R : list_R A₁ A₂ A_R (nil A₁) (nil A₂) 417s | list_R_cons_R : forall (H : A₁) (H0 : A₂), 417s A_R H H0 -> 417s forall (H1 : list A₁) (H2 : list A₂), 417s list_R A₁ A₂ A_R H1 H2 -> 417s list_R A₁ A₂ A_R (cons A₁ H H1) (cons A₂ H0 H2). 417s 417s Arguments list_R (A₁ A₂)%type_scope A_R%function_scope _ _ 417s Arguments list_R_nil_R (A₁ A₂)%type_scope A_R%function_scope 417s Arguments list_R_cons_R (A₁ A₂)%type_scope A_R%function_scope _ _ _ _ _ _ 417s length_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂) 417s length_R = 417s let fix_length_1 := 417s fix length (A : Type) (l : list A) {struct l} : nat := 417s match l with 417s | nil _ => O 417s | cons _ _ tl => S (length A tl) 417s end in 417s let fix_length_2 := 417s fix length (A : Type) (l : list A) {struct l} : nat := 417s match l with 417s | nil _ => O 417s | cons _ _ tl => S (length A tl) 417s end in 417s fix length_R 417s (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 417s (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) {struct l_R} : 417s nat_R (fix_length_1 A₁ l₁) (fix_length_2 A₂ l₂) := 417s match 417s l_R in (list_R _ _ _ l₁0 l₂0) 417s return (nat_R (fix_length_1 A₁ l₁0) (fix_length_2 A₂ l₂0)) 417s with 417s | list_R_nil_R _ _ _ => nat_R_O_R 417s | list_R_cons_R _ _ _ _ _ _ tl₁ tl₂ tl_R => 417s nat_R_S_R (fix_length_1 A₁ tl₁) (fix_length_2 A₂ tl₂) 417s (length_R A₁ A₂ A_R tl₁ tl₂ tl_R) 417s end 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂) 417s 417s Arguments length_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R 417s list_rec_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (P₁ : list A₁ -> Set) 417s (P₂ : list A₂ -> Set) 417s (P_R : forall (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set) => 417s (fun (A₁0 A₂0 : Type) (A_R0 : A₁0 -> A₂0 -> Type) 417s (P₁0 : list A₁0 -> Type) (P₂0 : list A₂0 -> Type) 417s (P_R0 : forall (l₁ : list A₁0) (l₂ : list A₂0), 417s list_R A₁0 A₂0 A_R0 l₁ l₂ -> P₁0 l₁ -> P₂0 l₂ -> Type) 417s (f₁ : P₁0 (nil A₁0)) (f₂ : P₂0 (nil A₂0)) 417s (f_R : P_R0 (nil A₁0) (nil A₂0) (list_R_nil_R A₁0 A₂0 A_R0) f₁ f₂) 417s (f0₁ : forall (a : A₁0) (l : list A₁0), P₁0 l -> P₁0 (cons A₁0 a l)) 417s (f0₂ : forall (a : A₂0) (l : list A₂0), P₂0 l -> P₂0 (cons A₂0 a l)) 417s (f0_R : forall (a₁ : A₁0) (a₂ : A₂0) (a_R : A_R0 a₁ a₂) 417s (l₁ : list A₁0) (l₂ : list A₂0) 417s (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) (H : P₁0 l₁) 417s (H0 : P₂0 l₂), 417s P_R0 l₁ l₂ l_R H H0 -> 417s P_R0 (cons A₁0 a₁ l₁) (cons A₂0 a₂ l₂) 417s (list_R_cons_R A₁0 A₂0 A_R0 a₁ a₂ a_R l₁ l₂ l_R) 417s (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) => 417s let fix_F_1 := 417s fix F (l : list A₁0) : P₁0 l := 417s match l as l0 return (P₁0 l0) with 417s | nil _ => f₁ 417s | cons _ y l0 => f0₁ y l0 (F l0) 417s end in 417s let fix_F_2 := 417s fix F (l : list A₂0) : P₂0 l := 417s match l as l0 return (P₂0 l0) with 417s | nil _ => f₂ 417s | cons _ y l0 => f0₂ y l0 (F l0) 417s end in 417s fix F_R 417s (l₁ : list A₁0) (l₂ : list A₂0) (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) {struct 417s l_R} : P_R0 l₁ l₂ l_R (fix_F_1 l₁) (fix_F_2 l₂) := 417s match 417s l_R as l_R0 in (list_R _ _ _ l₁0 l₂0) 417s return (P_R0 l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0)) 417s with 417s | list_R_nil_R _ _ _ => f_R 417s | list_R_cons_R _ _ _ y₁ y₂ y_R l₁0 l₂0 l_R0 => 417s f0_R y₁ y₂ y_R l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0) 417s (F_R l₁0 l₂0 l_R0) 417s end) A₁ A₂ A_R P₁ P₂ P_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (P₁ : list A₁ -> Set) (P₂ : list A₂ -> Set) 417s (P_R : forall (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set) 417s (f₁ : P₁ (nil A₁)) (f₂ : P₂ (nil A₂)), 417s P_R (nil A₁) (nil A₂) (list_R_nil_R A₁ A₂ A_R) f₁ f₂ -> 417s forall (f0₁ : forall (a : A₁) (l : list A₁), P₁ l -> P₁ (cons A₁ a l)) 417s (f0₂ : forall (a : A₂) (l : list A₂), P₂ l -> P₂ (cons A₂ a l)), 417s (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂) 417s (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) 417s (H : P₁ l₁) (H0 : P₂ l₂), 417s P_R l₁ l₂ l_R H H0 -> 417s P_R (cons A₁ a₁ l₁) (cons A₂ a₂ l₂) 417s (list_R_cons_R A₁ A₂ A_R a₁ a₂ a_R l₁ l₂ l_R) 417s (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) -> 417s forall (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂), 417s P_R l₁ l₂ l_R (list_rec A₁ P₁ f₁ f0₁ l₁) (list_rec A₂ P₂ f₂ f0₂ l₂) 417s 417s Arguments list_rec_R (A₁ A₂)%type_scope (A_R P₁ P₂ P_R)%function_scope 417s f₁ f₂ f_R (f0₁ f0₂ f0_R)%function_scope l₁ l₂ l_R 417s length2_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂) 417s length2_R = 417s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 417s (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) => 417s list_rec_R A₁ A₂ A_R (fun _ : list A₁ => nat) (fun _ : list A₂ => nat) 417s (fun (l₁0 : list A₁) (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) => 417s nat_R) O O nat_R_O_R (fun (_ : A₁) (_ : list A₁) => S) 417s (fun (_ : A₂) (_ : list A₂) => S) 417s (fun (a₁ : A₁) (a₂ : A₂) (_ : A_R a₁ a₂) (l₁0 : list A₁) 417s (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) => nat_R_S_R) l₁ l₂ l_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂) 417s 417s Arguments length2_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R 417s sum_rect = 417s fun (A B : Type) (P : A + B -> Type) (f : forall a : A, P (inl a)) 417s (f0 : forall b : B, P (inr b)) (s : A + B) => 417s match s as s0 return (P s0) with 417s | inl a => f a 417s | inr b => f0 b 417s end 417s : forall (A B : Type) (P : A + B -> Type), 417s (forall a : A, P (inl a)) -> 417s (forall b : B, P (inr b)) -> forall s : A + B, P s 417s 417s Arguments sum_rect [A B]%type_scope (P f f0)%function_scope s 417s sum_rect 417s : forall (A B : Type) (P : A + B -> Type), 417s (forall a : A, P (inl a)) -> 417s (forall b : B, P (inr b)) -> forall s : A + B, P s 417s sum_rect_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (P₁ : A₁ + B₁ -> Type) 417s (P₂ : A₂ + B₂ -> Type) 417s (P_R : forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂), 417s sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂ -> P₁ s₁ -> P₂ s₂ -> Type) 417s (f₁ : forall a : A₁, P₁ (inl a)) (f₂ : forall a : A₂, P₂ (inl a)), 417s (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂), 417s P_R (inl a₁) (inl a₂) (sum_R_inl_R A₁ A₂ A_R B₁ B₂ B_R a₁ a₂ a_R) 417s (f₁ a₁) (f₂ a₂)) -> 417s forall (f0₁ : forall b : B₁, P₁ (inr b)) 417s (f0₂ : forall b : B₂, P₂ (inr b)), 417s (forall (b₁ : B₁) (b₂ : B₂) (b_R : B_R b₁ b₂), 417s P_R (inr b₁) (inr b₂) (sum_R_inr_R A₁ A₂ A_R B₁ B₂ B_R b₁ b₂ b_R) 417s (f0₁ b₁) (f0₂ b₂)) -> 417s forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂) 417s (s_R : sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂), 417s P_R s₁ s₂ s_R (sum_rect P₁ f₁ f0₁ s₁) (sum_rect P₂ f₂ f0₂ s₂) 417s rev_R 417s : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 417s (l₁ : list A₁) (l₂ : list A₂), 417s list_R A₁ A₂ A_R l₁ l₂ -> list_R A₁ A₂ A_R (List.rev l₁) (List.rev l₂) 417s Module A_R := Struct Definition t_R : A.t -> A.t -> Set. Module B_R End 417s 417s Module A_R.B_R := Struct Definition t_R : A.B.t -> A.B.t -> Set. End 417s 417s Inductive 417s nat_R_10 417s : nat -> 417s nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Set := 417s nat_R_10_O_R_10 : nat_R_10 0 0 0 0 0 0 0 0 0 0 417s | nat_R_10_S_R_10 : forall H H0 H1 H2 H3 H4 H5 H6 H7 H8 : nat, 417s nat_R_10 H H0 H1 H2 H3 H4 H5 H6 H7 H8 -> 417s nat_R_10 (S H) (S H0) (S H1) 417s (S H2) (S H3) (S H4) (S H5) 417s (S H6) (S H7) (S H8). 417s 417s Arguments nat_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope 417s Arguments nat_R_10_S_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope _ 417s 'A_R' is now a registered translation. 417s = opaque 417s : True 417s = opaque_R 417s : True_R opaque opaque 418s autopkgtest [00:22:11]: test upstreamtestsuite: -----------------------] 419s autopkgtest [00:22:12]: test upstreamtestsuite: - - - - - - - - - - results - - - - - - - - - - 419s upstreamtestsuite PASS 419s autopkgtest [00:22:12]: @@@@@@@@@@@@@@@@@@@@ summary 419s upstreamtestsuite PASS 444s Creating nova instance adt-noble-ppc64el-paramcoq-20240326-001513-juju-7f2275-prod-proposed-migration-environment-3 from image adt/ubuntu-noble-ppc64el-server-20240325.img (UUID ce50e202-ac12-4562-879d-419903f0141e)...