0s autopkgtest [20:55:36]: starting date and time: 2024-03-25 20:55:36+0000
  0s autopkgtest [20:55:36]: git checkout: 4a1cd702 l/adt_testbed: don't blame the testbed for unsolvable build deps
  0s autopkgtest [20:55:36]: host juju-7f2275-prod-proposed-migration-environment-2; command line: /home/ubuntu/autopkgtest/runner/autopkgtest --output-dir /tmp/autopkgtest-work.q6nlj4fx/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=src:paramcoq,src:coq --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-2@bos02-s390x-12.secgroup --name adt-noble-s390x-paramcoq-20240325-205536-juju-7f2275-prod-proposed-migration-environment-2 --image adt/ubuntu-noble-s390x-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/
105s autopkgtest [20:57:21]: testbed dpkg architecture: s390x
105s autopkgtest [20:57:21]: testbed apt version: 2.7.12
105s autopkgtest [20:57:21]: @@@@@@@@@@@@@@@@@@@@ test bed setup
106s Get:1 http://ftpmaster.internal/ubuntu noble-proposed InRelease [117 kB]
106s Get:2 http://ftpmaster.internal/ubuntu noble-proposed/restricted Sources [7608 B]
107s Get:3 http://ftpmaster.internal/ubuntu noble-proposed/main Sources [497 kB]
107s Get:4 http://ftpmaster.internal/ubuntu noble-proposed/multiverse Sources [56.0 kB]
107s Get:5 http://ftpmaster.internal/ubuntu noble-proposed/universe Sources [4041 kB]
109s Get:6 http://ftpmaster.internal/ubuntu noble-proposed/main s390x Packages [693 kB]
109s Get:7 http://ftpmaster.internal/ubuntu noble-proposed/main s390x c-n-f Metadata [3032 B]
109s Get:8 http://ftpmaster.internal/ubuntu noble-proposed/restricted s390x Packages [1372 B]
109s Get:9 http://ftpmaster.internal/ubuntu noble-proposed/restricted s390x c-n-f Metadata [116 B]
109s Get:10 http://ftpmaster.internal/ubuntu noble-proposed/universe s390x Packages [4136 kB]
109s Get:11 http://ftpmaster.internal/ubuntu noble-proposed/universe s390x c-n-f Metadata [7292 B]
109s Get:12 http://ftpmaster.internal/ubuntu noble-proposed/multiverse s390x Packages [47.8 kB]
109s Get:13 http://ftpmaster.internal/ubuntu noble-proposed/multiverse s390x c-n-f Metadata [116 B]
112s Fetched 9607 kB in 5s (1986 kB/s)
112s Reading package lists...
115s Reading package lists...
115s Building dependency tree...
115s Reading state information...
116s Calculating upgrade...
116s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
116s Reading package lists...
116s Building dependency tree...
116s Reading state information...
117s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
117s Unknown architecture, assuming PC-style ttyS0
117s sh: Attempting to set up Debian/Ubuntu apt sources automatically
117s sh: Distribution appears to be Ubuntu
118s Reading package lists...
118s Building dependency tree...
118s Reading state information...
119s eatmydata is already the newest version (131-1).
119s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
119s Reading package lists...
119s Building dependency tree...
119s Reading state information...
119s dbus is already the newest version (1.14.10-4ubuntu1).
119s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
119s Reading package lists...
119s Building dependency tree...
119s Reading state information...
120s rng-tools-debian is already the newest version (2.4).
120s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
120s Reading package lists...
120s Building dependency tree...
120s Reading state information...
120s The following packages will be REMOVED:
120s   cloud-init* python3-configobj* python3-debconf*
120s 0 upgraded, 0 newly installed, 3 to remove and 0 not upgraded.
120s After this operation, 3256 kB disk space will be freed.
121s (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 ... 52170 files and directories currently installed.)
121s Removing cloud-init (24.1.2-0ubuntu1) ...
121s Removing python3-configobj (5.0.8-3) ...
121s Removing python3-debconf (1.5.86) ...
121s Processing triggers for man-db (2.12.0-3) ...
122s (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 ... 51781 files and directories currently installed.)
122s Purging configuration files for cloud-init (24.1.2-0ubuntu1) ...
122s dpkg: warning: while removing cloud-init, directory '/etc/cloud/cloud.cfg.d' not empty so not removed
122s Processing triggers for rsyslog (8.2312.0-3ubuntu3) ...
122s invoke-rc.d: policy-rc.d denied execution of try-restart.
123s Reading package lists...
123s Building dependency tree...
123s Reading state information...
123s linux-generic is already the newest version (6.8.0-11.11+1).
123s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
123s Hit:1 http://ftpmaster.internal/ubuntu noble InRelease
124s Hit:2 http://ftpmaster.internal/ubuntu noble-updates InRelease
124s Hit:3 http://ftpmaster.internal/ubuntu noble-security InRelease
126s Reading package lists...
126s Reading package lists...
126s Building dependency tree...
126s Reading state information...
126s Calculating upgrade...
126s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
126s Reading package lists...
126s Building dependency tree...
126s Reading state information...
127s 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
127s autopkgtest [20:57:43]: rebooting testbed after setup commands that affected boot
142s autopkgtest [20:57:58]: testbed running kernel: Linux 6.8.0-11-generic #11-Ubuntu SMP Tue Feb 13 23:45:46 UTC 2024
145s autopkgtest [20:58:01]: @@@@@@@@@@@@@@@@@@@@ apt-source paramcoq
148s Get:1 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (dsc) [2111 B]
148s Get:2 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (tar) [45.8 kB]
148s Get:3 http://ftpmaster.internal/ubuntu noble/universe paramcoq 1.1.3+coq8.18-1 (diff) [3092 B]
148s gpgv: Signature made Thu Dec 21 15:33:52 2023 UTC
148s gpgv:                using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551
148s gpgv:                issuer "jpuydt@debian.org"
148s gpgv: Can't check signature: No public key
148s dpkg-source: warning: cannot verify inline signature for ./paramcoq_1.1.3+coq8.18-1.dsc: no acceptable signature found
148s autopkgtest [20:58:04]: testing package paramcoq version 1.1.3+coq8.18-1
148s autopkgtest [20:58:04]: build not needed
148s autopkgtest [20:58:04]: test upstreamtestsuite: preparing testbed
149s Reading package lists...
150s Building dependency tree...
150s Reading state information...
150s Starting pkgProblemResolver with broken count: 0
150s Starting 2 pkgProblemResolver with broken count: 0
150s Done
150s The following additional packages will be installed:
150s   coq cpp cpp-13 cpp-13-s390x-linux-gnu cpp-s390x-linux-gnu gcc gcc-13
150s   gcc-13-s390x-linux-gnu gcc-s390x-linux-gnu libasan8 libatomic1 libc-dev-bin
150s   libc6-dev libcc1-0 libcompiler-libs-ocaml-dev libcoq-core-ocaml
150s   libcoq-paramcoq libcoq-stdlib libcrypt-dev libfindlib-ocaml libgcc-13-dev
150s   libgomp1 libisl23 libitm1 libmpc3 libncurses-dev libstdlib-ocaml
150s   libstdlib-ocaml-dev libubsan1 libzarith-ocaml linux-libc-dev ocaml
150s   ocaml-base ocaml-findlib ocaml-interp rpcsvc-proto
150s Suggested packages:
150s   coqide | proofgeneral ledit | readline-editor libcoq-core-ocaml-dev why
150s   coq-doc cpp-doc gcc-13-locales cpp-13-doc gcc-multilib manpages-dev autoconf
150s   automake libtool flex bison gdb gcc-doc gcc-13-multilib gcc-13-doc
150s   gdb-s390x-linux-gnu glibc-doc ncurses-doc ocaml-doc elpa-tuareg camlp4
150s Recommended packages:
150s   manpages manpages-dev libc-devtools ocaml-man libfindlib-ocaml-dev ledit
150s   | readline-editor
150s The following NEW packages will be installed:
150s   autopkgtest-satdep coq cpp cpp-13 cpp-13-s390x-linux-gnu cpp-s390x-linux-gnu
150s   gcc gcc-13 gcc-13-s390x-linux-gnu gcc-s390x-linux-gnu libasan8 libatomic1
150s   libc-dev-bin libc6-dev libcc1-0 libcompiler-libs-ocaml-dev libcoq-core-ocaml
150s   libcoq-paramcoq libcoq-stdlib libcrypt-dev libfindlib-ocaml libgcc-13-dev
150s   libgomp1 libisl23 libitm1 libmpc3 libncurses-dev libstdlib-ocaml
150s   libstdlib-ocaml-dev libubsan1 libzarith-ocaml linux-libc-dev ocaml
150s   ocaml-base ocaml-findlib ocaml-interp rpcsvc-proto
150s 0 upgraded, 37 newly installed, 0 to remove and 0 not upgraded.
150s Need to get 373 MB/373 MB of archives.
150s After this operation, 1165 MB of additional disk space will be used.
150s Get:1 /tmp/autopkgtest.9nggWl/1-autopkgtest-satdep.deb autopkgtest-satdep s390x 0 [712 B]
150s Get:2 http://ftpmaster.internal/ubuntu noble/universe s390x libcoq-stdlib s390x 8.18.0+dfsg-1 [35.2 MB]
164s Get:3 http://ftpmaster.internal/ubuntu noble/universe s390x libstdlib-ocaml s390x 4.14.1-1ubuntu1 [394 kB]
164s Get:4 http://ftpmaster.internal/ubuntu noble/universe s390x ocaml-base s390x 4.14.1-1ubuntu1 [278 kB]
164s Get:5 http://ftpmaster.internal/ubuntu noble/universe s390x libfindlib-ocaml s390x 1.9.6-1build3 [199 kB]
164s Get:6 http://ftpmaster.internal/ubuntu noble/universe s390x libzarith-ocaml s390x 1.13-2build3 [125 kB]
164s Get:7 http://ftpmaster.internal/ubuntu noble/universe s390x libcoq-core-ocaml s390x 8.18.0+dfsg-1 [35.3 MB]
175s Get:8 http://ftpmaster.internal/ubuntu noble/universe s390x libstdlib-ocaml-dev s390x 4.14.1-1ubuntu1 [8204 kB]
177s Get:9 http://ftpmaster.internal/ubuntu noble/universe s390x libcompiler-libs-ocaml-dev s390x 4.14.1-1ubuntu1 [37.5 MB]
185s Get:10 http://ftpmaster.internal/ubuntu noble/universe s390x ocaml-interp s390x 4.14.1-1ubuntu1 [7825 kB]
188s Get:11 http://ftpmaster.internal/ubuntu noble/main s390x libc-dev-bin s390x 2.39-0ubuntu6 [20.2 kB]
188s Get:12 http://ftpmaster.internal/ubuntu noble/main s390x linux-libc-dev s390x 6.8.0-11.11 [1590 kB]
188s Get:13 http://ftpmaster.internal/ubuntu noble/main s390x libcrypt-dev s390x 1:4.4.36-4 [135 kB]
188s Get:14 http://ftpmaster.internal/ubuntu noble/main s390x rpcsvc-proto s390x 1.4.2-0ubuntu6 [64.7 kB]
188s Get:15 http://ftpmaster.internal/ubuntu noble/main s390x libc6-dev s390x 2.39-0ubuntu6 [1629 kB]
189s Get:16 http://ftpmaster.internal/ubuntu noble/main s390x libncurses-dev s390x 6.4+20240113-1ubuntu1 [412 kB]
189s Get:17 http://ftpmaster.internal/ubuntu noble/main s390x libisl23 s390x 0.26-3 [722 kB]
189s Get:18 http://ftpmaster.internal/ubuntu noble/main s390x libmpc3 s390x 1.3.1-1 [54.9 kB]
189s Get:19 http://ftpmaster.internal/ubuntu noble/main s390x cpp-13-s390x-linux-gnu s390x 13.2.0-17ubuntu2 [9929 kB]
191s Get:20 http://ftpmaster.internal/ubuntu noble/main s390x cpp-13 s390x 13.2.0-17ubuntu2 [1026 B]
191s Get:21 http://ftpmaster.internal/ubuntu noble/main s390x cpp-s390x-linux-gnu s390x 4:13.2.0-7ubuntu1 [5308 B]
191s Get:22 http://ftpmaster.internal/ubuntu noble/main s390x cpp s390x 4:13.2.0-7ubuntu1 [22.4 kB]
191s Get:23 http://ftpmaster.internal/ubuntu noble/main s390x libcc1-0 s390x 14-20240303-1ubuntu1 [49.9 kB]
191s Get:24 http://ftpmaster.internal/ubuntu noble/main s390x libgomp1 s390x 14-20240303-1ubuntu1 [151 kB]
191s Get:25 http://ftpmaster.internal/ubuntu noble/main s390x libitm1 s390x 14-20240303-1ubuntu1 [31.1 kB]
191s Get:26 http://ftpmaster.internal/ubuntu noble/main s390x libatomic1 s390x 14-20240303-1ubuntu1 [9392 B]
191s Get:27 http://ftpmaster.internal/ubuntu noble/main s390x libasan8 s390x 14-20240303-1ubuntu1 [2998 kB]
192s Get:28 http://ftpmaster.internal/ubuntu noble/main s390x libubsan1 s390x 14-20240303-1ubuntu1 [1186 kB]
192s Get:29 http://ftpmaster.internal/ubuntu noble/main s390x libgcc-13-dev s390x 13.2.0-17ubuntu2 [1003 kB]
192s Get:30 http://ftpmaster.internal/ubuntu noble/main s390x gcc-13-s390x-linux-gnu s390x 13.2.0-17ubuntu2 [19.1 MB]
196s Get:31 http://ftpmaster.internal/ubuntu noble/main s390x gcc-13 s390x 13.2.0-17ubuntu2 [467 kB]
196s Get:32 http://ftpmaster.internal/ubuntu noble/main s390x gcc-s390x-linux-gnu s390x 4:13.2.0-7ubuntu1 [1208 B]
196s Get:33 http://ftpmaster.internal/ubuntu noble/main s390x gcc s390x 4:13.2.0-7ubuntu1 [5014 B]
196s Get:34 http://ftpmaster.internal/ubuntu noble/universe s390x ocaml s390x 4.14.1-1ubuntu1 [82.0 MB]
209s Get:35 http://ftpmaster.internal/ubuntu noble/universe s390x ocaml-findlib s390x 1.9.6-1build3 [587 kB]
209s Get:36 http://ftpmaster.internal/ubuntu noble/universe s390x coq s390x 8.18.0+dfsg-1 [126 MB]
259s Get:37 http://ftpmaster.internal/ubuntu noble/universe s390x libcoq-paramcoq s390x 1.1.3+coq8.18-1 [165 kB]
260s Fetched 373 MB in 1min 49s (3424 kB/s)
260s Selecting previously unselected package libcoq-stdlib.
260s (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 ... 51726 files and directories currently installed.)
260s Preparing to unpack .../00-libcoq-stdlib_8.18.0+dfsg-1_s390x.deb ...
260s Unpacking libcoq-stdlib (8.18.0+dfsg-1) ...
261s Selecting previously unselected package libstdlib-ocaml.
261s Preparing to unpack .../01-libstdlib-ocaml_4.14.1-1ubuntu1_s390x.deb ...
261s Unpacking libstdlib-ocaml (4.14.1-1ubuntu1) ...
261s Selecting previously unselected package ocaml-base.
261s Preparing to unpack .../02-ocaml-base_4.14.1-1ubuntu1_s390x.deb ...
261s Unpacking ocaml-base (4.14.1-1ubuntu1) ...
261s Selecting previously unselected package libfindlib-ocaml.
261s Preparing to unpack .../03-libfindlib-ocaml_1.9.6-1build3_s390x.deb ...
261s Unpacking libfindlib-ocaml (1.9.6-1build3) ...
261s Selecting previously unselected package libzarith-ocaml.
261s Preparing to unpack .../04-libzarith-ocaml_1.13-2build3_s390x.deb ...
261s Unpacking libzarith-ocaml (1.13-2build3) ...
261s Selecting previously unselected package libcoq-core-ocaml.
261s Preparing to unpack .../05-libcoq-core-ocaml_8.18.0+dfsg-1_s390x.deb ...
261s Unpacking libcoq-core-ocaml (8.18.0+dfsg-1) ...
262s Selecting previously unselected package libstdlib-ocaml-dev.
262s Preparing to unpack .../06-libstdlib-ocaml-dev_4.14.1-1ubuntu1_s390x.deb ...
262s Unpacking libstdlib-ocaml-dev (4.14.1-1ubuntu1) ...
262s Selecting previously unselected package libcompiler-libs-ocaml-dev.
262s Preparing to unpack .../07-libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1_s390x.deb ...
262s Unpacking libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ...
264s Selecting previously unselected package ocaml-interp.
264s Preparing to unpack .../08-ocaml-interp_4.14.1-1ubuntu1_s390x.deb ...
264s Unpacking ocaml-interp (4.14.1-1ubuntu1) ...
264s Selecting previously unselected package libc-dev-bin.
264s Preparing to unpack .../09-libc-dev-bin_2.39-0ubuntu6_s390x.deb ...
264s Unpacking libc-dev-bin (2.39-0ubuntu6) ...
264s Selecting previously unselected package linux-libc-dev:s390x.
264s Preparing to unpack .../10-linux-libc-dev_6.8.0-11.11_s390x.deb ...
264s Unpacking linux-libc-dev:s390x (6.8.0-11.11) ...
264s Selecting previously unselected package libcrypt-dev:s390x.
264s Preparing to unpack .../11-libcrypt-dev_1%3a4.4.36-4_s390x.deb ...
264s Unpacking libcrypt-dev:s390x (1:4.4.36-4) ...
264s Selecting previously unselected package rpcsvc-proto.
264s Preparing to unpack .../12-rpcsvc-proto_1.4.2-0ubuntu6_s390x.deb ...
264s Unpacking rpcsvc-proto (1.4.2-0ubuntu6) ...
264s Selecting previously unselected package libc6-dev:s390x.
264s Preparing to unpack .../13-libc6-dev_2.39-0ubuntu6_s390x.deb ...
264s Unpacking libc6-dev:s390x (2.39-0ubuntu6) ...
264s Selecting previously unselected package libncurses-dev:s390x.
264s Preparing to unpack .../14-libncurses-dev_6.4+20240113-1ubuntu1_s390x.deb ...
264s Unpacking libncurses-dev:s390x (6.4+20240113-1ubuntu1) ...
264s Selecting previously unselected package libisl23:s390x.
264s Preparing to unpack .../15-libisl23_0.26-3_s390x.deb ...
264s Unpacking libisl23:s390x (0.26-3) ...
264s Selecting previously unselected package libmpc3:s390x.
264s Preparing to unpack .../16-libmpc3_1.3.1-1_s390x.deb ...
264s Unpacking libmpc3:s390x (1.3.1-1) ...
264s Selecting previously unselected package cpp-13-s390x-linux-gnu.
264s Preparing to unpack .../17-cpp-13-s390x-linux-gnu_13.2.0-17ubuntu2_s390x.deb ...
264s Unpacking cpp-13-s390x-linux-gnu (13.2.0-17ubuntu2) ...
265s Selecting previously unselected package cpp-13.
265s Preparing to unpack .../18-cpp-13_13.2.0-17ubuntu2_s390x.deb ...
265s Unpacking cpp-13 (13.2.0-17ubuntu2) ...
265s Selecting previously unselected package cpp-s390x-linux-gnu.
265s Preparing to unpack .../19-cpp-s390x-linux-gnu_4%3a13.2.0-7ubuntu1_s390x.deb ...
265s Unpacking cpp-s390x-linux-gnu (4:13.2.0-7ubuntu1) ...
265s Selecting previously unselected package cpp.
265s Preparing to unpack .../20-cpp_4%3a13.2.0-7ubuntu1_s390x.deb ...
265s Unpacking cpp (4:13.2.0-7ubuntu1) ...
265s Selecting previously unselected package libcc1-0:s390x.
265s Preparing to unpack .../21-libcc1-0_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libcc1-0:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libgomp1:s390x.
265s Preparing to unpack .../22-libgomp1_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libgomp1:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libitm1:s390x.
265s Preparing to unpack .../23-libitm1_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libitm1:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libatomic1:s390x.
265s Preparing to unpack .../24-libatomic1_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libatomic1:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libasan8:s390x.
265s Preparing to unpack .../25-libasan8_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libasan8:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libubsan1:s390x.
265s Preparing to unpack .../26-libubsan1_14-20240303-1ubuntu1_s390x.deb ...
265s Unpacking libubsan1:s390x (14-20240303-1ubuntu1) ...
265s Selecting previously unselected package libgcc-13-dev:s390x.
265s Preparing to unpack .../27-libgcc-13-dev_13.2.0-17ubuntu2_s390x.deb ...
265s Unpacking libgcc-13-dev:s390x (13.2.0-17ubuntu2) ...
265s Selecting previously unselected package gcc-13-s390x-linux-gnu.
265s Preparing to unpack .../28-gcc-13-s390x-linux-gnu_13.2.0-17ubuntu2_s390x.deb ...
265s Unpacking gcc-13-s390x-linux-gnu (13.2.0-17ubuntu2) ...
266s Selecting previously unselected package gcc-13.
266s Preparing to unpack .../29-gcc-13_13.2.0-17ubuntu2_s390x.deb ...
266s Unpacking gcc-13 (13.2.0-17ubuntu2) ...
266s Selecting previously unselected package gcc-s390x-linux-gnu.
266s Preparing to unpack .../30-gcc-s390x-linux-gnu_4%3a13.2.0-7ubuntu1_s390x.deb ...
266s Unpacking gcc-s390x-linux-gnu (4:13.2.0-7ubuntu1) ...
266s Selecting previously unselected package gcc.
266s Preparing to unpack .../31-gcc_4%3a13.2.0-7ubuntu1_s390x.deb ...
266s Unpacking gcc (4:13.2.0-7ubuntu1) ...
266s Selecting previously unselected package ocaml.
266s Preparing to unpack .../32-ocaml_4.14.1-1ubuntu1_s390x.deb ...
266s Unpacking ocaml (4.14.1-1ubuntu1) ...
268s Selecting previously unselected package ocaml-findlib.
268s Preparing to unpack .../33-ocaml-findlib_1.9.6-1build3_s390x.deb ...
268s Unpacking ocaml-findlib (1.9.6-1build3) ...
268s Selecting previously unselected package coq.
268s Preparing to unpack .../34-coq_8.18.0+dfsg-1_s390x.deb ...
268s Unpacking coq (8.18.0+dfsg-1) ...
271s Selecting previously unselected package libcoq-paramcoq.
271s Preparing to unpack .../35-libcoq-paramcoq_1.1.3+coq8.18-1_s390x.deb ...
271s Unpacking libcoq-paramcoq (1.1.3+coq8.18-1) ...
271s Selecting previously unselected package autopkgtest-satdep.
271s Preparing to unpack .../36-1-autopkgtest-satdep.deb ...
271s Unpacking autopkgtest-satdep (0) ...
271s Setting up linux-libc-dev:s390x (6.8.0-11.11) ...
271s Setting up libgomp1:s390x (14-20240303-1ubuntu1) ...
271s Setting up libcoq-stdlib (8.18.0+dfsg-1) ...
271s Setting up rpcsvc-proto (1.4.2-0ubuntu6) ...
271s Setting up libstdlib-ocaml (4.14.1-1ubuntu1) ...
271s Setting up libmpc3:s390x (1.3.1-1) ...
271s Setting up libatomic1:s390x (14-20240303-1ubuntu1) ...
271s Setting up ocaml-base (4.14.1-1ubuntu1) ...
271s Setting up libubsan1:s390x (14-20240303-1ubuntu1) ...
271s Setting up libcrypt-dev:s390x (1:4.4.36-4) ...
271s Setting up libasan8:s390x (14-20240303-1ubuntu1) ...
271s Setting up libisl23:s390x (0.26-3) ...
271s Setting up libc-dev-bin (2.39-0ubuntu6) ...
271s Setting up libcc1-0:s390x (14-20240303-1ubuntu1) ...
271s Setting up libitm1:s390x (14-20240303-1ubuntu1) ...
271s Setting up libstdlib-ocaml-dev (4.14.1-1ubuntu1) ...
271s Setting up libcoq-paramcoq (1.1.3+coq8.18-1) ...
271s Setting up libfindlib-ocaml (1.9.6-1build3) ...
271s Setting up libzarith-ocaml (1.13-2build3) ...
271s Setting up libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ...
271s Setting up ocaml-interp (4.14.1-1ubuntu1) ...
271s Setting up cpp-13-s390x-linux-gnu (13.2.0-17ubuntu2) ...
271s Setting up ocaml-findlib (1.9.6-1build3) ...
271s Setting up libgcc-13-dev:s390x (13.2.0-17ubuntu2) ...
271s Setting up libcoq-core-ocaml (8.18.0+dfsg-1) ...
271s Setting up libc6-dev:s390x (2.39-0ubuntu6) ...
271s Setting up libncurses-dev:s390x (6.4+20240113-1ubuntu1) ...
271s Setting up cpp-13 (13.2.0-17ubuntu2) ...
271s Setting up cpp-s390x-linux-gnu (4:13.2.0-7ubuntu1) ...
271s Setting up gcc-13-s390x-linux-gnu (13.2.0-17ubuntu2) ...
271s Setting up gcc-s390x-linux-gnu (4:13.2.0-7ubuntu1) ...
271s Setting up gcc-13 (13.2.0-17ubuntu2) ...
271s Setting up cpp (4:13.2.0-7ubuntu1) ...
271s Setting up gcc (4:13.2.0-7ubuntu1) ...
271s Setting up ocaml (4.14.1-1ubuntu1) ...
271s Setting up coq (8.18.0+dfsg-1) ...
271s Setting up autopkgtest-satdep (0) ...
271s Processing triggers for man-db (2.12.0-3) ...
272s Processing triggers for libc-bin (2.39-0ubuntu6) ...
275s (Reading database ... 59470 files and directories currently installed.)
275s Removing autopkgtest-satdep (0) ...
275s autopkgtest [21:00:11]: test upstreamtestsuite: [-----------------------
299s Inductive nat_R : nat -> nat -> Set :=
299s     nat_R_O_R : nat_R 0 0
299s   | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0).
299s 
299s Arguments nat_R (_ _)%nat_scope
299s Arguments nat_R_S_R (_ _)%nat_scope _
299s Variant Queue_R : Queue -> Queue -> Type :=
299s     Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 
299s                               (t_R : t₁ -> t₂ -> Type) 
299s                               (empty₁ : t₁) (empty₂ : t₂),
299s                             t_R empty₁ empty₂ ->
299s                             forall (push₁ : nat -> t₁ -> t₁)
299s                               (push₂ : nat -> t₂ -> t₂),
299s                             (forall H H0 : nat,
299s                              nat_R H H0 ->
299s                              forall (H1 : t₁) (H2 : t₂),
299s                              t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) ->
299s                             forall (pop₁ : t₁ -> option (nat * t₁))
299s                               (pop₂ : t₂ -> option (nat * t₂)),
299s                             (forall (H : t₁) (H0 : t₂),
299s                              t_R H H0 ->
299s                              option_R (nat * t₁) (nat * t₂)
299s                                (prod_R nat nat nat_R t₁ t₂ t_R) 
299s                                (pop₁ H) (pop₂ H0)) ->
299s                             Queue_R
299s                               {|
299s                                 t := t₁;
299s                                 empty := empty₁;
299s                                 push := push₁;
299s                                 pop := pop₁
299s                               |}
299s                               {|
299s                                 t := t₂;
299s                                 empty := empty₂;
299s                                 push := push₂;
299s                                 pop := pop₂
299s                               |}.
299s 
299s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 
299s   t_R%function_scope empty₁ empty₂ empty_R
299s   (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope
299s Queue_R
299s      : Queue -> Queue -> Type
299s Variant Queue_R : Queue -> Queue -> Type :=
299s     Queue_R_Build_Queue_R : forall (t₁ t₂ : Type) 
299s                               (t_R : t₁ -> t₂ -> Type) 
299s                               (empty₁ : t₁) (empty₂ : t₂),
299s                             t_R empty₁ empty₂ ->
299s                             forall (push₁ : nat -> t₁ -> t₁)
299s                               (push₂ : nat -> t₂ -> t₂),
299s                             (forall H H0 : nat,
299s                              nat_R H H0 ->
299s                              forall (H1 : t₁) (H2 : t₂),
299s                              t_R H1 H2 -> t_R (push₁ H H1) (push₂ H0 H2)) ->
299s                             forall (pop₁ : t₁ -> option (nat * t₁))
299s                               (pop₂ : t₂ -> option (nat * t₂)),
299s                             (forall (H : t₁) (H0 : t₂),
299s                              t_R H H0 ->
299s                              option_R (nat * t₁) (nat * t₂)
299s                                (prod_R nat nat nat_R t₁ t₂ t_R) 
299s                                (pop₁ H) (pop₂ H0)) ->
299s                             Bisimilar
299s                               {|
299s                                 t := t₁;
299s                                 empty := empty₁;
299s                                 push := push₁;
299s                                 pop := pop₁
299s                               |}
299s                               {|
299s                                 t := t₂;
299s                                 empty := empty₂;
299s                                 push := push₂;
299s                                 pop := pop₂
299s                               |}.
299s 
299s Arguments Queue_R_Build_Queue_R (t₁ t₂)%type_scope 
299s   t_R%function_scope empty₁ empty₂ empty_R
299s   (push₁ push₂ push_R pop₁ pop₂ pop_R)%function_scope
299s File "./ListQueue.v", line 127, characters 36-43:
299s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead.
299s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default]
299s File "./ListQueue.v", line 127, characters 36-43:
299s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead.
299s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default]
299s File "./ListQueue.v", line 127, characters 36-43:
299s Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead.
299s [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default]
299s program =
299s fun (Q : Queue) (n : nat) =>
299s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in
299s let q0 :=
299s   nat_rect (fun _ : nat => option Q) (Some q)
299s     (fun (_ : nat) (q0 : option Q) =>
299s      do q1 <- q0
299s      in do x, q2  <- pop Q q1
299s         in do y, q3  <- pop Q q2 in Some (push Q (x + y) q3)) n in
299s do q1 <- q0 in option_map fst (pop Q q1)
299s      : Queue -> nat -> option nat
299s 
299s Arguments program Q n%nat_scope
299s program
299s      : Queue -> nat -> option nat
299s program_R
299s      : forall Q₁ Q₂ : Queue,
299s        Bisimilar Q₁ Q₂ ->
299s        forall n₁ n₂ : nat,
299s        nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂)
299s program =
299s fun (Q : Queue) (n : nat) =>
299s let q := nat_rect (fun _ : nat => Q) (empty Q) (push Q) (S n) in
299s let q0 :=
299s   nat_rect (fun _ : nat => option Q) (Some q)
299s     (fun (_ : nat) (q0 : option Q) =>
299s      do q1 <- q0
299s      in do x, q2  <- pop Q q1
299s         in do y, q3  <- pop Q q2 in Some (push Q (x + y) q3)) n in
299s do q1 <- q0 in option_map fst (pop Q q1)
299s      : Queue -> nat -> option nat
299s 
299s Arguments program Q n%nat_scope
299s program_R =
299s fun (Q₁ Q₂ : Queue) (Q_R : Bisimilar Q₁ Q₂) (n₁ n₂ : nat) (n_R : nat_R n₁ n₂)
299s =>
299s let q₁ := nat_rect (fun _ : nat => Q₁) (empty Q₁) (push Q₁) (S n₁) in
299s let q₂ := nat_rect (fun _ : nat => Q₂) (empty Q₂) (push Q₂) (S n₂) in
299s let q_R :=
299s   nat_rect_R (fun _ : nat => Q₁) (fun _ : nat => Q₂)
299s     (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) => t_R Q₁ Q₂ Q_R) 
299s     (empty Q₁) (empty Q₂) (empty_R Q₁ Q₂ Q_R) (push Q₁) 
299s     (push Q₂) (push_R Q₁ Q₂ Q_R) (S n₁) (S n₂) (nat_R_S_R n₁ n₂ n_R) in
299s let q₁0 :=
299s   nat_rect (fun _ : nat => option Q₁) (Some q₁)
299s     (fun (_ : nat) (q : option Q₁) =>
299s      do q0 <- q
299s      in do x, q1  <- pop Q₁ q0
299s         in do y, q2  <- pop Q₁ q1 in Some (push Q₁ (x + y) q2)) n₁ in
299s let q₂0 :=
299s   nat_rect (fun _ : nat => option Q₂) (Some q₂)
299s     (fun (_ : nat) (q : option Q₂) =>
299s      do q0 <- q
299s      in do x, q1  <- pop Q₂ q0
299s         in do y, q2  <- pop Q₂ q1 in Some (push Q₂ (x + y) q2)) n₂ in
299s let q_R0 :=
299s   nat_rect_R (fun _ : nat => option Q₁) (fun _ : nat => option Q₂)
299s     (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) =>
299s      option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (Some q₁) (Some q₂)
299s     (option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁ q₂ q_R)
299s     (fun (_ : nat) (q : option Q₁) =>
299s      do q0 <- q
299s      in do x, q1  <- pop Q₁ q0
299s         in do y, q2  <- pop Q₁ q1 in Some (push Q₁ (x + y) q2))
299s     (fun (_ : nat) (q : option Q₂) =>
299s      do q0 <- q
299s      in do x, q1  <- pop Q₂ q0
299s         in do y, q2  <- pop Q₂ q1 in Some (push Q₂ (x + y) q2))
299s     (fun (n₁0 n₂0 : nat) (_ : nat_R n₁0 n₂0) (q₁1 : option Q₁)
299s        (q₂1 : option Q₂) (q_R0 : option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) q₁1 q₂1) =>
299s      bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂ (t_R Q₁ Q₂ Q_R)
299s        (fun q : Q₁ =>
299s         do x, q0  <- pop Q₁ q
299s         in do y, q1  <- pop Q₁ q0 in Some (push Q₁ (x + y) q1))
299s        (fun q : Q₂ =>
299s         do x, q0  <- pop Q₂ q
299s         in do y, q1  <- pop Q₂ q0 in Some (push Q₂ (x + y) q1))
299s        (fun (q₁2 : Q₁) (q₂2 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁2 q₂2) =>
299s         bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂
299s           (t_R Q₁ Q₂ Q_R)
299s           (fun (x : nat) (q : Q₁) =>
299s            do y, q0  <- pop Q₁ q in Some (push Q₁ (x + y) q0))
299s           (fun (x : nat) (q : Q₂) =>
299s            do y, q0  <- pop Q₂ q in Some (push Q₂ (x + y) q0))
299s           (fun (x₁ x₂ : nat) (x_R : nat_R x₁ x₂) (q₁3 : Q₁) 
299s              (q₂3 : Q₂) (q_R2 : t_R Q₁ Q₂ Q_R q₁3 q₂3) =>
299s            bind_option2_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) Q₁ Q₂
299s              (t_R Q₁ Q₂ Q_R)
299s              (fun (y : nat) (q : Q₁) => Some (push Q₁ (x₁ + y) q))
299s              (fun (y : nat) (q : Q₂) => Some (push Q₂ (x₂ + y) q))
299s              (fun (y₁ y₂ : nat) (y_R : nat_R y₁ y₂) 
299s                 (q₁4 : Q₁) (q₂4 : Q₂) (q_R3 : t_R Q₁ Q₂ Q_R q₁4 q₂4) =>
299s               option_R_Some_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) 
299s                 (push Q₁ (x₁ + y₁) q₁4) (push Q₂ (x₂ + y₂) q₂4)
299s                 (push_R Q₁ Q₂ Q_R (x₁ + y₁) (x₂ + y₂)
299s                    (add_R x₁ x₂ x_R y₁ y₂ y_R) q₁4 q₂4 q_R3)) 
299s              (pop Q₁ q₁3) (pop Q₂ q₂3) (pop_R Q₁ Q₂ Q_R q₁3 q₂3 q_R2))
299s           (pop Q₁ q₁2) (pop Q₂ q₂2) (pop_R Q₁ Q₂ Q_R q₁2 q₂2 q_R1)) q₁1 q₂1
299s        q_R0) n₁ n₂ n_R in
299s bind_option_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R) nat nat nat_R
299s   (fun q : Q₁ => option_map fst (pop Q₁ q))
299s   (fun q : Q₂ => option_map fst (pop Q₂ q))
299s   (fun (q₁1 : Q₁) (q₂1 : Q₂) (q_R1 : t_R Q₁ Q₂ Q_R q₁1 q₂1) =>
299s    option_map_R (nat * Q₁) (nat * Q₂)
299s      (prod_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) nat nat nat_R fst fst
299s      (fst_R nat nat nat_R Q₁ Q₂ (t_R Q₁ Q₂ Q_R)) (pop Q₁ q₁1) 
299s      (pop Q₂ q₂1) (pop_R Q₁ Q₂ Q_R q₁1 q₂1 q_R1)) q₁0 q₂0 q_R0
299s      : forall Q₁ Q₂ : Queue,
299s        Bisimilar Q₁ Q₂ ->
299s        forall n₁ n₂ : nat,
299s        nat_R n₁ n₂ -> option_R nat nat nat_R (program Q₁ n₁) (program Q₂ n₂)
299s 
299s Arguments program_R Q₁ Q₂ Q_R (n₁ n₂)%nat_scope n_R
324s declare_abstraction, evd  = SHELF:
324s FUTURE GOALS STACK:
324s 
324s declare_abstraction, a =
324s 
324s  |-n1
324s declare_abstraction, b =
324s 
324s  |-nat
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-nat
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-nat
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-n1
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-3
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-2
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-1
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-0
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-0
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_O_R
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-1
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 0 0 nat_R_O_R)
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-2
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-3
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-n1
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s --->	output has cast : false
324s a_R = 
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s abstraction, evar_map = SHELF:
324s FUTURE GOALS STACK:
324s 
324s add_definition, term = 
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s add_definition, typ  = 
324s 
324s  |-(nat_R n1 n1)
324s add_definition, evd  = SHELF:
324s FUTURE GOALS STACK:
324s 
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-n1
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-3
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-2
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-1
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-0
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-0
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_O_R
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-1
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 0 0 nat_R_O_R)
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-2
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-3
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =EVARS:?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s input =
324s 
324s  |-n1
324s --->	input has cast : false
324s output =
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s --->	output has cast : false
324s a_R = 
324s 
324s  |-(nat_R_S_R 2 2 (nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R)))
324s abstraction, evar_map = EVARS:
324s  ?X9==[ |- nat_R n1 n1] (goal evar) {?Goal}
324s 
324s SHELF:||
324s FUTURE GOALS STACK:||||
324s 
324s declare_abstraction, evd  = SHELF:
324s FUTURE GOALS STACK:
324s 
324s declare_abstraction, a =
324s 
324s  |-n2
324s declare_abstraction, b =
324s 
324s  |-nat
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-nat
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-nat
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-n2
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-2
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-1
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-0
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-0
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_O_R
324s --->	output has cast : false
324s --->	translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
324s 
324s  |-S
324s --->	input has cast : false
324s output =
324s 
324s  |-nat_R_S_R
324s --->	output has cast : false
324s --->	exit translate 2 evd env t
324s evd =SHELF:
324s FUTURE GOALS STACK:
324s 
324s input =
325s 
325s  |-1
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 0 0 nat_R_O_R)
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-S
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-S
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R_S_R
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-2
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-n2
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s --->	output has cast : false
325s a_R = 
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s abstraction, evar_map = SHELF:
325s FUTURE GOALS STACK:
325s 
325s add_definition, term = 
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s add_definition, typ  = 
325s 
325s  |-(nat_R n2 n2)
325s add_definition, evd  = SHELF:
325s FUTURE GOALS STACK:
325s 
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-n2
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-2
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-1
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-0
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-0
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R_O_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-S
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-S
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R_S_R
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-1
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 0 0 nat_R_O_R)
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-S
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-S
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R_S_R
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-2
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =EVARS:?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s input =
325s 
325s  |-n2
325s --->	input has cast : false
325s output =
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s --->	output has cast : false
325s a_R = 
325s 
325s  |-(nat_R_S_R 1 1 (nat_R_S_R 0 0 nat_R_O_R))
325s abstraction, evar_map = EVARS:
325s  ?X10==[ |- nat_R n2 n2] (goal evar) {?Goal}
325s 
325s SHELF:||
325s FUTURE GOALS STACK:||||
325s 
325s --->	Translating mind body ...
325s --->	computing envs ...
325s translate_mind, env = 
325s 
325s translate_mind, evd = 
325s SHELF:
325s FUTURE GOALS STACK:
325s 
325s --->	Adding 'I1' to the environment.
325s --->	translatation of params ...
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-n1
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-n1
325s --->	input has cast : false
325s output =
325s 
325s  |-n1_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-n2
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-n2
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-n2_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-n
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-n
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s 
325s  |-n_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translatation of inductive ...
325s --->	mind_nparams = 1
325s --->	mind_nparams_rec = 4
325s --->	mind_nparams_ctxt = 4
325s Arity:
325s       p := n1 : nat
325s       q := n2 : nat
325s       n : nat
325s       r := n : nat
325s 
325s  |-Prop
325s --->	Computing arity
325s --->	Substitution:
325s 
325s 
325s  |-(I1 _UNBOUND_REL_5)
325s 
325s 
325s  |-(I1 _UNBOUND_REL_6)
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-n1
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-n1
325s --->	input has cast : false
325s output =
325s 
325s  |-n1_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-n2
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-n2
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-n2_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-n
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-n
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s 
325s  |-n_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-nat
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s 
325s  |-nat
325s --->	input has cast : false
325s output =
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s 
325s  |-nat_R
325s --->	output has cast : false
325s Arity_R after substitution:
325s                            p₁ := n1 : nat
325s                            p₂ := n1 : nat
325s                            p_R := n1_R : nat_R p₁ p₂
325s                            q₁ := n2 : nat
325s                            q₂ := n2 : nat
325s                            q_R := n2_R : nat_R q₁ q₂
325s                            n₁ : nat
325s                            n₂ : nat
325s                            n_R : nat_R n₁ n₂
325s                            r₁ := n₁ : nat
325s                            r₂ := n₂ : nat
325s                            r_R := n_R : nat_R r₁ r₂
325s 
325s  |-(I1 n₁ -> I1 n₂ -> Prop)
325s --->	Computing constructors
325s --->	before translation :
325s 
325s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s 
325s  |-(let p := n1 in let q := n2 in forall n : nat, let r := n in I1 n)
325s --->	remove uniform parameters :
325s 
325s I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s p := n1 : nat
325s q := n2 : nat
325s n : nat
325s r := n : nat
325s 
325s  |-(I1 n)
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-(I1 n)
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-n
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-n
325s --->	input has cast : false
325s output =
325s         I1₁ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1₂ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1_R :
325s         (let p₁ := n1 in
325s          let p₂ := n1 in
325s          let p_R := n1_R in
325s          let q₁ := n2 in
325s          let q₂ := n2 in
325s          let q_R := n2_R in
325s          fun H H0 : forall n : nat, let r := n in Prop =>
325s          forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂),
325s          (let r₁ := n₁ in
325s           let r₂ := n₂ in
325s           let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 
325s            (H n₁) (H0 n₂)) I1₁ I1₂
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s         r₁ := n₁ : nat
325s         r₂ := n₂ : nat
325s         r_R := n_R : nat_R r₁ r₂
325s 
325s  |-n_R
325s --->	output has cast : false
325s --->	translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-I1
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-I1
325s --->	input has cast : false
325s output =
325s         I1₁ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1₂ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1_R :
325s         (let p₁ := n1 in
325s          let p₂ := n1 in
325s          let p_R := n1_R in
325s          let q₁ := n2 in
325s          let q₂ := n2 in
325s          let q_R := n2_R in
325s          fun H H0 : forall n : nat, let r := n in Prop =>
325s          forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂),
325s          (let r₁ := n₁ in
325s           let r₂ := n₂ in
325s           let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 
325s            (H n₁) (H0 n₂)) I1₁ I1₂
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s         r₁ := n₁ : nat
325s         r₂ := n₂ : nat
325s         r_R := n_R : nat_R r₁ r₂
325s 
325s  |-I1_R
325s --->	output has cast : false
325s --->	exit translate 2 evd env t
325s evd =SHELF:
325s FUTURE GOALS STACK:
325s 
325s input =
325s        I1 : let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s        p := n1 : nat
325s        q := n2 : nat
325s        n : nat
325s        r := n : nat
325s 
325s  |-(I1 n)
325s --->	input has cast : false
325s output =
325s         I1₁ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1₂ :
325s         let p := n1 in let q := n2 in forall n : nat, let r := n in Prop
325s         I1_R :
325s         (let p₁ := n1 in
325s          let p₂ := n1 in
325s          let p_R := n1_R in
325s          let q₁ := n2 in
325s          let q₂ := n2 in
325s          let q_R := n2_R in
325s          fun H H0 : forall n : nat, let r := n in Prop =>
325s          forall (n₁ n₂ : nat) (n_R : nat_R n₁ n₂),
325s          (let r₁ := n₁ in
325s           let r₂ := n₂ in
325s           let r_R := n_R in fun H1 H2 : Prop => H1 -> H2 -> Prop) 
325s            (H n₁) (H0 n₂)) I1₁ I1₂
325s         p₁ := n1 : nat
325s         p₂ := n1 : nat
325s         p_R := n1_R : nat_R p₁ p₂
325s         q₁ := n2 : nat
325s         q₂ := n2 : nat
325s         q_R := n2_R : nat_R q₁ q₂
325s         n₁ : nat
325s         n₂ : nat
325s         n_R : nat_R n₁ n₂
325s         r₁ := n₁ : nat
325s         r₂ := n₂ : nat
325s         r_R := n_R : nat_R r₁ r₂
325s 
325s  |-(I1_R n₁ n₂ n_R)
325s --->	output has cast : false
325s --->	before substitution:
325s 
325s 
325s  |-(_UNBOUND_REL_15 _UNBOUND_REL_8 _UNBOUND_REL_7 _UNBOUND_REL_6
325s        _UNBOUND_REL_2 _UNBOUND_REL_1)
325s --->	constructor n°0
325s --->	substitution :
325s 
325s 
325s  |-(c1 _UNBOUND_REL_5)
325s 
325s 
325s  |-(c1 _UNBOUND_REL_6)
325s 
325s 
325s  |-_UNBOUND_REL_1
325s 
325s 
325s  |-_UNBOUND_REL_2
325s 
325s 
325s  |-_UNBOUND_REL_3
325s 
325s 
325s  |-_UNBOUND_REL_4
325s 
325s 
325s  |-_UNBOUND_REL_5
325s 
325s 
325s  |-_UNBOUND_REL_6
325s 
325s 
325s  |-_UNBOUND_REL_7
325s 
325s 
325s  |-_UNBOUND_REL_8
325s 
325s 
325s  |-_UNBOUND_REL_9
325s 
325s 
325s  |-_UNBOUND_REL_10
325s 
325s 
325s  |-_UNBOUND_REL_11
325s 
325s 
325s  |-_UNBOUND_REL_12
325s 
325s 
325s  |-_UNBOUND_REL_13
325s 
325s 
325s  |-I1
325s 
325s 
325s  |-I1
325s --->	after substitution:
325s 
325s 
325s  |-(_UNBOUND_REL_13 _UNBOUND_REL_6 _UNBOUND_REL_5 _UNBOUND_REL_4
325s        (c1 _UNBOUND_REL_6) (c1 _UNBOUND_REL_5))
325s translate_mind, evd = 
325s SHELF:
325s FUTURE GOALS STACK:
325s 
325s --->	env_params:
325s acc = 
325s def = 
325s 
325s  |-n1
325s typ = 
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s def = 
325s       p₁ := n1 : nat
325s 
325s  |-n1
325s typ = 
325s       p₁ := n1 : nat
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s 
325s  |-n1_R
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s 
325s  |-(nat_R p₁ p₂)
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-n2
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s 
325s  |-n2
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s 
325s  |-n2_R
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s 
325s  |-(nat_R q₁ q₂)
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s 
325s  |-(nat_R n₁ n₂)
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s 
325s  |-n₁
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s 
325s  |-n₂
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s 
325s  |-nat
325s acc = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s       r₂ := n₂ : nat
325s def = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s       r₂ := n₂ : nat
325s 
325s  |-n_R
325s typ = 
325s       p₁ := n1 : nat
325s       p₂ := n1 : nat
325s       p_R := n1_R : nat_R p₁ p₂
325s       q₁ := n2 : nat
325s       q₂ := n2 : nat
325s       q_R := n2_R : nat_R q₁ q₂
325s       n₁ : nat
325s       n₂ : nat
325s       n_R : nat_R n₁ n₂
325s       r₁ := n₁ : nat
325s       r₂ := n₂ : nat
325s 
325s  |-(nat_R r₁ r₂)
325s --->	arities:
325s {mind_entry_record : None
325s                                                  mind_entry_finite : Finite
325s                                                  
325s                                                  mind_entry_params : 
325s                                                  p₁ := n1 : nat
325s                                                  p₂ := n1 : nat
325s                                                  p_R := n1_R : nat_R p₁ p₂
325s                                                  q₁ := n2 : nat
325s                                                  q₂ := n2 : nat
325s                                                  q_R := n2_R : nat_R q₁ q₂
325s                                                  n₁ : nat
325s                                                  n₂ : nat
325s                                                  n_R : nat_R n₁ n₂
325s                                                  r₁ := n₁ : nat
325s                                                  r₂ := n₂ : nat
325s                                                  r_R := n_R : nat_R r₁ r₂
325s                                                  
325s                                                  mind_entry_inds : {
325s                                                  mind_entry_lc : (I1_R n₁ n₂
325s                                                  n_R (c1 n₁) (c1 n₂))
325s                                                  
325s                                                  mind_entry_consnames : I1_R_c1_R
325s                                                  
325s                                                  mind_entry_arity : (I1 n₁ ->
325s                                                  I1 n₂ -> Prop)
325s                                                  mind_entry_typename : I1_R
325s                                                  }
325s                                                  
325s                                                  mind_entry_polymorphic : false
325s                                                  mind_entry_universes : 
325s                                                  
325s                                                  mind_entry_cumulative : false
325s                                                  mind_entry_private : None
325s                                                  }
325s Prop
325s                                                  
325s --->	Translating mind body ... done.
325s evar_map inductive SHELF:
325s FUTURE GOALS STACK:
325s 
325s File "./bug3.v", line 20, characters 41-47:
325s Warning: Notation divmod is deprecated since 8.16.
325s The NPeano file is obsolete. Use Nat.divmod instead.
325s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
326s BinPosDef.Pos.sub_mask =
326s fix sub_mask (x y : positive) {struct y} : BinPosDef.Pos.mask :=
326s   match x with
326s   | (p~1)%positive =>
326s       match y with
326s       | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask p q)
326s       | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask p q)
326s       | 1%positive => BinPosDef.Pos.IsPos p~0
326s       end
326s   | (p~0)%positive =>
326s       match y with
326s       | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q)
326s       | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q)
326s       | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p)
326s       end
326s   | 1%positive =>
326s       match y with
326s       | 1%positive => BinPosDef.Pos.IsNul
326s       | _ => BinPosDef.Pos.IsNeg
326s       end
326s   end
326s with sub_mask_carry (x y : positive) {struct y} : BinPosDef.Pos.mask :=
326s   match x with
326s   | (p~1)%positive =>
326s       match y with
326s       | (q~1)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q)
326s       | (q~0)%positive => BinPosDef.Pos.double_mask (sub_mask p q)
326s       | 1%positive => BinPosDef.Pos.IsPos (BinPosDef.Pos.pred_double p)
326s       end
326s   | (p~0)%positive =>
326s       match y with
326s       | (q~1)%positive => BinPosDef.Pos.double_mask (sub_mask_carry p q)
326s       | (q~0)%positive => BinPosDef.Pos.succ_double_mask (sub_mask_carry p q)
326s       | 1%positive => BinPosDef.Pos.double_pred_mask p
326s       end
326s   | 1%positive => BinPosDef.Pos.IsNeg
326s   end
326s for
326s sub_mask
326s      : positive -> positive -> BinPosDef.Pos.mask
326s 
326s Arguments BinPosDef.Pos.sub_mask (x y)%positive_scope
326s File "./bug5.v", line 24, characters 41-47:
326s Warning: Notation divmod is deprecated since 8.16.
326s The NPeano file is obsolete. Use Nat.divmod instead.
326s [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
326s T_R =
326s fun H H0 : forall a b : nat, b <> 0 -> modS a b < b =>
326s forall (a₁ a₂ : nat) (a_R : nat_R a₁ a₂) (b₁ b₂ : nat) 
326s   (b_R : nat_R b₁ b₂) (H1 : b₁ <> 0) (H2 : b₂ <> 0),
326s not_R (eq_R nat_R b_R nat_R_O_R) H1 H2 ->
326s lt_R (modS_R a_R b_R) b_R (H a₁ b₁ H1) (H0 a₂ b₂ H2)
326s      : T -> T -> Prop
326s 'NNmod_upper_boundA_RR' is now a registered translation.
332s File "./dummyFix.v", line 6, characters 0-59:
332s Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default]
332s Inductive bool_P : bool -> Set :=
332s     bool_P_true_P : bool_P true | bool_P_false_P : bool_P false.
332s boolfun_P =
332s fun H : bool -> bool => forall H0 : bool, bool_P H0 -> bool_P (H H0)
332s      : boolfun -> Set
332s myneg_P =
332s fun (b : bool) (b_P : bool_P b) =>
332s match
332s   b_P in (bool_P b0)
332s   return (bool_P match b0 with
332s                  | true => false
332s                  | false => true
332s                  end)
332s with
332s | bool_P_true_P => bool_P_false_P
332s | bool_P_false_P => bool_P_true_P
332s end
332s      : forall b : bool, bool_P b -> bool_P (myneg b)
332s 
332s Arguments myneg_P b b_P
332s boolfun_R =
332s fun H H0 : bool -> bool =>
332s forall H1 H2 : bool, bool_R H1 H2 -> bool_R (H H1) (H0 H2)
332s      : boolfun -> boolfun -> Set
332s File "./example.v", line 64, characters 5-9:
332s Warning: Unused variable fale might be a misspelled constructor. Use _ or
332s _fale to silence this warning. [unused-pattern-matching-variable,default]
332s negb_R
332s      : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂)
332s negb_R =
332s fun (x₁ x₂ : bool) (x_R : bool_R x₁ x₂) =>
332s match
332s   x_R in (bool_R x₁0 x₂0)
332s   return
332s     (bool_R match x₁0 with
332s             | true => false
332s             | false => true
332s             end match x₂0 with
332s                 | true => false
332s                 | false => true
332s                 end)
332s with
332s | bool_R_true_R => bool_R_false_R
332s | bool_R_false_R => bool_R_true_R
332s end
332s      : forall x₁ x₂ : bool, bool_R x₁ x₂ -> bool_R (negb x₁) (negb x₂)
332s 
332s Arguments negb_R x₁ x₂ x_R
332s Type_R = fun H H0 : Type => H -> H0 -> Type
332s      : Type -> Type -> Type
332s 
332s Arguments Type_R (_ _)%type_scope
332s bool_R : Type_R bool bool
332s      : Type_R bool bool
332s boolfun_R : Type_R boolfun boolfun
332s      : Type_R boolfun boolfun
332s pType_R : pType_R pType pType
332s      : pType_R pType pType
332s arrow_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type)
332s   (B_R : B₁ -> B₂ -> Type) (H : A₁ -> B₁) (H0 : A₂ -> B₂) =>
332s forall (H1 : A₁) (H2 : A₂), A_R H1 H2 -> B_R (H H1) (H0 H2)
332s      : forall A₁ A₂ : Type,
332s        (A₁ -> A₂ -> Type) ->
332s        forall B₁ B₂ : Type,
332s        (B₁ -> B₂ -> Type) -> arrow A₁ B₁ -> arrow A₂ B₂ -> Type
332s 
332s Arguments arrow_R (A₁ A₂)%type_scope A_R%function_scope 
332s   (B₁ B₂)%type_scope B_R%function_scope _ _
332s lambda_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type)
332s   (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂)
332s   (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 
332s   (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁)
332s          (f₂ : arrow A₂ B₂),
332s        arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ ->
332s        forall (x₁ : A₁) (x₂ : A₂),
332s        A_R x₁ x₂ -> B_R (lambda A₁ B₁ f₁ x₁) (lambda A₂ B₂ f₂ x₂)
332s 
332s Arguments lambda_R (A₁ A₂)%type_scope A_R%function_scope 
332s   (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 
332s   x₁ x₂ x_R
332s application_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ B₂ : Type)
332s   (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂)
332s   (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) (x₁ : A₁) 
332s   (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (f₁ : arrow A₁ B₁)
332s          (f₂ : arrow A₂ B₂),
332s        arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂ ->
332s        forall (x₁ : A₁) (x₂ : A₂),
332s        A_R x₁ x₂ -> B_R (application A₁ B₁ f₁ x₁) (application A₂ B₂ f₂ x₂)
332s 
332s Arguments application_R (A₁ A₂)%type_scope A_R%function_scope
332s   (B₁ B₂)%type_scope B_R%function_scope f₁ f₂ f_R 
332s   x₁ x₂ x_R
332s for_all_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (B₁ : A₁ -> Type)
332s   (B₂ : A₂ -> Type)
332s   (B_R : forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type)
332s   (H : forall x : A₁, B₁ x) (H0 : forall x : A₂, B₂ x) =>
332s forall (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂), B_R x₁ x₂ x_R (H x₁) (H0 x₂)
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (B₁ : A₁ -> Type) (B₂ : A₂ -> Type),
332s        (forall (H : A₁) (H0 : A₂), A_R H H0 -> B₁ H -> B₂ H0 -> Type) ->
332s        for_all A₁ B₁ -> for_all A₂ B₂ -> Type
332s 
332s Arguments for_all_R (A₁ A₂)%type_scope (A_R B₁ B₂ B_R)%function_scope _ _
332s Inductive nat_R : nat -> nat -> Set :=
332s     nat_R_O_R : nat_R O O
332s   | nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0).
332s Inductive
332s list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type)
332s   : list A₁ -> list A₂ -> Type :=
332s     list_R_nil_R : list_R A₁ A₂ A_R (nil A₁) (nil A₂)
332s   | list_R_cons_R : forall (H : A₁) (H0 : A₂),
332s                     A_R H H0 ->
332s                     forall (H1 : list A₁) (H2 : list A₂),
332s                     list_R A₁ A₂ A_R H1 H2 ->
332s                     list_R A₁ A₂ A_R (cons A₁ H H1) (cons A₂ H0 H2).
332s 
332s Arguments list_R (A₁ A₂)%type_scope A_R%function_scope _ _
332s Arguments list_R_nil_R (A₁ A₂)%type_scope A_R%function_scope
332s Arguments list_R_cons_R (A₁ A₂)%type_scope A_R%function_scope _ _ _ _ _ _
332s length_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (l₁ : list A₁) (l₂ : list A₂),
332s        list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂)
332s length_R =
332s let fix_length_1 :=
332s   fix length (A : Type) (l : list A) {struct l} : nat :=
332s     match l with
332s     | nil _ => O
332s     | cons _ _ tl => S (length A tl)
332s     end in
332s let fix_length_2 :=
332s   fix length (A : Type) (l : list A) {struct l} : nat :=
332s     match l with
332s     | nil _ => O
332s     | cons _ _ tl => S (length A tl)
332s     end in
332s fix length_R
332s   (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 
332s   (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) {struct l_R} :
332s     nat_R (fix_length_1 A₁ l₁) (fix_length_2 A₂ l₂) :=
332s   match
332s     l_R in (list_R _ _ _ l₁0 l₂0)
332s     return (nat_R (fix_length_1 A₁ l₁0) (fix_length_2 A₂ l₂0))
332s   with
332s   | list_R_nil_R _ _ _ => nat_R_O_R
332s   | list_R_cons_R _ _ _ _ _ _ tl₁ tl₂ tl_R =>
332s       nat_R_S_R (fix_length_1 A₁ tl₁) (fix_length_2 A₂ tl₂)
332s         (length_R A₁ A₂ A_R tl₁ tl₂ tl_R)
332s   end
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (l₁ : list A₁) (l₂ : list A₂),
332s        list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length A₁ l₁) (length A₂ l₂)
332s 
332s Arguments length_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R
332s list_rec_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (P₁ : list A₁ -> Set)
332s   (P₂ : list A₂ -> Set)
332s   (P_R : forall (l₁ : list A₁) (l₂ : list A₂),
332s          list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set) =>
332s (fun (A₁0 A₂0 : Type) (A_R0 : A₁0 -> A₂0 -> Type) 
332s    (P₁0 : list A₁0 -> Type) (P₂0 : list A₂0 -> Type)
332s    (P_R0 : forall (l₁ : list A₁0) (l₂ : list A₂0),
332s            list_R A₁0 A₂0 A_R0 l₁ l₂ -> P₁0 l₁ -> P₂0 l₂ -> Type)
332s    (f₁ : P₁0 (nil A₁0)) (f₂ : P₂0 (nil A₂0))
332s    (f_R : P_R0 (nil A₁0) (nil A₂0) (list_R_nil_R A₁0 A₂0 A_R0) f₁ f₂)
332s    (f0₁ : forall (a : A₁0) (l : list A₁0), P₁0 l -> P₁0 (cons A₁0 a l))
332s    (f0₂ : forall (a : A₂0) (l : list A₂0), P₂0 l -> P₂0 (cons A₂0 a l))
332s    (f0_R : forall (a₁ : A₁0) (a₂ : A₂0) (a_R : A_R0 a₁ a₂) 
332s              (l₁ : list A₁0) (l₂ : list A₂0)
332s              (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) (H : P₁0 l₁) 
332s              (H0 : P₂0 l₂),
332s            P_R0 l₁ l₂ l_R H H0 ->
332s            P_R0 (cons A₁0 a₁ l₁) (cons A₂0 a₂ l₂)
332s              (list_R_cons_R A₁0 A₂0 A_R0 a₁ a₂ a_R l₁ l₂ l_R) 
332s              (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) =>
332s  let fix_F_1 :=
332s    fix F (l : list A₁0) : P₁0 l :=
332s      match l as l0 return (P₁0 l0) with
332s      | nil _ => f₁
332s      | cons _ y l0 => f0₁ y l0 (F l0)
332s      end in
332s  let fix_F_2 :=
332s    fix F (l : list A₂0) : P₂0 l :=
332s      match l as l0 return (P₂0 l0) with
332s      | nil _ => f₂
332s      | cons _ y l0 => f0₂ y l0 (F l0)
332s      end in
332s  fix F_R
332s    (l₁ : list A₁0) (l₂ : list A₂0) (l_R : list_R A₁0 A₂0 A_R0 l₁ l₂) {struct
332s     l_R} : P_R0 l₁ l₂ l_R (fix_F_1 l₁) (fix_F_2 l₂) :=
332s    match
332s      l_R as l_R0 in (list_R _ _ _ l₁0 l₂0)
332s      return (P_R0 l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0))
332s    with
332s    | list_R_nil_R _ _ _ => f_R
332s    | list_R_cons_R _ _ _ y₁ y₂ y_R l₁0 l₂0 l_R0 =>
332s        f0_R y₁ y₂ y_R l₁0 l₂0 l_R0 (fix_F_1 l₁0) (fix_F_2 l₂0)
332s          (F_R l₁0 l₂0 l_R0)
332s    end) A₁ A₂ A_R P₁ P₂ P_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (P₁ : list A₁ -> Set) (P₂ : list A₂ -> Set)
332s          (P_R : forall (l₁ : list A₁) (l₂ : list A₂),
332s                 list_R A₁ A₂ A_R l₁ l₂ -> P₁ l₁ -> P₂ l₂ -> Set)
332s          (f₁ : P₁ (nil A₁)) (f₂ : P₂ (nil A₂)),
332s        P_R (nil A₁) (nil A₂) (list_R_nil_R A₁ A₂ A_R) f₁ f₂ ->
332s        forall (f0₁ : forall (a : A₁) (l : list A₁), P₁ l -> P₁ (cons A₁ a l))
332s          (f0₂ : forall (a : A₂) (l : list A₂), P₂ l -> P₂ (cons A₂ a l)),
332s        (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂) 
332s           (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂)
332s           (H : P₁ l₁) (H0 : P₂ l₂),
332s         P_R l₁ l₂ l_R H H0 ->
332s         P_R (cons A₁ a₁ l₁) (cons A₂ a₂ l₂)
332s           (list_R_cons_R A₁ A₂ A_R a₁ a₂ a_R l₁ l₂ l_R) 
332s           (f0₁ a₁ l₁ H) (f0₂ a₂ l₂ H0)) ->
332s        forall (l₁ : list A₁) (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂),
332s        P_R l₁ l₂ l_R (list_rec A₁ P₁ f₁ f0₁ l₁) (list_rec A₂ P₂ f₂ f0₂ l₂)
332s 
332s Arguments list_rec_R (A₁ A₂)%type_scope (A_R P₁ P₂ P_R)%function_scope 
332s   f₁ f₂ f_R (f0₁ f0₂ f0_R)%function_scope l₁ l₂ l_R
332s length2_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (l₁ : list A₁) (l₂ : list A₂),
332s        list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂)
332s length2_R =
332s fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (l₁ : list A₁) 
332s   (l₂ : list A₂) (l_R : list_R A₁ A₂ A_R l₁ l₂) =>
332s list_rec_R A₁ A₂ A_R (fun _ : list A₁ => nat) (fun _ : list A₂ => nat)
332s   (fun (l₁0 : list A₁) (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) =>
332s    nat_R) O O nat_R_O_R (fun (_ : A₁) (_ : list A₁) => S)
332s   (fun (_ : A₂) (_ : list A₂) => S)
332s   (fun (a₁ : A₁) (a₂ : A₂) (_ : A_R a₁ a₂) (l₁0 : list A₁) 
332s      (l₂0 : list A₂) (_ : list_R A₁ A₂ A_R l₁0 l₂0) => nat_R_S_R) l₁ l₂ l_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (l₁ : list A₁) (l₂ : list A₂),
332s        list_R A₁ A₂ A_R l₁ l₂ -> nat_R (length2 A₁ l₁) (length2 A₂ l₂)
332s 
332s Arguments length2_R (A₁ A₂)%type_scope A_R%function_scope l₁ l₂ l_R
332s sum_rect =
332s fun (A B : Type) (P : A + B -> Type) (f : forall a : A, P (inl a))
332s   (f0 : forall b : B, P (inr b)) (s : A + B) =>
332s match s as s0 return (P s0) with
332s | inl a => f a
332s | inr b => f0 b
332s end
332s      : forall (A B : Type) (P : A + B -> Type),
332s        (forall a : A, P (inl a)) ->
332s        (forall b : B, P (inr b)) -> forall s : A + B, P s
332s 
332s Arguments sum_rect [A B]%type_scope (P f f0)%function_scope s
332s sum_rect
332s      : forall (A B : Type) (P : A + B -> Type),
332s        (forall a : A, P (inl a)) ->
332s        (forall b : B, P (inr b)) -> forall s : A + B, P s
332s sum_rect_R
332s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
332s          (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) (P₁ : A₁ + B₁ -> Type)
332s          (P₂ : A₂ + B₂ -> Type)
332s          (P_R : forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂),
332s                 sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂ -> P₁ s₁ -> P₂ s₂ -> Type)
332s          (f₁ : forall a : A₁, P₁ (inl a)) (f₂ : forall a : A₂, P₂ (inl a)),
332s        (forall (a₁ : A₁) (a₂ : A₂) (a_R : A_R a₁ a₂),
332s         P_R (inl a₁) (inl a₂) (sum_R_inl_R A₁ A₂ A_R B₁ B₂ B_R a₁ a₂ a_R)
332s           (f₁ a₁) (f₂ a₂)) ->
332s        forall (f0₁ : forall b : B₁, P₁ (inr b))
332s          (f0₂ : forall b : B₂, P₂ (inr b)),
332s        (forall (b₁ : B₁) (b₂ : B₂) (b_R : B_R b₁ b₂),
332s         P_R (inr b₁) (inr b₂) (sum_R_inr_R A₁ A₂ A_R B₁ B₂ B_R b₁ b₂ b_R)
332s           (f0₁ b₁) (f0₂ b₂)) ->
332s        forall (s₁ : A₁ + B₁) (s₂ : A₂ + B₂)
332s          (s_R : sum_R A₁ A₂ A_R B₁ B₂ B_R s₁ s₂),
332s        P_R s₁ s₂ s_R (sum_rect P₁ f₁ f0₁ s₁) (sum_rect P₂ f₂ f0₂ s₂)
333s rev_R
333s      : forall (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
333s          (l₁ : list A₁) (l₂ : list A₂),
333s        list_R A₁ A₂ A_R l₁ l₂ -> list_R A₁ A₂ A_R (List.rev l₁) (List.rev l₂)
333s Module A_R := Struct Definition t_R : A.t -> A.t -> Set. Module B_R End
333s 
333s Module A_R.B_R := Struct Definition t_R : A.B.t -> A.B.t -> Set. End
333s 
333s Inductive
333s nat_R_10
333s     : nat ->
333s       nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Set :=
333s     nat_R_10_O_R_10 : nat_R_10 0 0 0 0 0 0 0 0 0 0
333s   | nat_R_10_S_R_10 : forall H H0 H1 H2 H3 H4 H5 H6 H7 H8 : nat,
333s                       nat_R_10 H H0 H1 H2 H3 H4 H5 H6 H7 H8 ->
333s                       nat_R_10 (S H) (S H0) (S H1) 
333s                         (S H2) (S H3) (S H4) (S H5) 
333s                         (S H6) (S H7) (S H8).
333s 
333s Arguments nat_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope
333s Arguments nat_R_10_S_R_10 (_ _ _ _ _ _ _ _ _ _)%nat_scope _
333s 'A_R' is now a registered translation.
333s      = opaque
333s      : True
333s      = opaque_R
333s      : True_R opaque opaque
333s autopkgtest [21:01:09]: test upstreamtestsuite: -----------------------]
334s autopkgtest [21:01:10]: test upstreamtestsuite:  - - - - - - - - - - results - - - - - - - - - -
334s upstreamtestsuite    PASS
334s autopkgtest [21:01:10]: @@@@@@@@@@@@@@@@@@@@ summary
334s upstreamtestsuite    PASS
346s Creating nova instance adt-noble-s390x-paramcoq-20240325-205536-juju-7f2275-prod-proposed-migration-environment-2 from image adt/ubuntu-noble-s390x-server-20240325.img (UUID 9f25d9bc-613c-4979-9452-2ea8e4d84cd0)...