I: pbuilder: network access will be disabled during build
I: Current time: Sun Apr 16 11:18:33 -12 2023
I: pbuilder-time-stamp: 1681687113
I: Building the build Environment
I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz]
I: copying local configuration
W: --override-config is not set; not updating apt.conf Read the manpage for details.
I: mounting /proc filesystem
I: mounting /sys filesystem
I: creating /{dev,run}/shm
I: mounting /dev/pts filesystem
I: redirecting /dev/ptmx to /dev/pts/ptmx
I: policy-rc.d already exists
I: using eatmydata during job
I: Copying source file
I: copying [minlog_4.0.99.20100221-7.dsc]
I: copying [./minlog_4.0.99.20100221.orig.tar.gz]
I: copying [./minlog_4.0.99.20100221-7.debian.tar.xz]
I: Extracting source
gpgv: Signature made Thu Dec 31 11:07:33 2020 -12
gpgv: using EDDSA key 658073613BFCC5C7E2E45D45DC518FC87F9716AA
gpgv: issuer "vagrant@reproducible-builds.org"
gpgv: Can't check signature: No public key
dpkg-source: warning: cannot verify inline signature for ./minlog_4.0.99.20100221-7.dsc: no acceptable signature found
dpkg-source: info: extracting minlog in minlog-4.0.99.20100221
dpkg-source: info: unpacking minlog_4.0.99.20100221.orig.tar.gz
dpkg-source: info: unpacking minlog_4.0.99.20100221-7.debian.tar.xz
I: Not using root during the build.
I: Installing the build-deps
I: user script /srv/workspace/pbuilder/7405/tmp/hooks/D02_print_environment starting
I: set
BUILDDIR='/build'
BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other'
BUILDUSERNAME='pbuilder1'
BUILD_ARCH='i386'
DEBIAN_FRONTEND='noninteractive'
DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=8'
DISTRIBUTION='bookworm'
HOME='/root'
HOST_ARCH='i386'
IFS='
'
INVOCATION_ID='dce4f489a4394253902b515c7b271863'
LANG='C'
LANGUAGE='en_US:en'
LC_ALL='C'
LD_LIBRARY_PATH='/usr/lib/libeatmydata'
LD_PRELOAD='libeatmydata.so'
MAIL='/var/mail/root'
OPTIND='1'
PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games'
PBCURRENTCOMMANDLINEOPERATION='build'
PBUILDER_OPERATION='build'
PBUILDER_PKGDATADIR='/usr/share/pbuilder'
PBUILDER_PKGLIBDIR='/usr/lib/pbuilder'
PBUILDER_SYSCONFDIR='/etc'
PPID='7405'
PS1='# '
PS2='> '
PS4='+ '
PWD='/'
SHELL='/bin/bash'
SHLVL='2'
SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.3CMdEpet/pbuilderrc_xNNg --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.3CMdEpet/b1 --logfile b1/build.log minlog_4.0.99.20100221-7.dsc'
SUDO_GID='112'
SUDO_UID='107'
SUDO_USER='jenkins'
TERM='unknown'
TZ='/usr/share/zoneinfo/Etc/GMT+12'
USER='root'
_='/usr/bin/systemd-run'
http_proxy='http://78.137.99.97:3128'
I: uname -a
Linux ionos2-i386 5.10.0-21-686-pae #1 SMP Debian 5.10.162-1 (2023-01-21) i686 GNU/Linux
I: ls -l /bin
total 6036
-rwxr-xr-x 1 root root 1408088 Feb 12 08:21 bash
-rwxr-xr-x 3 root root 38404 Sep 18 2022 bunzip2
-rwxr-xr-x 3 root root 38404 Sep 18 2022 bzcat
lrwxrwxrwx 1 root root 6 Sep 18 2022 bzcmp -> bzdiff
-rwxr-xr-x 1 root root 2225 Sep 18 2022 bzdiff
lrwxrwxrwx 1 root root 6 Sep 18 2022 bzegrep -> bzgrep
-rwxr-xr-x 1 root root 4893 Nov 27 2021 bzexe
lrwxrwxrwx 1 root root 6 Sep 18 2022 bzfgrep -> bzgrep
-rwxr-xr-x 1 root root 3775 Sep 18 2022 bzgrep
-rwxr-xr-x 3 root root 38404 Sep 18 2022 bzip2
-rwxr-xr-x 1 root root 17892 Sep 18 2022 bzip2recover
lrwxrwxrwx 1 root root 6 Sep 18 2022 bzless -> bzmore
-rwxr-xr-x 1 root root 1297 Sep 18 2022 bzmore
-rwxr-xr-x 1 root root 42920 Sep 20 2022 cat
-rwxr-xr-x 1 root root 79816 Sep 20 2022 chgrp
-rwxr-xr-x 1 root root 67496 Sep 20 2022 chmod
-rwxr-xr-x 1 root root 79816 Sep 20 2022 chown
-rwxr-xr-x 1 root root 162024 Sep 20 2022 cp
-rwxr-xr-x 1 root root 136916 Jan 5 01:20 dash
-rwxr-xr-x 1 root root 137160 Sep 20 2022 date
-rwxr-xr-x 1 root root 100364 Sep 20 2022 dd
-rwxr-xr-x 1 root root 108940 Sep 20 2022 df
-rwxr-xr-x 1 root root 162152 Sep 20 2022 dir
-rwxr-xr-x 1 root root 87760 Mar 22 22:20 dmesg
lrwxrwxrwx 1 root root 8 Dec 19 01:33 dnsdomainname -> hostname
lrwxrwxrwx 1 root root 8 Dec 19 01:33 domainname -> hostname
-rwxr-xr-x 1 root root 38760 Sep 20 2022 echo
-rwxr-xr-x 1 root root 41 Jan 24 02:43 egrep
-rwxr-xr-x 1 root root 34664 Sep 20 2022 false
-rwxr-xr-x 1 root root 41 Jan 24 02:43 fgrep
-rwxr-xr-x 1 root root 84272 Mar 22 22:20 findmnt
-rwsr-xr-x 1 root root 30240 Mar 22 20:38 fusermount
-rwxr-xr-x 1 root root 218680 Jan 24 02:43 grep
-rwxr-xr-x 2 root root 2346 Apr 9 2022 gunzip
-rwxr-xr-x 1 root root 6447 Apr 9 2022 gzexe
-rwxr-xr-x 1 root root 100952 Apr 9 2022 gzip
-rwxr-xr-x 1 root root 21916 Dec 19 01:33 hostname
-rwxr-xr-x 1 root root 75756 Sep 20 2022 ln
-rwxr-xr-x 1 root root 55600 Mar 22 23:43 login
-rwxr-xr-x 1 root root 162152 Sep 20 2022 ls
-rwxr-xr-x 1 root root 214568 Mar 22 22:20 lsblk
-rwxr-xr-x 1 root root 96328 Sep 20 2022 mkdir
-rwxr-xr-x 1 root root 84008 Sep 20 2022 mknod
-rwxr-xr-x 1 root root 38792 Sep 20 2022 mktemp
-rwxr-xr-x 1 root root 63016 Mar 22 22:20 more
-rwsr-xr-x 1 root root 58912 Mar 22 22:20 mount
-rwxr-xr-x 1 root root 13856 Mar 22 22:20 mountpoint
-rwxr-xr-x 1 root root 157932 Sep 20 2022 mv
lrwxrwxrwx 1 root root 8 Dec 19 01:33 nisdomainname -> hostname
lrwxrwxrwx 1 root root 14 Apr 2 18:25 pidof -> /sbin/killall5
-rwxr-xr-x 1 root root 38792 Sep 20 2022 pwd
lrwxrwxrwx 1 root root 4 Feb 12 08:21 rbash -> bash
-rwxr-xr-x 1 root root 51080 Sep 20 2022 readlink
-rwxr-xr-x 1 root root 75720 Sep 20 2022 rm
-rwxr-xr-x 1 root root 51080 Sep 20 2022 rmdir
-rwxr-xr-x 1 root root 22308 Nov 2 04:31 run-parts
-rwxr-xr-x 1 root root 133224 Jan 5 07:55 sed
lrwxrwxrwx 1 root root 4 Jan 5 01:20 sh -> dash
-rwxr-xr-x 1 root root 38760 Sep 20 2022 sleep
-rwxr-xr-x 1 root root 87976 Sep 20 2022 stty
-rwsr-xr-x 1 root root 83492 Mar 22 22:20 su
-rwxr-xr-x 1 root root 38792 Sep 20 2022 sync
-rwxr-xr-x 1 root root 598456 Apr 6 02:25 tar
-rwxr-xr-x 1 root root 13860 Nov 2 04:31 tempfile
-rwxr-xr-x 1 root root 120776 Sep 20 2022 touch
-rwxr-xr-x 1 root root 34664 Sep 20 2022 true
-rwxr-xr-x 1 root root 17892 Mar 22 20:38 ulockmgr_server
-rwsr-xr-x 1 root root 30236 Mar 22 22:20 umount
-rwxr-xr-x 1 root root 38760 Sep 20 2022 uname
-rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress
-rwxr-xr-x 1 root root 162152 Sep 20 2022 vdir
-rwxr-xr-x 1 root root 71216 Mar 22 22:20 wdctl
lrwxrwxrwx 1 root root 8 Dec 19 01:33 ypdomainname -> hostname
-rwxr-xr-x 1 root root 1984 Apr 9 2022 zcat
-rwxr-xr-x 1 root root 1678 Apr 9 2022 zcmp
-rwxr-xr-x 1 root root 6460 Apr 9 2022 zdiff
-rwxr-xr-x 1 root root 29 Apr 9 2022 zegrep
-rwxr-xr-x 1 root root 29 Apr 9 2022 zfgrep
-rwxr-xr-x 1 root root 2081 Apr 9 2022 zforce
-rwxr-xr-x 1 root root 8103 Apr 9 2022 zgrep
-rwxr-xr-x 1 root root 2206 Apr 9 2022 zless
-rwxr-xr-x 1 root root 1842 Apr 9 2022 zmore
-rwxr-xr-x 1 root root 4577 Apr 9 2022 znew
I: user script /srv/workspace/pbuilder/7405/tmp/hooks/D02_print_environment finished
-> Attempting to satisfy build-dependencies
-> Creating pbuilder-satisfydepends-dummy package
Package: pbuilder-satisfydepends-dummy
Version: 0.invalid.0
Architecture: i386
Maintainer: Debian Pbuilder Team <pbuilder-maint@lists.alioth.debian.org>
Description: Dummy package to satisfy dependencies with aptitude - created by pbuilder
This package was created automatically by pbuilder to satisfy the
build-dependencies of the package being currently built.
Depends: debhelper-compat (= 13), racket, texlive (>= 2007-11)
dpkg-deb: building package 'pbuilder-satisfydepends-dummy' in '/tmp/satisfydepends-aptitude/pbuilder-satisfydepends-dummy.deb'.
Selecting previously unselected package pbuilder-satisfydepends-dummy.
(Reading database ... 19604 files and directories currently installed.)
Preparing to unpack .../pbuilder-satisfydepends-dummy.deb ...
Unpacking pbuilder-satisfydepends-dummy (0.invalid.0) ...
dpkg: pbuilder-satisfydepends-dummy: dependency problems, but configuring anyway as you requested:
pbuilder-satisfydepends-dummy depends on debhelper-compat (= 13); however:
Package debhelper-compat is not installed.
pbuilder-satisfydepends-dummy depends on racket; however:
Package racket is not installed.
pbuilder-satisfydepends-dummy depends on texlive (>= 2007-11); however:
Package texlive is not installed.
Setting up pbuilder-satisfydepends-dummy (0.invalid.0) ...
Reading package lists...
Building dependency tree...
Reading state information...
Initializing package states...
Writing extended state information...
Building tag database...
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
The following NEW packages will be installed:
autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} debhelper{a} dh-autoreconf{a} dh-strip-nondeterminism{a} dwz{a} file{a} fontconfig-config{a} fonts-dejavu-core{a} fonts-lmodern{a} gettext{a} gettext-base{a} groff-base{a} intltool-debian{a} isa-support{a} libarchive-zip-perl{a} libbrotli1{a} libbsd0{a} libcairo2{a} libdebhelper-perl{a} libelf1{a} libexpat1{a} libfile-stripnondeterminism-perl{a} libfontconfig1{a} libfreetype6{a} libglib2.0-0{a} libgraphite2-3{a} libharfbuzz0b{a} libice6{a} libicu72{a} libkpathsea6{a} libmagic-mgc{a} libmagic1{a} libpaper-utils{a} libpaper1{a} libpipeline1{a} libpixman-1-0{a} libpng16-16{a} libptexenc1{a} libsm6{a} libsub-override-perl{a} libsynctex2{a} libteckit0{a} libtexlua53-5{a} libtexluajit2{a} libtool{a} libuchardet0{a} libx11-6{a} libx11-data{a} libxau6{a} libxaw7{a} libxcb-render0{a} libxcb-shm0{a} libxcb1{a} libxdmcp6{a} libxext6{a} libxi6{a} libxml2{a} libxmu6{a} libxpm4{a} libxrender1{a} libxt6{a} libzzip-0-13{a} m4{a} man-db{a} po-debconf{a} racket{a} racket-common{a} sensible-utils{a} sse2-support{a} t1utils{a} tex-common{a} texlive{a} texlive-base{a} texlive-binaries{a} texlive-fonts-recommended{a} texlive-latex-base{a} texlive-latex-recommended{a} ucf{a} x11-common{a} xdg-utils{a}
The following packages are RECOMMENDED but will NOT be installed:
curl dvisvgm libarchive-cpio-perl libfile-mimeinfo-perl libgdk-pixbuf2.0-0 libglib2.0-data libgtk2.0-0 libjpeg62-turbo libltdl-dev libmail-sendmail-perl libnet-dbus-perl libpangocairo-1.0-0 libx11-protocol-perl lmodern lynx racket-doc shared-mime-info tex-gyre tipa wget x11-utils x11-xserver-utils xdg-user-dirs
0 packages upgraded, 84 newly installed, 0 to remove and 0 not upgraded.
Need to get 193 MB of archives. After unpacking 641 MB will be used.
Writing extended state information...
Get: 1 http://deb.debian.org/debian bookworm/main i386 isa-support i386 15 [9692 B]
Get: 2 http://deb.debian.org/debian bookworm/main i386 sse2-support i386 15 [3320 B]
Get: 3 http://deb.debian.org/debian bookworm/main i386 sensible-utils all 0.0.17+nmu1 [19.0 kB]
Get: 4 http://deb.debian.org/debian bookworm/main i386 libmagic-mgc i386 1:5.44-3 [305 kB]
Get: 5 http://deb.debian.org/debian bookworm/main i386 libmagic1 i386 1:5.44-3 [114 kB]
Get: 6 http://deb.debian.org/debian bookworm/main i386 file i386 1:5.44-3 [42.5 kB]
Get: 7 http://deb.debian.org/debian bookworm/main i386 gettext-base i386 0.21-12 [162 kB]
Get: 8 http://deb.debian.org/debian bookworm/main i386 libuchardet0 i386 0.0.7-1 [67.9 kB]
Get: 9 http://deb.debian.org/debian bookworm/main i386 groff-base i386 1.22.4-10 [932 kB]
Get: 10 http://deb.debian.org/debian bookworm/main i386 bsdextrautils i386 2.38.1-5+b1 [90.3 kB]
Get: 11 http://deb.debian.org/debian bookworm/main i386 libpipeline1 i386 1.5.7-1 [40.0 kB]
Get: 12 http://deb.debian.org/debian bookworm/main i386 man-db i386 2.11.2-2 [1397 kB]
Get: 13 http://deb.debian.org/debian bookworm/main i386 ucf all 3.0043+nmu1 [55.2 kB]
Get: 14 http://deb.debian.org/debian bookworm/main i386 m4 i386 1.4.19-3 [294 kB]
Get: 15 http://deb.debian.org/debian bookworm/main i386 autoconf all 2.71-3 [332 kB]
Get: 16 http://deb.debian.org/debian bookworm/main i386 autotools-dev all 20220109.1 [51.6 kB]
Get: 17 http://deb.debian.org/debian bookworm/main i386 automake all 1:1.16.5-1.3 [823 kB]
Get: 18 http://deb.debian.org/debian bookworm/main i386 autopoint all 0.21-12 [495 kB]
Get: 19 http://deb.debian.org/debian bookworm/main i386 libdebhelper-perl all 13.11.4 [81.2 kB]
Get: 20 http://deb.debian.org/debian bookworm/main i386 libtool all 2.4.7-5 [517 kB]
Get: 21 http://deb.debian.org/debian bookworm/main i386 dh-autoreconf all 20 [17.1 kB]
Get: 22 http://deb.debian.org/debian bookworm/main i386 libarchive-zip-perl all 1.68-1 [104 kB]
Get: 23 http://deb.debian.org/debian bookworm/main i386 libsub-override-perl all 0.09-4 [9304 B]
Get: 24 http://deb.debian.org/debian bookworm/main i386 libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB]
Get: 25 http://deb.debian.org/debian bookworm/main i386 dh-strip-nondeterminism all 1.13.1-1 [8620 B]
Get: 26 http://deb.debian.org/debian bookworm/main i386 libelf1 i386 0.188-2.1 [179 kB]
Get: 27 http://deb.debian.org/debian bookworm/main i386 dwz i386 0.15-1 [118 kB]
Get: 28 http://deb.debian.org/debian bookworm/main i386 libicu72 i386 72.1-3 [9541 kB]
Get: 29 http://deb.debian.org/debian bookworm/main i386 libxml2 i386 2.9.14+dfsg-1.1+b3 [720 kB]
Get: 30 http://deb.debian.org/debian bookworm/main i386 gettext i386 0.21-12 [1311 kB]
Get: 31 http://deb.debian.org/debian bookworm/main i386 intltool-debian all 0.35.0+20060710.6 [22.9 kB]
Get: 32 http://deb.debian.org/debian bookworm/main i386 po-debconf all 1.0.21+nmu1 [248 kB]
Get: 33 http://deb.debian.org/debian bookworm/main i386 debhelper all 13.11.4 [942 kB]
Get: 34 http://deb.debian.org/debian bookworm/main i386 fonts-dejavu-core all 2.37-6 [1068 kB]
Get: 35 http://deb.debian.org/debian bookworm/main i386 fontconfig-config i386 2.14.1-4 [315 kB]
Get: 36 http://deb.debian.org/debian bookworm/main i386 fonts-lmodern all 2.005-1 [4540 kB]
Get: 37 http://deb.debian.org/debian bookworm/main i386 libbrotli1 i386 1.0.9-2+b6 [275 kB]
Get: 38 http://deb.debian.org/debian bookworm/main i386 libbsd0 i386 0.11.7-2 [121 kB]
Get: 39 http://deb.debian.org/debian bookworm/main i386 libexpat1 i386 2.5.0-1 [103 kB]
Get: 40 http://deb.debian.org/debian bookworm/main i386 libpng16-16 i386 1.6.39-2 [283 kB]
Get: 41 http://deb.debian.org/debian bookworm/main i386 libfreetype6 i386 2.12.1+dfsg-4 [410 kB]
Get: 42 http://deb.debian.org/debian bookworm/main i386 libfontconfig1 i386 2.14.1-4 [398 kB]
Get: 43 http://deb.debian.org/debian bookworm/main i386 libpixman-1-0 i386 0.42.2-1 [548 kB]
Get: 44 http://deb.debian.org/debian bookworm/main i386 libxau6 i386 1:1.0.9-1 [20.0 kB]
Get: 45 http://deb.debian.org/debian bookworm/main i386 libxdmcp6 i386 1:1.1.2-3 [26.7 kB]
Get: 46 http://deb.debian.org/debian bookworm/main i386 libxcb1 i386 1.15-1 [148 kB]
Get: 47 http://deb.debian.org/debian bookworm/main i386 libx11-data all 2:1.8.4-2 [292 kB]
Get: 48 http://deb.debian.org/debian bookworm/main i386 libx11-6 i386 2:1.8.4-2 [782 kB]
Get: 49 http://deb.debian.org/debian bookworm/main i386 libxcb-render0 i386 1.15-1 [116 kB]
Get: 50 http://deb.debian.org/debian bookworm/main i386 libxcb-shm0 i386 1.15-1 [106 kB]
Get: 51 http://deb.debian.org/debian bookworm/main i386 libxext6 i386 2:1.3.4-1+b1 [55.3 kB]
Get: 52 http://deb.debian.org/debian bookworm/main i386 libxrender1 i386 1:0.9.10-1.1 [34.1 kB]
Get: 53 http://deb.debian.org/debian bookworm/main i386 libcairo2 i386 1.16.0-7 [627 kB]
Get: 54 http://deb.debian.org/debian bookworm/main i386 libglib2.0-0 i386 2.74.6-1 [1467 kB]
Get: 55 http://deb.debian.org/debian bookworm/main i386 libgraphite2-3 i386 1.3.14-1 [84.0 kB]
Get: 56 http://deb.debian.org/debian bookworm/main i386 libharfbuzz0b i386 6.0.0+dfsg-3 [1966 kB]
Get: 57 http://deb.debian.org/debian bookworm/main i386 x11-common all 1:7.7+23 [252 kB]
Get: 58 http://deb.debian.org/debian bookworm/main i386 libice6 i386 2:1.0.10-1 [60.8 kB]
Get: 59 http://deb.debian.org/debian bookworm/main i386 libkpathsea6 i386 2022.20220321.62855-5 [155 kB]
Get: 60 http://deb.debian.org/debian bookworm/main i386 libpaper1 i386 1.1.29 [12.7 kB]
Get: 61 http://deb.debian.org/debian bookworm/main i386 libpaper-utils i386 1.1.29 [8972 B]
Get: 62 http://deb.debian.org/debian bookworm/main i386 libptexenc1 i386 2022.20220321.62855-5 [44.6 kB]
Get: 63 http://deb.debian.org/debian bookworm/main i386 libsm6 i386 2:1.2.3-1 [35.7 kB]
Get: 64 http://deb.debian.org/debian bookworm/main i386 libsynctex2 i386 2022.20220321.62855-5 [62.2 kB]
Get: 65 http://deb.debian.org/debian bookworm/main i386 libteckit0 i386 2.5.11+ds1-1+b1 [282 kB]
Get: 66 http://deb.debian.org/debian bookworm/main i386 libtexlua53-5 i386 2022.20220321.62855-5 [126 kB]
Get: 67 http://deb.debian.org/debian bookworm/main i386 libtexluajit2 i386 2022.20220321.62855-5 [262 kB]
Get: 68 http://deb.debian.org/debian bookworm/main i386 libxt6 i386 1:1.2.1-1.1 [192 kB]
Get: 69 http://deb.debian.org/debian bookworm/main i386 libxmu6 i386 2:1.1.3-3 [62.5 kB]
Get: 70 http://deb.debian.org/debian bookworm/main i386 libxpm4 i386 1:3.5.12-1.1 [50.0 kB]
Get: 71 http://deb.debian.org/debian bookworm/main i386 libxaw7 i386 2:1.0.14-1 [209 kB]
Get: 72 http://deb.debian.org/debian bookworm/main i386 libxi6 i386 2:1.8-1+b1 [86.2 kB]
Get: 73 http://deb.debian.org/debian bookworm/main i386 libzzip-0-13 i386 0.13.72+dfsg.1-1.1 [60.1 kB]
Get: 74 http://deb.debian.org/debian bookworm/main i386 racket-common all 8.7+dfsg1-1 [14.9 MB]
Get: 75 http://deb.debian.org/debian bookworm/main i386 racket i386 8.7+dfsg1-1 [95.3 MB]
Get: 76 http://deb.debian.org/debian bookworm/main i386 t1utils i386 1.41-4 [62.3 kB]
Get: 77 http://deb.debian.org/debian bookworm/main i386 tex-common all 6.18 [32.5 kB]
Get: 78 http://deb.debian.org/debian bookworm/main i386 texlive-binaries i386 2022.20220321.62855-5 [10.6 MB]
Get: 79 http://deb.debian.org/debian bookworm/main i386 xdg-utils all 1.1.3-4.1 [75.5 kB]
Get: 80 http://deb.debian.org/debian bookworm/main i386 texlive-base all 2022.20230122-3 [21.9 MB]
Get: 81 http://deb.debian.org/debian bookworm/main i386 texlive-fonts-recommended all 2022.20230122-3 [4988 kB]
Get: 82 http://deb.debian.org/debian bookworm/main i386 texlive-latex-base all 2022.20230122-3 [1182 kB]
Get: 83 http://deb.debian.org/debian bookworm/main i386 texlive-latex-recommended all 2022.20230122-3 [8880 kB]
Get: 84 http://deb.debian.org/debian bookworm/main i386 texlive all 2022.20230122-3 [18.2 kB]
Fetched 193 MB in 6s (33.1 MB/s)
debconf: delaying package configuration, since apt-utils is not installed
Selecting previously unselected package isa-support:i386.
(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 ... 19604 files and directories currently installed.)
Preparing to unpack .../isa-support_15_i386.deb ...
Unpacking isa-support:i386 (15) ...
Setting up isa-support:i386 (15) ...
Selecting previously unselected package sse2-support.
(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 ... 19622 files and directories currently installed.)
Preparing to unpack .../00-sse2-support_15_i386.deb ...
Unpacking sse2-support (15) ...
Selecting previously unselected package sensible-utils.
Preparing to unpack .../01-sensible-utils_0.0.17+nmu1_all.deb ...
Unpacking sensible-utils (0.0.17+nmu1) ...
Selecting previously unselected package libmagic-mgc.
Preparing to unpack .../02-libmagic-mgc_1%3a5.44-3_i386.deb ...
Unpacking libmagic-mgc (1:5.44-3) ...
Selecting previously unselected package libmagic1:i386.
Preparing to unpack .../03-libmagic1_1%3a5.44-3_i386.deb ...
Unpacking libmagic1:i386 (1:5.44-3) ...
Selecting previously unselected package file.
Preparing to unpack .../04-file_1%3a5.44-3_i386.deb ...
Unpacking file (1:5.44-3) ...
Selecting previously unselected package gettext-base.
Preparing to unpack .../05-gettext-base_0.21-12_i386.deb ...
Unpacking gettext-base (0.21-12) ...
Selecting previously unselected package libuchardet0:i386.
Preparing to unpack .../06-libuchardet0_0.0.7-1_i386.deb ...
Unpacking libuchardet0:i386 (0.0.7-1) ...
Selecting previously unselected package groff-base.
Preparing to unpack .../07-groff-base_1.22.4-10_i386.deb ...
Unpacking groff-base (1.22.4-10) ...
Selecting previously unselected package bsdextrautils.
Preparing to unpack .../08-bsdextrautils_2.38.1-5+b1_i386.deb ...
Unpacking bsdextrautils (2.38.1-5+b1) ...
Selecting previously unselected package libpipeline1:i386.
Preparing to unpack .../09-libpipeline1_1.5.7-1_i386.deb ...
Unpacking libpipeline1:i386 (1.5.7-1) ...
Selecting previously unselected package man-db.
Preparing to unpack .../10-man-db_2.11.2-2_i386.deb ...
Unpacking man-db (2.11.2-2) ...
Selecting previously unselected package ucf.
Preparing to unpack .../11-ucf_3.0043+nmu1_all.deb ...
Moving old data out of the way
Unpacking ucf (3.0043+nmu1) ...
Selecting previously unselected package m4.
Preparing to unpack .../12-m4_1.4.19-3_i386.deb ...
Unpacking m4 (1.4.19-3) ...
Selecting previously unselected package autoconf.
Preparing to unpack .../13-autoconf_2.71-3_all.deb ...
Unpacking autoconf (2.71-3) ...
Selecting previously unselected package autotools-dev.
Preparing to unpack .../14-autotools-dev_20220109.1_all.deb ...
Unpacking autotools-dev (20220109.1) ...
Selecting previously unselected package automake.
Preparing to unpack .../15-automake_1%3a1.16.5-1.3_all.deb ...
Unpacking automake (1:1.16.5-1.3) ...
Selecting previously unselected package autopoint.
Preparing to unpack .../16-autopoint_0.21-12_all.deb ...
Unpacking autopoint (0.21-12) ...
Selecting previously unselected package libdebhelper-perl.
Preparing to unpack .../17-libdebhelper-perl_13.11.4_all.deb ...
Unpacking libdebhelper-perl (13.11.4) ...
Selecting previously unselected package libtool.
Preparing to unpack .../18-libtool_2.4.7-5_all.deb ...
Unpacking libtool (2.4.7-5) ...
Selecting previously unselected package dh-autoreconf.
Preparing to unpack .../19-dh-autoreconf_20_all.deb ...
Unpacking dh-autoreconf (20) ...
Selecting previously unselected package libarchive-zip-perl.
Preparing to unpack .../20-libarchive-zip-perl_1.68-1_all.deb ...
Unpacking libarchive-zip-perl (1.68-1) ...
Selecting previously unselected package libsub-override-perl.
Preparing to unpack .../21-libsub-override-perl_0.09-4_all.deb ...
Unpacking libsub-override-perl (0.09-4) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../22-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../23-dh-strip-nondeterminism_1.13.1-1_all.deb ...
Unpacking dh-strip-nondeterminism (1.13.1-1) ...
Selecting previously unselected package libelf1:i386.
Preparing to unpack .../24-libelf1_0.188-2.1_i386.deb ...
Unpacking libelf1:i386 (0.188-2.1) ...
Selecting previously unselected package dwz.
Preparing to unpack .../25-dwz_0.15-1_i386.deb ...
Unpacking dwz (0.15-1) ...
Selecting previously unselected package libicu72:i386.
Preparing to unpack .../26-libicu72_72.1-3_i386.deb ...
Unpacking libicu72:i386 (72.1-3) ...
Selecting previously unselected package libxml2:i386.
Preparing to unpack .../27-libxml2_2.9.14+dfsg-1.1+b3_i386.deb ...
Unpacking libxml2:i386 (2.9.14+dfsg-1.1+b3) ...
Selecting previously unselected package gettext.
Preparing to unpack .../28-gettext_0.21-12_i386.deb ...
Unpacking gettext (0.21-12) ...
Selecting previously unselected package intltool-debian.
Preparing to unpack .../29-intltool-debian_0.35.0+20060710.6_all.deb ...
Unpacking intltool-debian (0.35.0+20060710.6) ...
Selecting previously unselected package po-debconf.
Preparing to unpack .../30-po-debconf_1.0.21+nmu1_all.deb ...
Unpacking po-debconf (1.0.21+nmu1) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../31-debhelper_13.11.4_all.deb ...
Unpacking debhelper (13.11.4) ...
Selecting previously unselected package fonts-dejavu-core.
Preparing to unpack .../32-fonts-dejavu-core_2.37-6_all.deb ...
Unpacking fonts-dejavu-core (2.37-6) ...
Selecting previously unselected package fontconfig-config.
Preparing to unpack .../33-fontconfig-config_2.14.1-4_i386.deb ...
Unpacking fontconfig-config (2.14.1-4) ...
Selecting previously unselected package fonts-lmodern.
Preparing to unpack .../34-fonts-lmodern_2.005-1_all.deb ...
Unpacking fonts-lmodern (2.005-1) ...
Selecting previously unselected package libbrotli1:i386.
Preparing to unpack .../35-libbrotli1_1.0.9-2+b6_i386.deb ...
Unpacking libbrotli1:i386 (1.0.9-2+b6) ...
Selecting previously unselected package libbsd0:i386.
Preparing to unpack .../36-libbsd0_0.11.7-2_i386.deb ...
Unpacking libbsd0:i386 (0.11.7-2) ...
Selecting previously unselected package libexpat1:i386.
Preparing to unpack .../37-libexpat1_2.5.0-1_i386.deb ...
Unpacking libexpat1:i386 (2.5.0-1) ...
Selecting previously unselected package libpng16-16:i386.
Preparing to unpack .../38-libpng16-16_1.6.39-2_i386.deb ...
Unpacking libpng16-16:i386 (1.6.39-2) ...
Selecting previously unselected package libfreetype6:i386.
Preparing to unpack .../39-libfreetype6_2.12.1+dfsg-4_i386.deb ...
Unpacking libfreetype6:i386 (2.12.1+dfsg-4) ...
Selecting previously unselected package libfontconfig1:i386.
Preparing to unpack .../40-libfontconfig1_2.14.1-4_i386.deb ...
Unpacking libfontconfig1:i386 (2.14.1-4) ...
Selecting previously unselected package libpixman-1-0:i386.
Preparing to unpack .../41-libpixman-1-0_0.42.2-1_i386.deb ...
Unpacking libpixman-1-0:i386 (0.42.2-1) ...
Selecting previously unselected package libxau6:i386.
Preparing to unpack .../42-libxau6_1%3a1.0.9-1_i386.deb ...
Unpacking libxau6:i386 (1:1.0.9-1) ...
Selecting previously unselected package libxdmcp6:i386.
Preparing to unpack .../43-libxdmcp6_1%3a1.1.2-3_i386.deb ...
Unpacking libxdmcp6:i386 (1:1.1.2-3) ...
Selecting previously unselected package libxcb1:i386.
Preparing to unpack .../44-libxcb1_1.15-1_i386.deb ...
Unpacking libxcb1:i386 (1.15-1) ...
Selecting previously unselected package libx11-data.
Preparing to unpack .../45-libx11-data_2%3a1.8.4-2_all.deb ...
Unpacking libx11-data (2:1.8.4-2) ...
Selecting previously unselected package libx11-6:i386.
Preparing to unpack .../46-libx11-6_2%3a1.8.4-2_i386.deb ...
Unpacking libx11-6:i386 (2:1.8.4-2) ...
Selecting previously unselected package libxcb-render0:i386.
Preparing to unpack .../47-libxcb-render0_1.15-1_i386.deb ...
Unpacking libxcb-render0:i386 (1.15-1) ...
Selecting previously unselected package libxcb-shm0:i386.
Preparing to unpack .../48-libxcb-shm0_1.15-1_i386.deb ...
Unpacking libxcb-shm0:i386 (1.15-1) ...
Selecting previously unselected package libxext6:i386.
Preparing to unpack .../49-libxext6_2%3a1.3.4-1+b1_i386.deb ...
Unpacking libxext6:i386 (2:1.3.4-1+b1) ...
Selecting previously unselected package libxrender1:i386.
Preparing to unpack .../50-libxrender1_1%3a0.9.10-1.1_i386.deb ...
Unpacking libxrender1:i386 (1:0.9.10-1.1) ...
Selecting previously unselected package libcairo2:i386.
Preparing to unpack .../51-libcairo2_1.16.0-7_i386.deb ...
Unpacking libcairo2:i386 (1.16.0-7) ...
Selecting previously unselected package libglib2.0-0:i386.
Preparing to unpack .../52-libglib2.0-0_2.74.6-1_i386.deb ...
Unpacking libglib2.0-0:i386 (2.74.6-1) ...
Selecting previously unselected package libgraphite2-3:i386.
Preparing to unpack .../53-libgraphite2-3_1.3.14-1_i386.deb ...
Unpacking libgraphite2-3:i386 (1.3.14-1) ...
Selecting previously unselected package libharfbuzz0b:i386.
Preparing to unpack .../54-libharfbuzz0b_6.0.0+dfsg-3_i386.deb ...
Unpacking libharfbuzz0b:i386 (6.0.0+dfsg-3) ...
Selecting previously unselected package x11-common.
Preparing to unpack .../55-x11-common_1%3a7.7+23_all.deb ...
Unpacking x11-common (1:7.7+23) ...
Selecting previously unselected package libice6:i386.
Preparing to unpack .../56-libice6_2%3a1.0.10-1_i386.deb ...
Unpacking libice6:i386 (2:1.0.10-1) ...
Selecting previously unselected package libkpathsea6:i386.
Preparing to unpack .../57-libkpathsea6_2022.20220321.62855-5_i386.deb ...
Unpacking libkpathsea6:i386 (2022.20220321.62855-5) ...
Selecting previously unselected package libpaper1:i386.
Preparing to unpack .../58-libpaper1_1.1.29_i386.deb ...
Unpacking libpaper1:i386 (1.1.29) ...
Selecting previously unselected package libpaper-utils.
Preparing to unpack .../59-libpaper-utils_1.1.29_i386.deb ...
Unpacking libpaper-utils (1.1.29) ...
Selecting previously unselected package libptexenc1:i386.
Preparing to unpack .../60-libptexenc1_2022.20220321.62855-5_i386.deb ...
Unpacking libptexenc1:i386 (2022.20220321.62855-5) ...
Selecting previously unselected package libsm6:i386.
Preparing to unpack .../61-libsm6_2%3a1.2.3-1_i386.deb ...
Unpacking libsm6:i386 (2:1.2.3-1) ...
Selecting previously unselected package libsynctex2:i386.
Preparing to unpack .../62-libsynctex2_2022.20220321.62855-5_i386.deb ...
Unpacking libsynctex2:i386 (2022.20220321.62855-5) ...
Selecting previously unselected package libteckit0:i386.
Preparing to unpack .../63-libteckit0_2.5.11+ds1-1+b1_i386.deb ...
Unpacking libteckit0:i386 (2.5.11+ds1-1+b1) ...
Selecting previously unselected package libtexlua53-5:i386.
Preparing to unpack .../64-libtexlua53-5_2022.20220321.62855-5_i386.deb ...
Unpacking libtexlua53-5:i386 (2022.20220321.62855-5) ...
Selecting previously unselected package libtexluajit2:i386.
Preparing to unpack .../65-libtexluajit2_2022.20220321.62855-5_i386.deb ...
Unpacking libtexluajit2:i386 (2022.20220321.62855-5) ...
Selecting previously unselected package libxt6:i386.
Preparing to unpack .../66-libxt6_1%3a1.2.1-1.1_i386.deb ...
Unpacking libxt6:i386 (1:1.2.1-1.1) ...
Selecting previously unselected package libxmu6:i386.
Preparing to unpack .../67-libxmu6_2%3a1.1.3-3_i386.deb ...
Unpacking libxmu6:i386 (2:1.1.3-3) ...
Selecting previously unselected package libxpm4:i386.
Preparing to unpack .../68-libxpm4_1%3a3.5.12-1.1_i386.deb ...
Unpacking libxpm4:i386 (1:3.5.12-1.1) ...
Selecting previously unselected package libxaw7:i386.
Preparing to unpack .../69-libxaw7_2%3a1.0.14-1_i386.deb ...
Unpacking libxaw7:i386 (2:1.0.14-1) ...
Selecting previously unselected package libxi6:i386.
Preparing to unpack .../70-libxi6_2%3a1.8-1+b1_i386.deb ...
Unpacking libxi6:i386 (2:1.8-1+b1) ...
Selecting previously unselected package libzzip-0-13:i386.
Preparing to unpack .../71-libzzip-0-13_0.13.72+dfsg.1-1.1_i386.deb ...
Unpacking libzzip-0-13:i386 (0.13.72+dfsg.1-1.1) ...
Selecting previously unselected package racket-common.
Preparing to unpack .../72-racket-common_8.7+dfsg1-1_all.deb ...
Unpacking racket-common (8.7+dfsg1-1) ...
Selecting previously unselected package racket.
Preparing to unpack .../73-racket_8.7+dfsg1-1_i386.deb ...
Unpacking racket (8.7+dfsg1-1) ...
Selecting previously unselected package t1utils.
Preparing to unpack .../74-t1utils_1.41-4_i386.deb ...
Unpacking t1utils (1.41-4) ...
Selecting previously unselected package tex-common.
Preparing to unpack .../75-tex-common_6.18_all.deb ...
Unpacking tex-common (6.18) ...
Selecting previously unselected package texlive-binaries.
Preparing to unpack .../76-texlive-binaries_2022.20220321.62855-5_i386.deb ...
Unpacking texlive-binaries (2022.20220321.62855-5) ...
Selecting previously unselected package xdg-utils.
Preparing to unpack .../77-xdg-utils_1.1.3-4.1_all.deb ...
Unpacking xdg-utils (1.1.3-4.1) ...
Selecting previously unselected package texlive-base.
Preparing to unpack .../78-texlive-base_2022.20230122-3_all.deb ...
Unpacking texlive-base (2022.20230122-3) ...
Selecting previously unselected package texlive-fonts-recommended.
Preparing to unpack .../79-texlive-fonts-recommended_2022.20230122-3_all.deb ...
Unpacking texlive-fonts-recommended (2022.20230122-3) ...
Selecting previously unselected package texlive-latex-base.
Preparing to unpack .../80-texlive-latex-base_2022.20230122-3_all.deb ...
Unpacking texlive-latex-base (2022.20230122-3) ...
Selecting previously unselected package texlive-latex-recommended.
Preparing to unpack .../81-texlive-latex-recommended_2022.20230122-3_all.deb ...
Unpacking texlive-latex-recommended (2022.20230122-3) ...
Selecting previously unselected package texlive.
Preparing to unpack .../82-texlive_2022.20230122-3_all.deb ...
Unpacking texlive (2022.20230122-3) ...
Setting up libexpat1:i386 (2.5.0-1) ...
Setting up libpipeline1:i386 (1.5.7-1) ...
Setting up libgraphite2-3:i386 (1.3.14-1) ...
Setting up libpixman-1-0:i386 (0.42.2-1) ...
Setting up libxau6:i386 (1:1.0.9-1) ...
Setting up libicu72:i386 (72.1-3) ...
Setting up bsdextrautils (2.38.1-5+b1) ...
Setting up libmagic-mgc (1:5.44-3) ...
Setting up libarchive-zip-perl (1.68-1) ...
Setting up libglib2.0-0:i386 (2.74.6-1) ...
No schema files found: doing nothing.
Setting up libtexluajit2:i386 (2022.20220321.62855-5) ...
Setting up libdebhelper-perl (13.11.4) ...
Setting up libbrotli1:i386 (1.0.9-2+b6) ...
Setting up x11-common (1:7.7+23) ...
invoke-rc.d: could not determine current runlevel
Setting up X socket directories... /tmp/.X11-unix /tmp/.ICE-unix.
Setting up libmagic1:i386 (1:5.44-3) ...
Setting up gettext-base (0.21-12) ...
Setting up m4 (1.4.19-3) ...
Setting up libzzip-0-13:i386 (0.13.72+dfsg.1-1.1) ...
Setting up file (1:5.44-3) ...
Setting up sse2-support (15) ...
Setting up autotools-dev (20220109.1) ...
Setting up libx11-data (2:1.8.4-2) ...
Setting up libteckit0:i386 (2.5.11+ds1-1+b1) ...
Setting up t1utils (1.41-4) ...
Setting up libtexlua53-5:i386 (2022.20220321.62855-5) ...
Setting up libpng16-16:i386 (1.6.39-2) ...
Setting up autopoint (0.21-12) ...
Setting up fonts-dejavu-core (2.37-6) ...
Setting up libkpathsea6:i386 (2022.20220321.62855-5) ...
Setting up autoconf (2.71-3) ...
Setting up sensible-utils (0.0.17+nmu1) ...
Setting up libuchardet0:i386 (0.0.7-1) ...
Setting up fonts-lmodern (2.005-1) ...
Setting up libsub-override-perl (0.09-4) ...
Setting up libbsd0:i386 (0.11.7-2) ...
Setting up racket-common (8.7+dfsg1-1) ...
Setting up libelf1:i386 (0.188-2.1) ...
Setting up libxml2:i386 (2.9.14+dfsg-1.1+b3) ...
Setting up xdg-utils (1.1.3-4.1) ...
update-alternatives: using /usr/bin/xdg-open to provide /usr/bin/open (open) in auto mode
Setting up libsynctex2:i386 (2022.20220321.62855-5) ...
Setting up automake (1:1.16.5-1.3) ...
update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode
Setting up libfile-stripnondeterminism-perl (1.13.1-1) ...
Setting up libice6:i386 (2:1.0.10-1) ...
Setting up libxdmcp6:i386 (1:1.1.2-3) ...
Setting up libxcb1:i386 (1.15-1) ...
Setting up gettext (0.21-12) ...
Setting up libtool (2.4.7-5) ...
Setting up libxcb-render0:i386 (1.15-1) ...
Setting up fontconfig-config (2.14.1-4) ...
Setting up libxcb-shm0:i386 (1.15-1) ...
Setting up intltool-debian (0.35.0+20060710.6) ...
Setting up dh-autoreconf (20) ...
Setting up libptexenc1:i386 (2022.20220321.62855-5) ...
Setting up libfreetype6:i386 (2.12.1+dfsg-4) ...
Setting up racket (8.7+dfsg1-1) ...
Setting up ucf (3.0043+nmu1) ...
Setting up dh-strip-nondeterminism (1.13.1-1) ...
Setting up dwz (0.15-1) ...
Setting up groff-base (1.22.4-10) ...
Setting up libx11-6:i386 (2:1.8.4-2) ...
Setting up libharfbuzz0b:i386 (6.0.0+dfsg-3) ...
Setting up libfontconfig1:i386 (2.14.1-4) ...
Setting up libsm6:i386 (2:1.2.3-1) ...
Setting up libpaper1:i386 (1.1.29) ...
Creating config file /etc/papersize with new version
Setting up libxpm4:i386 (1:3.5.12-1.1) ...
Setting up libxrender1:i386 (1:0.9.10-1.1) ...
Setting up po-debconf (1.0.21+nmu1) ...
Setting up libxext6:i386 (2:1.3.4-1+b1) ...
Setting up libpaper-utils (1.1.29) ...
Setting up man-db (2.11.2-2) ...
Not building database; man-db/auto-update is not 'true'.
Setting up libcairo2:i386 (1.16.0-7) ...
Setting up tex-common (6.18) ...
update-language: texlive-base not installed and configured, doing nothing!
Setting up libxt6:i386 (1:1.2.1-1.1) ...
Setting up libxmu6:i386 (2:1.1.3-3) ...
Setting up libxi6:i386 (2:1.8-1+b1) ...
Setting up debhelper (13.11.4) ...
Setting up libxaw7:i386 (2:1.0.14-1) ...
Setting up texlive-binaries (2022.20220321.62855-5) ...
update-alternatives: using /usr/bin/xdvi-xaw to provide /usr/bin/xdvi.bin (xdvi.bin) in auto mode
update-alternatives: using /usr/bin/bibtex.original to provide /usr/bin/bibtex (bibtex) in auto mode
Setting up texlive-base (2022.20230122-3) ...
tl-paper: setting paper size for dvips to a4: /var/lib/texmf/dvips/config/config-paper.ps
tl-paper: setting paper size for dvipdfmx to a4: /var/lib/texmf/dvipdfmx/dvipdfmx-paper.cfg
tl-paper: setting paper size for xdvi to a4: /var/lib/texmf/xdvi/XDvi-paper
tl-paper: setting paper size for pdftex to a4: /var/lib/texmf/tex/generic/tex-ini-files/pdftexconfig.tex
Setting up texlive-latex-base (2022.20230122-3) ...
Setting up texlive-latex-recommended (2022.20230122-3) ...
Setting up texlive-fonts-recommended (2022.20230122-3) ...
Setting up texlive (2022.20230122-3) ...
Processing triggers for libc-bin (2.36-8) ...
Processing triggers for tex-common (6.18) ...
Running updmap-sys. This may take some time... done.
Running mktexlsr /var/lib/texmf ... done.
Building format(s) --all.
This may take some time... done.
Reading package lists...
Building dependency tree...
Reading state information...
Reading extended state information...
Initializing package states...
Writing extended state information...
Building tag database...
-> Finished parsing the build-deps
I: Building the package
I: Running cd /build/minlog-4.0.99.20100221/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../minlog_4.0.99.20100221-7_source.changes
dpkg-buildpackage: info: source package minlog
dpkg-buildpackage: info: source version 4.0.99.20100221-7
dpkg-buildpackage: info: source distribution unstable
dpkg-buildpackage: info: source changed by Vagrant Cascadian <vagrant@reproducible-builds.org>
dpkg-source --before-build .
dpkg-buildpackage: info: host architecture i386
debian/rules clean
dh clean --no-parallel
dh_auto_clean -O--no-parallel
make -j1 clean
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
rm -rf *~
rm -rf init.scm mpc minlog minlog.el welcome.scm
(cd src; make clean)
make[2]: Entering directory '/build/minlog-4.0.99.20100221/src'
rm -rf .dep .dep.*
rm -rf TAGS
rm -rf *~ *%
rm -rf grammar.log
make[2]: Leaving directory '/build/minlog-4.0.99.20100221/src'
(cd doc; make clean)
make[2]: Entering directory '/build/minlog-4.0.99.20100221/doc'
rm -rf *.aux *.log *.blg *.bbl *.idx *.toc *.ind *.ilg *.brf *.out
rm -rf .dep .dep.*
rm -rf *.dvi *.pdf *.ps
rm -rf *~ *%
ls -sh
total 744K
4.0K Makefile
4.0K acknow.tex
28K bussproofs.sty
8.0K infrule.sty
4.0K manual.txt
16K minlog.bib
20K minlog.mac
320K mlcf.tex
32K mpcref.tex
16K notation.sty
216K ref.tex
12K reflection_manual.tex
64K tutor.tex
make[2]: Leaving directory '/build/minlog-4.0.99.20100221/doc'
(cd examples; make clean)
make[2]: Entering directory '/build/minlog-4.0.99.20100221/examples'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
(cd classical; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/classical'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/classical'
(cd hounif; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/hounif'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/hounif'
(cd prop; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/prop'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/prop'
(cd quant; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/quant'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/quant'
(cd warshall; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/warshall'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/warshall'
(cd dijkstra; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/dijkstra'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/dijkstra'
(cd bar; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/bar'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/bar'
(cd dc; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/dc'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/dc'
(cd arith; make clean)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples/arith'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
(cd quotrem; make clean)
make[4]: Entering directory '/build/minlog-4.0.99.20100221/examples/arith/quotrem'
rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed
make[4]: Leaving directory '/build/minlog-4.0.99.20100221/examples/arith/quotrem'
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples/arith'
make[2]: Leaving directory '/build/minlog-4.0.99.20100221/examples'
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
dh_autoreconf_clean -O--no-parallel
dh_clean -O--no-parallel
debian/rules binary
dh binary --no-parallel
dh_update_autotools_config -O--no-parallel
dh_autoreconf -O--no-parallel
dh_auto_configure -O--no-parallel
dh_auto_build -O--no-parallel
make -j1 "INSTALL=install --strip-program=true"
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
(cd src; make .dep.notags)
make[2]: Entering directory '/build/minlog-4.0.99.20100221/src'
make[2]: Nothing to be done for '.dep.notags'.
make[2]: Leaving directory '/build/minlog-4.0.99.20100221/src'
sed "s%---MINLOGPATH---%`pwd`%g" < src/init.scm > init.scm
sed "s%---MINLOGPATH---%`pwd`%g" < src/mpc > mpc
chmod a+x mpc
sed "s%---MINLOGPATH---%`pwd`%g" < src/minlog > minlog
chmod a+x minlog
sed "s%---MINLOGPATH---%`pwd`%g; s%---MINLOGELPATH---%`pwd`%g" < src/minlog.el > minlog.el
(cd doc; make .dep)
make[2]: Entering directory '/build/minlog-4.0.99.20100221/doc'
pdflatex mlcf >> /dev/null
bibtex -terse mlcf
makeindex -q mlcf
pdflatex mlcf >> /dev/null
pdflatex mlcf >> /dev/null
pdflatex mpcref.tex >> /dev/null
kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 tcrm1095
mktexpk: Running mf-nowin -progname=mf \mode:=ljfour; mag:=1+0/600; nonstopmode; input tcrm1095
This is METAFONT, Version 2.71828182 (TeX Live 2022/Debian) (preloaded base=mf)
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/tcrm1095.mf
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/tcrm.mf
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txsymb.mf
Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf
Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txpseudo.mf
Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txaccent.mf
Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [27] [29])
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txgen.mf
Ok [100] [109] [98] [99] [108])
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txsymbol.mf
Ok [13] [18] [21] [22] [23] [24] [25] [26] [28] [31] [32] [36] [39] [44]
[45] [46] [42] [47] [60] [61] [62] [77] [79] [87] [110] [91] [93] [94] [95]
[96] [126] [127] [128] [129] [130] [131] [132] [133] [134] [135] [136] [137]
[138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149]
[150] [151] [152] [153] [154] [155] [156] [157] [158] [159] [160] [161]
[162] [163] [164] [165] [166] [167] [168] [169] [171] [172] [173] [174]
[175] [177] [176] [180] [181] [182] [183] [184] [187] [191] [214] [246])
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txromod.mf
Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txrsuper.mf
Ok [185] [178] [179] [170] [186])
(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txrfract.mf
Ok [188] [189] [190]) ) ) )
(some charht values had to be adjusted by as much as 0.06952pt)
Font metrics written on tcrm1095.tfm.
Output written on tcrm1095.600gf (128 characters, 25592 bytes).
Transcript written on tcrm1095.log.
mktexpk: /build/minlog-4.0.99.20100221/debian/.debhelper/generated/_source/home/.texlive2022/texmf-var/fonts/pk/ljfour/jknappen/ec/tcrm1095.600pk: successfully generated.
pdflatex mpcref.tex >> /dev/null
pdflatex ref >> /dev/null
bibtex -terse ref
makeindex -q ref
pdflatex ref >> /dev/null
pdflatex ref >> /dev/null
pdflatex reflection_manual.tex >> /dev/null
pdflatex reflection_manual.tex >> /dev/null
pdflatex tutor >> /dev/null
bibtex -terse tutor
pdflatex tutor >> /dev/null
rm -rf *.aux *.log *.blg *.bbl *.idx *.toc *.ind *.ilg *.brf *.out
touch .dep
make[2]: Leaving directory '/build/minlog-4.0.99.20100221/doc'
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
debian/rules override_dh_auto_test
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
dh_auto_test || echo 'WARNING: Test suite failures'
make -j1 test
make[2]: Entering directory '/build/minlog-4.0.99.20100221'
(cd src; make .dep.notags)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/src'
make[3]: Nothing to be done for '.dep.notags'.
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/src'
(cd examples; make .TEST)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/examples'
cat test.scm | petite -- ..//init.scm | sed "1d;2d" > test.out
/bin/sh: 1: petite: not found
cat test.out | sed "s/[0-9]//g" > test.out.nodigits
cat test.save | sed "s/[0-9]//g" > test.save.nodigits
if diff -u test.out.nodigits test.save.nodigits > test.diff; then \
rm test.out.nodigits test.save.nodigits test.out test.diff; \
touch .test.test-passed; echo 'test is OK'; else \
if [ -n "" ]; then \
cat test.diff; \
echo -n "Accept new output for `pwd`/test.scm? [n|y] "; \
read input; \
if [ "$input" = "y" -o "$input" = "yes" ]; then \
cp test.out test.save; \
fi; \
else \
cat ..//examples/warning.txt; echo "test"; echo " ";pwd; echo " "; \
cat test.diff; \
false;\
fi; \
fi
==============================================================================
WARNING: detected a difference in the output
------------------------------------------------------------------------------
The offending filename is printed below (followed by the current directory)
There might be two reasons for this:
1.) Minlog has a new feature and therefore gives new answers. In this case
change the corresponding .save file.
2.) A new bug was introduced to the minlog system. Fix it!
Read the differences carefully before deciding whether 1 or 2 is the case.
You might also whish to read the .out file containing all of minlog's output.
==============================================================================
test
/build/minlog-4.0.99.20100221/examples
--- test.out.nodigits 2023-04-16 11:20:52.662140032 -1200
+++ test.save.nodigits 2023-04-16 11:20:52.674139598 -1200
@@ -0,0 +1,4545 @@
+
+
+Minlog loaded successfully
+> > ; ok, algebra nat added
+> ; ok, algebra ordl added
+> ; ok, algebra list added
+> ; ok, algebra ytensor added
+> ; ok, algebra yplus added
+> ; ok, algebra tree added
+; ok, algebra tlist added
+> ; ok, algebra labtree added
+; ok, algebra labtlist added
+> ; ok, algebra hterm added
+; ok, algebra htermlist added
+; ok, algebra term added
+> ; ok, algebra inftree added
+; ok, algebra inftlist added
+> #t
+> #f
+> #t
+> #f
+> #t
+> #f
+> #t
+> #f
+> #t
+> #t
+> #t
+> #t
+> #f
+> #f
+> #t
+> #f
+> #t
+> #f
+> #t
+> #t
+> #t
+> #t
+> #f
+> ; ok, algebra nat removed
+; ok, constructor Lim removed
+; ok, constructor Infbranch removed
+; ok, constructor Newleaf removed
+; ok, constructor Dn removed
+; ok, constructor OrdSup removed
+; ok, constructor Succ removed
+; ok, constructor Zero removed
+; ok, algebra ordl removed
+; ok, constructor OrdZero removed
+; ok, algebra list removed
+; ok, constructor Cons removed
+; ok, constructor Nil removed
+; ok, algebra ytensor removed
+; ok, constructor TensorPair removed
+; ok, algebra yplus removed
+; ok, constructor Inright removed
+; ok, constructor Inleft removed
+; ok, algebra tree removed
+; ok, algebra tlist removed
+; ok, constructor Tcons removed
+; ok, constructor Empty removed
+; ok, constructor Branch removed
+; ok, constructor Leaf removed
+; ok, algebra labtree removed
+; ok, algebra labtlist removed
+; ok, constructor LabTcons removed
+; ok, constructor LabEmpty removed
+; ok, constructor LabBranch removed
+; ok, constructor LabLeaf removed
+; ok, algebra hterm removed
+; ok, algebra htermlist removed
+; ok, algebra term removed
+; ok, constructor Seq removed
+; ok, constructor Hcons removed
+; ok, constructor Hempty removed
+; ok, constructor One removed
+; ok, algebra inftree removed
+; ok, algebra inftlist removed
+; ok, constructor Inftcons removed
+; ok, constructor Emptyinftlist removed
+> ; ok, algebra tree added
+; ok, algebra tlist added
+> ; ok, algebra nat added
+> alpha=>boole
+tlist alpha=>nat=>boole
+nat
+tree alpha=>tlist alpha=>boole=>nat=>nat
+> nat
+tlist alpha=>nat=>nat
+> alpha=>boole
+boole
+> tree alpha=>
+(alpha=>alpha)=>
+(tlist alpha=>alpha=>alpha)=>
+alpha=>(tree alpha=>tlist alpha=>alpha=>alpha=>alpha)=>alpha
+tlist alpha=>
+(alpha=>alpha)=>
+(tlist alpha=>alpha=>alpha)=>
+alpha=>(tree alpha=>tlist alpha=>alpha=>alpha=>alpha)=>alpha
+; Type substitution:
+; alpha -> unit
+; alpha -> boole
+; alpha -> nat
+> tlist alpha=>alpha=>(tlist alpha=>alpha=>alpha)=>alpha
+; Type substitution:
+; alpha -> unit
+; alpha -> nat
+> tree alpha=>(alpha=>alpha)=>alpha=>alpha
+; Type substitution:
+; alpha -> unit
+; alpha -> boole
+> ; ok, algebra tree removed
+; ok, algebra tlist removed
+; ok, constructor Tcons removed
+; ok, constructor Empty removed
+; ok, constructor Branch removed
+; ok, constructor Leaf removed
+> ; ok, algebra nat removed
+; ok, constructor Succ removed
+; ok, constructor Zero removed
+> > loading nat.scm ...
+> > ; ok, inductively defined predicate constant Even added
+> ("cInitEven" "cGenEven")
+> ; ok, inductively defined predicate constant Ev added
+; ok, inductively defined predicate constant Od added
+> ("cInitEv" "cGenEv")
+> ("cGenOd")
+> ; ok, variable x: alpha added
+; ok, variable y: alpha added
+; ok, variable z: alpha added
+> ; ok, predicate variable P: (arity) added
+> ; ok, predicate variable Q: (arity alpha) added
+> ; ok, predicate variable R: (arity alpha alpha) added
+> ; ok, inductively defined predicate constant EqD added
+> > x^ eqd x^
+> > n eqd n
+> ; ok, inductively defined predicate constant OrD added
+> ("cInlOrD" "cInrOrD")
+> > P ord P
+> > T ord F
+> ; ok, inductively defined predicate constant ExD added
+> > "exd n n=m"
+> ; ok, inductively defined predicate constant PiOne added
+> ; ok, inductively defined predicate constant TrCl added
+> ; ok, inductively defined predicate constant Acc added
+> ("cEfqAcc" "cGenAccSup")
+> > (Acc (cterm (x^,x^) R x^ x^))x^
+> > (Acc (cterm (n,n) n<n))n
+> ; ok, inductively defined predicate constant ExDT added
+> ; ok, inductively defined predicate constant Cup added
+> ; ok, inductively defined predicate constant Cap added
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable y is removed
+; ok, variable z is removed
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity)
+; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity alpha)
+; ok, predicate variable R is removed
+; warning: R was default pvariable of arity (arity alpha alpha)
+> ; ok, inductively defined predicate constant Even removed
+; ok, inductively defined predicate constant Ev removed
+; ok, inductively defined predicate constant Od removed
+; ok, inductively defined predicate constant EqD removed
+; ok, inductively defined predicate constant OrD removed
+; ok, inductively defined predicate constant ExD removed
+; ok, inductively defined predicate constant PiOne removed
+; ok, inductively defined predicate constant TrCl removed
+; ok, inductively defined predicate constant Acc removed
+; ok, inductively defined predicate constant ExDT removed
+; ok, inductively defined predicate constant Cup removed
+; ok, inductively defined predicate constant Cap removed
+> ; ok, variable x: alpha added
+> ; ok, predicate variable Q: (arity alpha) added
+> ; Predicate substitution:
+; Q -> (cterm (x^) Total x^)
+> ; Predicate substitution:
+; (Pvar unit) -> (cterm (unit^) Total x^)
+> ; Type substitution:
+; alpha -> unit
+; Substitution:
+; x^ -> unit^
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity alpha)
+> ; Predicate substitution:
+; (Pvar boole) -> (cterm (boole) boole=boole)
+> ; Predicate substitution:
+; (Pvar boole) -> (cterm (boole^) Equal boole^ boole^)
+> ; ok, algebra tree added
+; ok, algebra tlist added
+> ; ok, variable u: tree alpha added
+; ok, variable v: tree alpha added
+> ; ok, variable us: tlist alpha added
+; ok, variable vs: tlist alpha added
+> ; ok, variable a: tree unit added
+; ok, variable b: tree unit added
+> ; ok, variable as: tlist unit added
+; ok, variable bs: tlist unit added
+> (Rec tlist unit=>nat tree unit=>tree unit)as([unit](Leaf unit)unit)
+([as,n](Branch unit)as)
+
+([a,bs,a,n]Succ n)
+> (Rec tlist unit=>nat)as ([as]Succ)
+> (Rec tlist unit=>nat)as ([as,n]Succ n)
+> ; ok, variable u is removed
+; warning: u was default variable of type tree alpha
+; ok, variable v is removed
+> ; ok, variable us is removed
+; warning: us was default variable of type tlist alpha
+; ok, variable vs is removed
+> ; ok, variable a is removed
+; warning: a was default variable of type tree unit
+; ok, variable b is removed
+> ; ok, variable as is removed
+; warning: as was default variable of type tlist unit
+; ok, variable bs is removed
+> ; ok, algebra tree removed
+; ok, algebra tlist removed
+; ok, constructor Tcons removed
+; ok, constructor Empty removed
+; ok, constructor Branch removed
+; ok, constructor Leaf removed
+> ; ok, variable x: alpha added
+; ok, variable y: alpha added
+> ; ok, predicate variable Q: (arity alpha) added
+> ; ok, inductively defined predicate constant ExD added
+> > > ("x" "x")
+> ("alpha")
+> ("Q")
+> ; warning: x already is a variable of type alpha
+; warning: y already is a variable of type alpha
+> ; warning: Q already is a predicate variable of arity (arity alpha)
+> exd unit(Equal unit unit -> (Pvar unit)_ unit)
+> Total boole^
+> Q y
+> Total x
+> Equal x^ x^
+> Equal x^ x^
+> exd boole^ Equal boole^ boole^
+> exd x^ Equal x^ x^
+> exd x^ Equal x^ x^
+> ; ok, inductively defined predicate constant ExDT added
+> exdt x Equal x x
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable y is removed
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity alpha)
+> ; ok, inductively defined predicate constant ExD removed
+; ok, inductively defined predicate constant ExDT removed
+> > ()
+> #t
+> nat=>
+nat=>((nat=>atomic=>atomic)=>atomic)=>(nat=>nat=>atomic=>alpha)=>alpha
+>
+> (((var (alg "unit") "") (var (alg "unit") "")))
+> "n"
+> all n(
+ = -> all n(n=n -> Succ n=Succ n) -> n=n)
+> all n(= -> all n(n=n -> Succ n=Succ n) -> n=n)
+> all (nat=>nat)_,n(
+ all n(
+ all n((nat=>nat)_ n<(nat=>nat)_ n -> n=n) ->
+ n=n) ->
+ allnc boole(boole -> n=n))
+> all (nat=>nat),n(
+ all n(all n((nat=>nat)n<(nat=>nat)n -> n=n) -> n=n) ->
+ allnc boole(boole -> n=n))
+> ; ok, algebra list added
+> ; ok, predicate variable P: (arity nat) added
+> all n^(
+ E n^ ->
+ P -> all n(P n -> P(Succ n)) -> P n^)
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity nat)
+> ; ok, predicate variable P: (arity list nat) added
+> ; ok, variable ns: list nat added
+> all (list alpha)^(
+ SE(list alpha)^ ->
+ (Pvar list alpha)_(Nil alpha) ->
+ all alpha^,(list alpha)^(
+ SE(list alpha)^ ->
+ (Pvar list alpha)_(list alpha)^ ->
+ (Pvar list alpha)_((Cons alpha)alpha^(list alpha)^)) ->
+ (Pvar list alpha)_(list alpha)^)
+> ; Type substitution:
+; alpha -> nat
+; Predicate substitution:
+; (Pvar list alpha)_ -> (cterm (ns^) P ns^)
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity list nat)
+> ; ok, variable ns is removed
+; warning: ns was default variable of type list nat
+> ; ok, algebra list removed
+; ok, constructor Cons removed
+; ok, constructor Nil removed
+> ; ok, predicate variable P: (arity nat) added
+> all n(P -> all n(P n -> P(Succ n)) -> P n)
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity nat)
+> ; ok, algebra tree added
+; ok, algebra tlist added
+> ; ok, predicate variable P: (arity tree) added
+> ; ok, predicate variable Q: (arity tlist) added
+> all tree(
+ P Leaf ->
+ all tlist(Q tlist -> P(Branch tlist)) ->
+ Q Empty ->
+ all tree,tlist(
+ P tree -> Q tlist -> Q(Tcons tree tlist)) ->
+ P tree)
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity tree)
+; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity tlist)
+> ; ok, algebra tree removed
+; ok, algebra tlist removed
+; ok, constructor Tcons removed
+; ok, constructor Empty removed
+; ok, constructor Branch removed
+; ok, constructor Leaf removed
+> ; ok, predicate variable P: (arity nat) added
+> all n(P -> all n P(Succ n) -> P n)
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity nat)
+> ; ok, variable h: alpha=>alpha=>nat added
+> ; ok, variable x: alpha added
+> ; ok, predicate variable R: (arity alpha alpha) added
+> all h,x,x(
+ all x,x(
+ all x,x(h x x<h x x -> R x x) ->
+ R x x) ->
+ allnc boole(boole -> R x x))
+> ; ok, inductively defined predicate constant Even added
+> > > Even
+> > allnc n^(Even n^ -> Even(n^ +))
+> > algEven=>algEven
+> ; ok, predicate variable Q: (arity nat) added
+> > allnc n^(
+ Even n^ -> Q -> allnc n^(Even n^ -> Q n^ -> Q(n^ +)) -> Q n^)
+> > algEven=>alpha=>(algEven=>alpha=>alpha)=>alpha
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity nat)
+> ; ok, inductively defined predicate constant Even removed
+> ; ok, inductively defined predicate constant Ev added
+; ok, inductively defined predicate constant Od added
+> > > > Ev
+> > allnc n^(Od n^ -> Ev(n^ +))
+> > allnc n^(Ev n^ -> Od(n^ +))
+> > algEv=>algOd
+> ; ok, predicate variable Q: (arity nat) added
+> > allnc n^(
+ Ev n^ ->
+ Q ->
+ allnc n^(Od n^ -> Q n^ -> Q(n^ +)) ->
+ allnc n^(Ev n^ -> Q n^ -> Q(n^ +)) -> Q n^)
+> > algEv=>
+alpha=>(algOd=>alpha=>alpha)=>(algEv=>alpha=>alpha)=>alpha
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity nat)
+> ; ok, inductively defined predicate constant Ev removed
+; ok, inductively defined predicate constant Od removed
+> ; warning: x already is a variable of type alpha
+; ok, variable y: alpha added
+; ok, variable z: alpha added
+> ; ok, predicate variable P: (arity) added
+> ; ok, predicate variable Q: (arity alpha) added
+> ; warning: R already is a predicate variable of arity (arity alpha alpha)
+> ; ok, inductively defined predicate constant EqD added
+> > > allnc x^ x^ eqd x^
+> > algEqD
+> > allnc x^,x^(
+ x^ eqd x^ -> allnc x^ R x^ x^ -> R x^ x^)
+> > algEqD=>alpha=>alpha
+> ; ok, inductively defined predicate constant OrD added
+> > > P -> P ord P
+> > P -> P ord P
+> > alpha=>algOrD alpha alpha
+> > P ord P -> (P -> P) -> (P -> P) -> P
+> > algOrD alpha alpha=>(alpha=>alpha)=>(alpha=>alpha)=>alpha
+> ; ok, inductively defined predicate constant ExD added
+> > "exd n n=m"
+> > allnc m all n^(n^=m -> exd n^ n^=m)
+> > nat=>algExD nat unit
+> > allnc m,k(exd n^ n^=m -> all n^(n^=m -> k=) -> k=)
+> > "exd n^ n^ =m"
+> > allnc m all n^(n^=m -> exd n^ n^=m)
+> > allnc m,k(exd n^ n^=m -> all n^(n^=m -> k=) -> k=)
+> ; ok, inductively defined predicate constant PiOne added
+> > "(PiOne (cterm (x^,x^) R x^ x^))"
+> > all x^,y^(R x^ y^ -> (PiOne (cterm (x^,x^) R x^ x^))x^)
+> > alpha=>alpha=>alpha=>algPiOne alpha alpha
+> > allnc x^,k(
+ (PiOne (cterm (x^,x^) R x^ x^))x^ ->
+ all x^,y^(R x^ y^ -> k=) -> k=)
+> ; ok, inductively defined predicate constant TrCl added
+> > "(TrCl (cterm (x^,x^) R x^ x^))"
+> > allnc x^,y^(R x^ y^ -> (TrCl (cterm (x^,x^) R x^ x^))x^ y^)
+> > alpha=>algTrCl alpha
+> > allnc x^,x^,k(
+ (TrCl (cterm (x^,x^) R x^ x^))x^ x^ ->
+ allnc x^,y^(R x^ y^ -> k=) ->
+ allnc x^,y^,z^(
+ R x^ y^ ->
+ (TrCl (cterm (x^,x^) R x^ x^))y^ z^ -> k= -> k=) ->
+ k=)
+> ; ok, inductively defined predicate constant Acc added
+> > > allnc x^(F -> (Acc (cterm (x^,x^) R x^ x^))x^)
+> > algAcc alpha alpha
+> > allnc x^(
+ all y^(R y^ x^ -> (Acc (cterm (x^,x^) R x^ x^))y^) ->
+ (Acc (cterm (x^,x^) R x^ x^))x^)
+> > (alpha=>alpha=>algAcc alpha alpha)=>algAcc alpha alpha
+> > allnc x^,k(
+ (Acc (cterm (x^,x^) R x^ x^))x^ ->
+ allnc x^(F -> k=) ->
+ allnc x^(
+ all y^(R y^ x^ -> (Acc (cterm (x^,x^) R x^ x^))y^) ->
+ all y^(R y^ x^ -> k=) -> k=) ->
+ k=)
+> ; ok, inductively defined predicate constant ExDT added
+> > "exdt n n=m"
+> > allnc m all n(n=m -> exdt n n=m)
+> > nat=>algExDT nat unit
+> > allnc m,k(exdt n n=m -> all n(n=m -> k=) -> k=)
+> ; ok, inductively defined predicate constant Cup added
+> > > all x^(
+ Q x^ -> (Cup (cterm (x^) Q x^) (cterm (x^) Q x^))x^)
+> > all x^(
+ Q x^ -> (Cup (cterm (x^) Q x^) (cterm (x^) Q x^))x^)
+> > alpha=>alpha=>algCup alpha alpha alpha
+> > allnc x^(
+ (Cup (cterm (x^) Q x^) (cterm (x^) Q x^))x^ ->
+ all x^(Q x^ -> P) -> all x^(Q x^ -> P) -> P)
+> > algCup alpha alpha alpha=>
+(alpha=>alpha=>alpha)=>(alpha=>alpha=>alpha)=>alpha
+> ; ok, inductively defined predicate constant Cap added
+> > > all x^(
+ Q x^ ->
+ Q x^ -> (Cap (cterm (x^) Q x^) (cterm (x^) Q x^))x^)
+> > alpha=>alpha=>alpha=>algCap alpha alpha alpha
+> > allnc x^(
+ (Cap (cterm (x^) Q x^) (cterm (x^) Q x^))x^ ->
+ all x^(Q x^ -> Q x^ -> P) -> P)
+> > algCap alpha alpha alpha=>(alpha=>alpha=>alpha=>alpha)=>alpha
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable y is removed
+; ok, variable z is removed
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity)
+; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity alpha)
+; ok, predicate variable R is removed
+; warning: R was default pvariable of arity (arity alpha alpha)
+> ; ok, inductively defined predicate constant EqD removed
+; ok, inductively defined predicate constant OrD removed
+; ok, inductively defined predicate constant ExD removed
+; ok, inductively defined predicate constant PiOne removed
+; ok, inductively defined predicate constant TrCl removed
+; ok, inductively defined predicate constant Acc removed
+; ok, inductively defined predicate constant ExDT removed
+; ok, inductively defined predicate constant Cup removed
+; ok, inductively defined predicate constant Cap removed
+> ; ok, variable x: alpha added
+> allnc alpha^ Equal alpha^ alpha^
+> ; ?_: all boole Equal boole boole
+> ; ok, we now have the new goal
+; ?_: Equal boole boole from
+; boole
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, predicate variable P: (arity alpha) added
+> ; ok, MPUnary has been added as a new global assumption.
+; ok, program constant cMPUnary: alpha=>alpha=>(alpha=>alpha)=>alpha
+; of t-degree and arity added
+; warning: theorem cMPUnaryTotal stating totality missing
+> ; ?_: all x P x
+> ; ok, we now have the new goal
+; ?_: P x from
+; x
+> ; ok, ?_ can be obtained from
+; ?_: Total x -> P x from
+; x x
+
+; ?_: Total x from
+; x x
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity alpha)
+> allnc alpha^,alpha^,alpha^(
+ Equal alpha^ alpha^ -> Equal alpha^ alpha^ -> Equal alpha^ alpha^)
+> ; ?_: all x Equal x x
+> ; ok, we now have the new goal
+; ?_: Equal x x from
+; x
+> ; ok, ?_ can be obtained from
+; ?_: Equal x x from
+; x x
+
+; ?_: Equal x x from
+; x x
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+> ; ok, predicate variable P: (arity nat) added
+> ; ?_: all n P n
+> ; ok, ?_ can be obtained from
+; ?_: all n(P n -> P(Succ n)) from
+; n
+
+; ?_: P from
+; n
+> ; ?_: all n^(E n^ -> P n^)
+> ; ok, ?_ can be obtained from
+; ?_: all n(P n -> P(Succ n)) from
+; n^ :E n^
+
+; ?_: P from
+; n^ :E n^
+> ; ?_: all n^ P n^
+> ; ok, we now have the new goal
+; ?_: P n^ from
+; n^
+> ; ok, ?_ can be obtained from
+; ?_: all n(P n -> P(Succ n)) from
+; n^
+
+; ?_: P from
+; n^
+
+; ?_: E n^ from
+; n^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity nat)
+> ; ok, algebra ordl added
+> ; ok, predicate variable P: (arity ordl) added
+> ; ?_: all ordl P ordl
+> ; ok, ?_ can be obtained from
+; ?_: all (nat=>ordl)_(
+; all n P((nat=>ordl)_ n) -> P(OrdSup(nat=>ordl)_)) from
+; ordl
+
+; ?_: P OrdZero from
+; ordl
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity ordl)
+> ; ok, algebra ordl removed
+; ok, constructor OrdSup removed
+; ok, constructor OrdZero removed
+> ; ok, algebra list added
+> ; ok, predicate variable P: (arity list nat) added
+> ; ok, variable ns: list nat added
+> ; ?_: all ns P ns
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(P ns -> P((Cons nat)n ns)) from
+; ns
+
+; ?_: P(Nil nat) from
+; ns
+> ; ?_: all ns^(SE ns^ -> P ns^)
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(SE ns^ -> P ns^ -> P((Cons nat)n^ ns^)) from
+; ns^ :SE ns^
+
+; ?_: P(Nil nat) from
+; ns^ :SE ns^
+> ; ?_: all ns^(STotal ns^ -> P ns^)
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(SE ns^ -> P ns^ -> P((Cons nat)n^ ns^)) from
+; ns^ :SE ns^
+
+; ?_: P(Nil nat) from
+; ns^ :SE ns^
+> ; ?_: all ns^ P ns^
+> ; ok, we now have the new goal
+; ?_: P ns^ from
+; ns^
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(SE ns^ -> P ns^ -> P((Cons nat)n^ ns^)) from
+; ns^
+
+; ?_: P(Nil nat) from
+; ns^
+
+; ?_: SE ns^ from
+; ns^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity list nat)
+> ; ok, variable ns is removed
+; warning: ns was default variable of type list nat
+> ; ok, predicate variable P: (arity list alpha) added
+> ; ok, variable x: alpha added
+> ; ok, variable xs: list alpha added
+> ; ?_: all xs P xs
+> ; ok, ?_ can be obtained from
+; ?_: all x,xs(P xs -> P((Cons alpha)x xs)) from
+; xs
+
+; ?_: P(Nil alpha) from
+; xs
+> ; ?_: all xs^(SE xs^ -> P xs^)
+> ; ok, ?_ can be obtained from
+; ?_: all x^,xs^(
+; SE xs^ -> P xs^ -> P((Cons alpha)x^ xs^)) from
+; xs^ :SE xs^
+
+; ?_: P(Nil alpha) from
+; xs^ :SE xs^
+> ; ?_: all xs^(STotal xs^ -> P xs^)
+> ; ok, ?_ can be obtained from
+; ?_: all x^,xs^(
+; SE xs^ -> P xs^ -> P((Cons alpha)x^ xs^)) from
+; xs^ :SE xs^
+
+; ?_: P(Nil alpha) from
+; xs^ :SE xs^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity list alpha)
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable xs is removed
+; warning: xs was default variable of type list alpha
+> ; ok, algebra list removed
+; ok, constructor Cons removed
+; ok, constructor Nil removed
+> ; ok, algebra tree added
+; ok, algebra tlist added
+> ; ok, predicate variable P: (arity tree) added
+> ; ok, predicate variable Q: (arity tlist) added
+> ; ?_: all tree P tree
+> ; ok, ?_ can be obtained from
+; ?_: all tree,tlist(
+; P tree -> Q tlist -> Q(Tcons tree tlist)) from
+; tree
+
+; ?_: Q Empty from
+; tree
+
+; ?_: all tlist(Q tlist -> P(Branch tlist)) from
+; tree
+
+; ?_: P Leaf from
+; tree
+> ; ?_: all tree^(STotal tree^ -> P tree^)
+> ; ok, ?_ can be obtained from
+; ?_: all tree,tlist(
+; P tree -> Q tlist -> Q(Tcons tree tlist)) from
+; tree^ :E tree^
+
+; ?_: Q Empty from
+; tree^ :E tree^
+
+; ?_: all tlist(Q tlist -> P(Branch tlist)) from
+; tree^ :E tree^
+
+; ?_: P Leaf from
+; tree^ :E tree^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity tree)
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity tlist)
+> ; ok, algebra tree removed
+; ok, algebra tlist removed
+; ok, constructor Tcons removed
+; ok, constructor Empty removed
+; ok, constructor Branch removed
+; ok, constructor Leaf removed
+> ; ok, algebra inftree added
+; ok, algebra inftlist added
+> ; ok, predicate variable P: (arity inftree) added
+> ; ok, predicate variable Q: (arity inftlist) added
+> ; ?_: all inftree P inftree
+> ; ok, ?_ can be obtained from
+; ?_: all inftree,inftlist(
+; P inftree ->
+; Q inftlist -> Q(Inftcons inftree inftlist)) from
+; inftree
+
+; ?_: Q Emptyinftlist from
+; inftree
+
+; ?_: all boole,(boole=>inftree)_(
+; all boole P((boole=>inftree)_ boole) ->
+; P(Lim boole(boole=>inftree)_)) from
+; inftree
+
+; ?_: all boole,inftlist(
+; Q inftlist -> P(Infbranch boole inftlist)) from
+; inftree
+
+; ?_: all boole P(Newleaf boole) from
+; inftree
+> ; ?_: all inftree^(STotal inftree^ -> P inftree^)
+> ; ok, ?_ can be obtained from
+; ?_: all inftree^,inftlist^(
+; STotal inftree^ ->
+; STotal inftlist^ ->
+; P inftree^ ->
+; Q inftlist^ -> Q(Inftcons inftree^ inftlist^)) from
+; inftree^ :STotal inftree^
+
+; ?_: Q Emptyinftlist from
+; inftree^ :STotal inftree^
+
+; ?_: all boole^,(boole=>inftree)^(
+; SE boole^ ->
+; all boole STotal((boole=>inftree)^ boole) ->
+; all boole P((boole=>inftree)^ boole) ->
+; P(Lim boole^(boole=>inftree)^)) from
+; inftree^ :STotal inftree^
+
+; ?_: all boole^,inftlist^(
+; SE boole^ ->
+; STotal inftlist^ ->
+; Q inftlist^ -> P(Infbranch boole^ inftlist^)) from
+; inftree^ :STotal inftree^
+
+; ?_: all boole^(SE boole^ -> P(Newleaf boole^)) from
+; inftree^ :STotal inftree^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity inftree)
+; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity inftlist)
+> ; ok, algebra inftree removed
+; ok, algebra inftlist removed
+; ok, constructor Inftcons removed
+; ok, constructor Emptyinftlist removed
+; ok, constructor Lim removed
+; ok, constructor Infbranch removed
+; ok, constructor Newleaf removed
+> ; ok, predicate variable P: (arity nat) added
+> ; ?_: all n P n
+> ; ok, ?_ can be obtained from
+; ?_: all n P(Succ n) from
+; n
+
+; ?_: P from
+; n
+> ; ?_: all n^(E n^ -> P n^)
+> ; ok, ?_ can be obtained from
+; ?_: all n P(Succ n) from
+; n^ :E n^
+
+; ?_: P from
+; n^ :E n^
+> ; ?_: all n^ P n^
+> ; ok, we now have the new goal
+; ?_: P n^ from
+; n^
+> ; ok, ?_ can be obtained from
+; ?_: all n(Equal n^(Succ n) -> P(Succ n)) from
+; n^
+
+; ?_: Equal n^ -> P from
+; n^
+
+; ?_: E n^ from
+; n^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity nat)
+> ; ok, algebra ordl added
+> ; ok, predicate variable P: (arity ordl) added
+> ; ?_: all ordl P ordl
+> ; ok, ?_ can be obtained from
+; ?_: all (nat=>ordl)_ P(OrdSup(nat=>ordl)_) from
+; ordl
+
+; ?_: P OrdZero from
+; ordl
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity ordl)
+> ; ok, algebra ordl removed
+; ok, constructor OrdSup removed
+; ok, constructor OrdZero removed
+> ; ok, algebra list added
+> ; ok, predicate variable P: (arity list nat) added
+> ; ok, variable ns: list nat added
+> ; ?_: all ns P ns
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns P((Cons nat)n ns) from
+; ns
+
+; ?_: P(Nil nat) from
+; ns
+> ; ?_: all ns^(SE ns^ -> P ns^)
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(SE ns^ -> P((Cons nat)n^ ns^)) from
+; ns^ :SE ns^
+
+; ?_: P(Nil nat) from
+; ns^ :SE ns^
+> ; ?_: all ns^(STotal ns^ -> P ns^)
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(SE ns^ -> P((Cons nat)n^ ns^)) from
+; ns^ :SE ns^
+
+; ?_: P(Nil nat) from
+; ns^ :SE ns^
+> ; ?_: all ns^ P ns^
+> ; ok, we now have the new goal
+; ?_: P ns^ from
+; ns^
+> ; ok, ?_ can be obtained from
+; ?_: all n^,ns^(
+; SE ns^ ->
+; Equal ns^((Cons nat)n^ ns^) -> P((Cons nat)n^ ns^)) from
+; ns^
+
+; ?_: Equal ns^(Nil nat) -> P(Nil nat) from
+; ns^
+
+; ?_: SE ns^ from
+; ns^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity list nat)
+> ; ok, variable ns is removed
+; warning: ns was default variable of type list nat
+> ; ok, predicate variable P: (arity list alpha) added
+> ; ok, variable x: alpha added
+> ; ok, variable xs: list alpha added
+> ; ?_: all xs P xs
+> ; ok, ?_ can be obtained from
+; ?_: all x,xs P((Cons alpha)x xs) from
+; xs
+
+; ?_: P(Nil alpha) from
+; xs
+> ; ?_: all xs^(SE xs^ -> P xs^)
+> ; ok, ?_ can be obtained from
+; ?_: all x^,xs^(SE xs^ -> P((Cons alpha)x^ xs^)) from
+; xs^ :SE xs^
+
+; ?_: P(Nil alpha) from
+; xs^ :SE xs^
+> ; ?_: all xs^(STotal xs^ -> P xs^)
+> ; ok, ?_ can be obtained from
+; ?_: all x^,xs^(SE xs^ -> P((Cons alpha)x^ xs^)) from
+; xs^ :SE xs^
+
+; ?_: P(Nil alpha) from
+; xs^ :SE xs^
+> ; ok, predicate variable P is removed
+; warning: P was default pvariable of arity (arity list alpha)
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable xs is removed
+; warning: xs was default variable of type list alpha
+> ; ok, algebra list removed
+; ok, constructor Cons removed
+; ok, constructor Nil removed
+> ; ?_: all boole^(STotal boole^ -> boole^ =boole^)
+> ; ok, ?_ can be obtained from
+; ?_: False=False from
+; boole^ :E boole^
+
+; ?_: True=True from
+; boole^ :E boole^
+> ; ok, ?_ is proved. The active goal now is
+; ?_: False=False from
+; boole^ :E boole^
+> ; ok, ?_ is proved. Proof finished.
+> ; ?_: all boole^ boole^ =boole^
+> ; ok, we now have the new goal
+; ?_: boole^ =boole^ from
+; boole^
+> ; ok, ?_ can be obtained from
+; ?_: (boole^ -> F) -> False=False from
+; boole^
+
+; ?_: boole^ -> True=True from
+; boole^
+
+; ?_: E boole^ from
+; boole^
+> ; ok, inductively defined predicate constant Even added
+> ; ?_: allnc n^(Even n^ -> ex m n^ =m+m)
+> ; ok, we now have the new goal
+; ?_: Even n^ -> ex m n^ =m+m from
+; {n^}
+> ; ok, ?_ can be obtained from
+; ?_: allnc n^(Even n^ -> ex m n^ =m+m -> ex m n^ +=m+m) from
+; {n^} :Even n^
+
+; ?_: ex m =m+m from
+; {n^} :Even n^
+> ; ok, ?_ can be obtained from
+; ?_: =+ from
+; {n^} :Even n^
+> ; ok, ?_ is proved. The active goal now is
+; ?_: allnc n^(Even n^ -> ex m n^ =m+m -> ex m n^ +=m+m) from
+; {n^} :Even n^
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m from
+; {n^} :Even n^
+; {n^} Even n^:Even n^
+; IH:ex m n^=m+m
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m from
+; {n^} :Even n^
+; {n^} Even n^:Even n^
+; m n^=m+m:n^=m+m
+> ; ok, ?_ can be obtained from
+; ?_: n^+=m++(m+) from
+; {n^} :Even n^
+; {n^} Even n^:Even n^
+; m n^=m+m:n^=m+m
+> ; ok, the normalized goal is
+; ?_: n^=m+m from
+; {n^} :Even n^
+; {n^} Even n^:Even n^
+; m n^=m+m:n^=m+m
+> ; ok, ?_ is proved. Proof finished.
+> > > [algEven](Rec algEven=>nat)algEven ([algEven]Succ)
+> ; ok, inductively defined predicate constant Even removed
+> ; ok, inductively defined predicate constant Ev added
+; ok, inductively defined predicate constant Od added
+> ; ?_: allnc n^(Ev n^ -> ex m n^ =m+m)
+> ; ok, we now have the new goal
+; ?_: Ev n^ -> ex m n^ =m+m from
+; {n^}
+> ; ok, ?_ can be obtained from
+; ?_: allnc n^(Ev n^ -> ex m n^ =m+m -> ex m n^ +=m+m+) from
+; {n^} :Ev n^
+
+; ?_: allnc n^(Od n^ -> ex m n^ =m+m+ -> ex m n^ +=m+m) from
+; {n^} :Ev n^
+
+; ?_: ex m =m+m from
+; {n^} :Ev n^
+> ; ok, ?_ can be obtained from
+; ?_: =+ from
+; {n^} :Ev n^
+> ; ok, ?_ is proved. The active goal now is
+; ?_: allnc n^(Od n^ -> ex m n^ =m+m+ -> ex m n^ +=m+m) from
+; {n^} :Ev n^
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m from
+; {n^} :Ev n^
+; {n^} Od n^:Od n^
+; H:ex m n^=m+m+
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m from
+; {n^} :Ev n^
+; {n^} Od n^:Od n^
+; m H:n^=m+m+
+> ; ok, ?_ can be obtained from
+; ?_: n^+=Succ m+Succ m from
+; {n^} :Ev n^
+; {n^} Od n^:Od n^
+; m H:n^=m+m+
+> ; ok, ?_ is proved. The active goal now is
+; ?_: allnc n^(Ev n^ -> ex m n^ =m+m -> ex m n^ +=m+m+) from
+; {n^} :Ev n^
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m+ from
+; {n^} :Ev n^
+; {n^} Ev n^:Ev n^
+; H:ex m n^=m+m
+> ; ok, we now have the new goal
+; ?_: ex m n^+=m+m+ from
+; {n^} :Ev n^
+; {n^} Ev n^:Ev n^
+; m H:n^=m+m
+> ; ok, ?_ can be obtained from
+; ?_: n^+=m+m+ from
+; {n^} :Ev n^
+; {n^} Ev n^:Ev n^
+; m H:n^=m+m
+> ; ok, ?_ is proved. Proof finished.
+> > > [algEv](Rec algEv=>nat algOd=>nat)algEv ([algOd]Succ)([algEv,n]n)
+> ; ok, inductively defined predicate constant Ev removed
+; ok, inductively defined predicate constant Od removed
+> ; ok, variable x: alpha added
+; ok, variable y: alpha added
+; ok, variable z: alpha added
+> ; ok, predicate variable Q: (arity alpha) added
+> ; ok, inductively defined predicate constant EqD added
+> ; ?_: all x^ x^ eqd x^
+> ; ok, we now have the new goal
+; ?_: x^ eqd x^ from
+; x^
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, EqDRefl has been added as a new theorem.
+> ; ?_: all x^,y^(x^ eqd y^ -> Q x^ -> Q y^)
+> ; ok, we now have the new goal
+; ?_: x^ eqd y^ -> Q x^ -> Q y^ from
+; x^ y^
+> ; ok, ?_ can be obtained from
+; ?_: allnc x^(Q x^ -> Q x^) from
+; x^ y^ :x^ eqd y^
+> ; ok, we now have the new goal
+; ?_: Q x^ from
+; x^ y^ :x^ eqd y^
+; {x^} H:Q x^
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, EqDCompat has been added as a new theorem.
+; ok, program constant cEqDCompat: alpha=>alpha=>alpha=>alpha
+; of t-degree and arity added
+> ; ?_: all x^,y^(x^ eqd y^ -> y^ eqd x^)
+> ; ok, we now have the new goal
+; ?_: y^ eqd x^ from
+; x^ y^ H:x^ eqd y^
+> ; ok, ?_ can be obtained from
+; ?_: x^ eqd x^ from
+; x^ y^ H:x^ eqd y^
+
+; ?_: x^ eqd y^ from
+; x^ y^ H:x^ eqd y^
+> ; ok, ?_ is proved. The active goal now is
+; ?_: x^ eqd x^ from
+; x^ y^ H:x^ eqd y^
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, EqDSym has been added as a new theorem.
+> ; ?_: all x^,y^,z^(x^ eqd y^ -> y^ eqd z^ -> x^ eqd z^)
+> ; ok, we now have the new goal
+; ?_: y^ eqd z^ -> x^ eqd z^ from
+; x^ y^ z^ H:x^ eqd y^
+> ; ok, ?_ can be obtained from
+; ?_: x^ eqd z^ -> x^ eqd z^ from
+; x^ y^ z^ H:x^ eqd y^
+
+; ?_: x^ eqd y^ from
+; x^ y^ z^ H:x^ eqd y^
+> ; ok, ?_ is proved. The active goal now is
+; ?_: x^ eqd z^ -> x^ eqd z^ from
+; x^ y^ z^ H:x^ eqd y^
+> ; ok, we now have the new goal
+; ?_: x^ eqd z^ from
+; x^ y^ z^ H:x^ eqd y^
+; H:x^ eqd z^
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, EqDTrans has been added as a new theorem.
+> ; ?_: all x^,y^(False eqd True -> x^ eqd y^)
+> ; ok, we now have the new goal
+; ?_: x^ eqd y^ from
+; x^ y^ FF:False eqd True
+> ; ok, ?_ can be obtained from
+; ?_: [if False x^ y^]eqd[if False x^ y^] from
+; x^ y^ FF:False eqd True
+
+; ?_: False eqd True from
+; x^ y^ FF:False eqd True
+> ; ok, ?_ is proved. The active goal now is
+; ?_: [if False x^ y^]eqd[if False x^ y^] from
+; x^ y^ FF:False eqd True
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, EFEdD has been added as a new theorem.
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable y is removed
+; ok, variable z is removed
+> ; ok, predicate variable Q is removed
+; warning: Q was default pvariable of arity (arity alpha)
+> ; ok, inductively defined predicate constant EqD removed
+> ; ok, inductively defined predicate constant Even added
+> ; ?_: all n(Even(Succ(Succ n)) -> Even n)
+> ; ok, we now have the new goal
+; ?_: Even n from
+; n H:Even(Succ(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: allnc n^(
+; Even n^ ->
+; (Succ(Succ n)=n^ -> Even n) -> Succ(Succ n)=n^ + -> Even n) from
+; n H:Even(Succ(Succ n))
+> ; ok, we now have the new goal
+; ?_: Even m^ -> (Succ(Succ n)=m^ -> Even n) -> Succ(Succ n)=m^ + -> Even n from
+; n H:Even(Succ(Succ n))
+; {m^}
+> ; ok, the normalized goal is
+; ?_: Even m^ -> (Succ(Succ n)=m^ -> Even n) -> n=m^ -> Even n from
+; n H:Even(Succ(Succ n))
+; {m^}
+> ; ok, we now have the new goal
+; ?_: Even n from
+; n H:Even(Succ(Succ n))
+; {m^} Even m^:Even m^
+; H:Succ(Succ n)=m^ -> Even n
+; n=m^:n=m^
+> ; ok, ?_ can be obtained from
+; ?_: Even m^ from
+; n H:Even(Succ(Succ n))
+; {m^} Even m^:Even m^
+; H:Succ(Succ n)=m^ -> Even n
+; n=m^:n=m^
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, inductively defined predicate constant Even removed
+> > > loading list.scm ...
+> > ; ok, variable l: nat added
+> ; ok, algebra type added
+> > > ; ok, variable rho: type added
+; ok, variable sig: type added
+; ok, variable tau: type added
+> ; ok, program constant Argtyp: type=>type
+; of t-degree and arity added
+; warning: theorem ArgtypTotal stating totality missing
+> ; ok, program constant Valtyp: type=>type
+; of t-degree and arity added
+; warning: theorem ValtypTotal stating totality missing
+> ; ok, program constant Arrowtyp: type=>boole
+; of t-degree and arity added
+; warning: theorem ArrowtypTotal stating totality missing
+> ; ok, computation rule Argtyp Iota -> Iota added
+> ; ok, computation rule Valtyp Iota -> Iota added
+> ; ok, computation rule Argtyp(rho to sig) -> rho added
+> ; ok, computation rule Valtyp(rho to sig) -> sig added
+> ; ok, computation rule Arrowtyp Iota -> False added
+> ; ok, computation rule Arrowtyp(rho to sig) -> True added
+> ; ok, algebra term added
+> > > ; ok, variable r: term added
+; ok, variable s: term added
+; ok, variable t: term added
+> ; ok, variable rs: list term added
+; ok, variable ss: list term added
+; ok, variable ts: list term added
+> ; ok, variable rhos: list type added
+; ok, variable sigs: list type added
+; ok, variable taus: list type added
+> ; ok, program constant Typ: list type=>term=>type
+; of t-degree and arity added
+; warning: theorem TypTotal stating totality missing
+> ; ok, computation rule Typ(Nil type)(Var n) -> Iota added
+> ; ok, computation rule Typ(rho::rhos)(Var ) -> rho added
+> ; ok, computation rule Typ(rho::rhos)(Var(Succ n)) -> Typ rhos(Var n) added
+> ; ok, computation rule Typ rhos(r s) -> Valtyp(Typ rhos r) added
+> ; ok, computation rule Typ rhos(Abs rho r) -> rho to Typ(rho::rhos)r added
+> ; ok, program constant Cor: list type=>term=>boole
+; of t-degree and arity added
+; warning: theorem CorTotal stating totality missing
+> ; ok, computation rule Cor rhos(Var n) -> n<Lh rhos added
+> ; ok, computation rule Cor rhos(r s) -> Cor rhos r andb Cor rhos s andb Typ rhos r=(Typ rhos s to Valtyp(Typ rhos r)) added
+> ; ok, computation rule Cor rhos(Abs rho r) -> Cor(rho::rhos)r added
+> ; ok, program constant Lift: term=>nat=>nat=>term
+; of t-degree and arity added
+; warning: theorem LiftTotal stating totality missing
+> ; ok, computation rule Lift(Var n)l k -> [if (n<l) (Var n) (Var(n+k))] added
+> ; ok, computation rule Lift(r s)l k -> Lift r l k(Lift s l k) added
+> ; ok, computation rule Lift(Abs rho r)l k -> Abs rho(Lift r(l+)k) added
+> ; ok, algebra sub added
+> ; ok, variable theta: sub added
+> ; ok, program constant Sublift: sub=>nat=>sub
+; of t-degree and arity added
+; warning: theorem SubliftTotal stating totality missing
+> ; ok, computation rule Sublift(Up m)n -> Up(m+n) added
+> ; ok, computation rule Sublift(Dot r theta)n -> Dot(Lift r n)(Sublift theta n) added
+> ; ok, program constant Mksub: list term=>nat=>sub
+; of t-degree and arity added
+; warning: theorem MksubTotal stating totality missing
+> ; ok, computation rule Mksub(Nil term)n -> Up n added
+> ; ok, computation rule Mksub(r::rs)n -> Dot r(Mksub rs n) added
+> ; ok, program constant Sublist: sub=>list term
+; of t-degree and arity added
+; warning: theorem SublistTotal stating totality missing
+> ; ok, computation rule Sublist(Up n) -> (Nil term) added
+> ; ok, computation rule Sublist(Dot r theta) -> r::Sublist theta added
+> ; ok, program constant Subup: sub=>nat
+; of t-degree and arity added
+; warning: theorem SubupTotal stating totality missing
+> ; ok, computation rule Subup(Up n) -> n added
+> ; ok, computation rule Subup(Dot r theta) -> Subup theta added
+> ; ok, program constant Sub: term=>sub=>term
+; of t-degree and arity added
+; warning: theorem SubTotal stating totality missing
+> ; ok, computation rule Sub(Var n)(Up m) -> Var(n+m) added
+> ; ok, computation rule Sub(Var )(Dot r theta) -> r added
+> ; ok, computation rule Sub(Var(Succ n))(Dot r theta) -> Sub(Var n)theta added
+> ; ok, computation rule Sub(r s)theta -> Sub r theta(Sub s theta) added
+> ; ok, computation rule Sub(Abs rho r)theta -> Abs rho(Sub r(Dot(Var )(Sublift theta ))) added
+> ; ok, program constant Wrap: nat=>list term=>sub
+; of t-degree and arity added
+; warning: theorem WrapTotal stating totality missing
+> ; ok, computation rule Wrap n(Nil term) -> Up n added
+> ; ok, computation rule Wrap n(r::rs) -> Dot r(Wrap n rs) added
+> ; ok, program constant Eta: type=>term=>term
+; of t-degree and arity added
+; warning: theorem EtaTotal stating totality missing
+> ; ok, computation rule Eta Iota r -> r added
+> ; ok, computation rule Eta(rho to sig)r -> Abs rho(Eta sig(Lift r (Eta rho(Var )))) added
+> Abs Iota(Var (Var ))
+> Abs Iota(Var (Var ))
+> Abs(Iota to Iota)(Abs Iota(Var (Abs Iota(Var (Var )))(Var )))
+> ; ok, program constant Exp: list type=>type=>term=>term
+; of t-degree and arity added
+; warning: theorem ExpTotal stating totality missing
+> ; ok, program constant IExp: list type=>term=>term
+; of t-degree and arity added
+; warning: theorem IExpTotal stating totality missing
+> ; ok, computation rule Exp rhos rho(Var n) -> Eta rho(Var n) added
+> ; ok, computation rule Exp rhos rho(r s) -> Eta rho(IExp rhos(r s)) added
+> ; ok, computation rule Exp rhos tau(Abs rho r) -> Abs rho(Exp(rho::rhos)(Valtyp tau)r) added
+> ; ok, computation rule IExp rhos(Var n) -> Var n added
+> ; ok, computation rule IExp rhos(r s) -> IExp rhos r(Exp rhos(Typ rhos s)s) added
+> Abs rho(Abs sig(Var ))
+> Abs(rho to sig to rho)(Abs(rho to sig)(Abs rho(Var (Var )(Var (Var )))))
+> > > Typ(Nil type)
+(Abs((Iota to Iota)to Iota to Iota to Iota)
+ (Abs((Iota to Iota)to Iota)(Abs(Iota to Iota)(Var (Var )(Var (Var ))))))
+> ((Iota to Iota)to Iota to Iota to Iota)to
+((Iota to Iota)to Iota)to(Iota to Iota)to Iota to Iota
+> Abs((Iota to Iota)to Iota to Iota to Iota)
+(Abs((Iota to Iota)to Iota)
+ (Abs(Iota to Iota)
+ (Abs Iota
+ (Var (Abs Iota(Var (Var )))(Var (Abs Iota(Var (Var ))))(Var )))))
+> ; ok, program constant FoldApp: term=>list term=>term
+; of t-degree and arity added
+; warning: theorem FoldAppTotal stating totality missing
+> ; ok, computation rule FoldApp r(Nil term) -> r added
+> ; ok, computation rule FoldApp r(s::ss) -> FoldApp(r s)ss added
+> ; ok, inductively defined predicate constant WN added
+; ok, inductively defined predicate constant WNs added
+> ; ?_: all r,s,rs,ss(WNs(r::rs)(s::ss) -> WNs rs ss)
+> ; ok, we now have the new goal
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+> ; ok, ?_ can be obtained from
+; ?_: all r,s,rs,ss(
+; WNs rs ss ->
+; ((r::rs)=rs -> (s::ss)=ss -> WNs rs ss) ->
+; (r::rs)=(r::rs) -> (s::ss)=(s::ss) -> WNs rs ss) from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+> ; ok, we now have the new goal
+; ?_: WNs rs ss ->
+; ((r::rs)=rs -> (s::ss)=ss -> WNs rs ss) ->
+; (r::rs)=(r::rs) -> (s::ss)=(s::ss) -> WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss
+> ; ok, we now have the new goal
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):(r::rs)=(r::rs)
+; (s::ss)=(s::ss):(s::ss)=(s::ss)
+> ; ok, the normalized goal is
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):r=r andb rs=rs
+; (s::ss)=(s::ss):s=s andb ss=ss
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):r=r andb rs=rs
+; (s::ss)=(s::ss):s=s andb ss=ss
+; rs=rs:rs=rs
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):r=r andb rs=rs
+; (s::ss)=(s::ss):s=s andb ss=ss
+; rs=rs:rs=rs
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):r=r andb rs=rs
+; (s::ss)=(s::ss):s=s andb ss=ss
+; rs=rs:rs=rs
+; ss=ss:ss=ss
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; r s rs ss WNs(r::rs)(s::ss):
+; WNs(r::rs)(s::ss)
+; r s rs ss WNs rs ss:
+; WNs rs ss
+; H:(r::rs)=rs -> (s::ss)=ss -> WNs rs ss
+; (r::rs)=(r::rs):r=r andb rs=rs
+; (s::ss)=(s::ss):s=s andb ss=ss
+; rs=rs:rs=rs
+; ss=ss:ss=ss
+> ; ok, ?_ is proved. Proof finished.
+> > [r,s,rs,ss,algWNs]
+ (Rec algWNs=>algWNs)algWNs cWNsNil
+ ([r,s,rs,ss,algWNs,algWNs]
+ ([algWNs]algWNs)(([algWNs]algWNs)algWNs))
+> ; ?_: all r,rs,ss(WNs(r::rs)ss -> ss=(Nil term) -> F)
+> ; ok, we now have the new goal
+; ?_: ss=(Nil term) -> F from
+; r rs ss H:WNs(r::rs)ss
+> ; ok, ?_ can be obtained from
+; ?_: all r,s,rs,ss(
+; WNs rs ss ->
+; ((r::rs)=rs -> ss=ss -> ss=(Nil term) -> F) ->
+; (r::rs)=(r::rs) -> ss=(s::ss) -> ss=(Nil term) -> F) from
+; r rs ss H:WNs(r::rs)ss
+> ; ok, we now have the new goal
+; ?_: ss=(Nil term) -> F from
+; r rs ss H:WNs(r::rs)ss
+; r s rs ss H:WNs rs ss
+; H:(r::rs)=rs -> ss=ss -> ss=(Nil term) -> F
+; H:(r::rs)=(r::rs)
+; H:ss=(s::ss)
+> ; ok, ?_ can be obtained from
+; ?_: (s::ss)=(Nil term) -> F from
+; r rs ss H:WNs(r::rs)ss
+; r s rs ss H:WNs rs ss
+; H:(r::rs)=rs -> ss=ss -> ss=(Nil term) -> F
+; H:(r::rs)=(r::rs)
+; H:ss=(s::ss)
+> ; ok, ?_ is proved in minimal propositional logic. Proof finished.
+> ; ?_: all rs,ss(WNs rs ss -> rs=(Nil term) -> ss=(Nil term))
+> ; ok, we now have the new goal
+; ?_: WNs rs ss -> rs=(Nil term) -> ss=(Nil term) from
+; rs ss
+> ; ok, ?_ can be obtained from
+; ?_: all r,s,rs,ss(
+; WNs rs ss ->
+; (rs=(Nil term) -> ss=(Nil term)) ->
+; (r::rs)=(Nil term) -> (s::ss)=(Nil term)) from
+; rs ss :WNs rs ss
+
+; ?_: (Nil term)=(Nil term) -> (Nil term)=(Nil term) from
+; rs ss :WNs rs ss
+> ; ok, ?_ is proved in minimal propositional logic. The active goal now is
+; ?_: all r,s,rs,ss(
+; WNs rs ss ->
+; (rs=(Nil term) -> ss=(Nil term)) ->
+; (r::rs)=(Nil term) -> (s::ss)=(Nil term)) from
+; rs ss :WNs rs ss
+> ; ok, we now have the new goal
+; ?_: (s::ss)=(Nil term) from
+; rs ss :WNs rs ss
+; r s rs ss :
+; WNs rs ss
+; :rs=(Nil term) -> ss=(Nil term)
+; :(r::rs)=(Nil term)
+> ; ok, ?_ is proved in minimal propositional logic. Proof finished.
+> ; ?_: all ss(WNs(Nil term)ss -> ss=(Nil term))
+> ; ok, we now have the new goal
+; ?_: ss=(Nil term) from
+; ss H:WNs(Nil term)ss
+> ; ok, ?_ can be obtained from
+; ?_: (Nil term)=(Nil term) -> ss=(Nil term) -> ss=(Nil term) from
+; ss H:WNs(Nil term)ss
+> ; ok, ?_ is proved in minimal propositional logic. Proof finished.
+> ; ?_: all rs,ss,rs,ss(
+; WNs rs ss -> WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+> ; ok, ?_ can be obtained from
+; ?_: all r,rs(
+; all ss,rs,ss(
+; WNs rs ss -> WNs rs ss -> WNs(rs:+:rs)(ss:+:ss)) ->
+; all ss,rs,ss(
+; WNs(r::rs)ss ->
+; WNs rs ss -> WNs((r::rs):+:rs)(ss:+:ss))) from
+; rs
+
+; ?_: all ss,rs,ss(
+; WNs(Nil term)ss -> WNs rs ss -> WNs((Nil term):+:rs)(ss:+:ss)) from
+; rs
+> ; ok, ?_ can be obtained from
+; ?_: all r,rs,rs,ss(
+; WNs(Nil term)(r::rs) ->
+; WNs rs ss -> WNs((Nil term):+:rs)((r::rs):+:ss)) from
+; rs ss
+
+; ?_: all rs,ss(
+; WNs(Nil term)(Nil term) ->
+; WNs rs ss -> WNs((Nil term):+:rs)((Nil term):+:ss)) from
+; rs ss
+> ; ok, we now have the new goal
+; ?_: WNs((Nil term):+:rs)((Nil term):+:ss) from
+; rs ss rs ss :
+; WNs(Nil term)(Nil term)
+; :WNs rs ss
+> ; ok, the normalized goal is
+; ?_: WNs rs ss from
+; rs ss rs ss :
+; WNs(Nil term)(Nil term)
+; :WNs rs ss
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all r,rs,rs,ss(
+; WNs(Nil term)(r::rs) ->
+; WNs rs ss -> WNs((Nil term):+:rs)((r::rs):+:ss)) from
+; rs ss
+> ; ok, we now have the new goal
+; ?_: WNs((Nil term):+:rs)((r::rs):+:ss) from
+; rs ss r rs rs ss :
+; WNs(Nil term)(r::rs)
+; :WNs rs ss
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all r,rs(
+; all ss,rs,ss(
+; WNs rs ss -> WNs rs ss -> WNs(rs:+:rs)(ss:+:ss)) ->
+; all ss,rs,ss(
+; WNs(r::rs)ss ->
+; WNs rs ss -> WNs((r::rs):+:rs)(ss:+:ss))) from
+; rs
+> ; ok, we now have the new goal
+; ?_: all ss,rs,ss(
+; WNs(r::rs)ss -> WNs rs ss -> WNs((r::rs):+:rs)(ss:+:ss)) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+> ; ok, ?_ can be obtained from
+; ?_: all r,rs,rs,ss(
+; WNs(r::rs)(r::rs) ->
+; WNs rs ss -> WNs((r::rs):+:rs)((r::rs):+:ss)) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss
+
+; ?_: all rs,ss(
+; WNs(r::rs)(Nil term) ->
+; WNs rs ss -> WNs((r::rs):+:rs)((Nil term):+:ss)) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss
+> ; ok, we now have the new goal
+; ?_: WNs((r::rs):+:rs)((Nil term):+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss rs ss :WNs(r::rs)(Nil term)
+; :WNs rs ss
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all r,rs,rs,ss(
+; WNs(r::rs)(r::rs) ->
+; WNs rs ss -> WNs((r::rs):+:rs)((r::rs):+:ss)) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss
+> ; ok, we now have the new goal
+; ?_: WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+> ; ok, ?_ can be obtained from
+; ?_: all r,s,rs,ss(
+; WN r s ->
+; WNs rs ss ->
+; WN r s ->
+; ((r::rs)=rs ->
+; (s::ss)=ss ->
+; WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss)) ->
+; (r::rs)=(r::rs) ->
+; (s::ss)=(s::ss) ->
+; WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss)) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+> ; ok, we now have the new goal
+; ?_: WN r s ->
+; WNs rs ss ->
+; WN r s ->
+; ((r::rs)=rs ->
+; (s::ss)=ss ->
+; WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss)) ->
+; (r::rs)=(r::rs) ->
+; (s::ss)=(s::ss) ->
+; WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss
+> ; ok, we now have the new goal
+; ?_: WNs((r::rs):+:rs)((s::ss):+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs((r::rs):+:rs)((s::ss):+:ss)
+; :(r::rs)=(r::rs)
+; :(s::ss)=(s::ss)
+; :WNs rs ss
+> ; ok, the normalized goal is
+; ?_: WNs(r::rs:+:rs)(s::ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+> ; ok, ?_ can be obtained from
+; ?_: WNs(r::rs:+:rs)(s::ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+> ; ok, ?_ can be obtained from
+; ?_: WNs(r::rs:+:rs)(s::ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+> ; ok, ?_ can be obtained from
+; ?_: WNs(r::rs:+:rs)(s::ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ can be obtained from
+; ?_: WNs(r::rs:+:rs)(s::ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ can be obtained from
+; ?_: WNs(rs:+:rs)(ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+
+; ?_: WN r s from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ is proved. The active goal now is
+; ?_: WNs(rs:+:rs)(ss:+:ss) from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+; rs=rs:rs=rs
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+; rs=rs:rs=rs
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+; rs=rs:rs=rs
+; ss=ss:ss=ss
+> ; ok, ?_ can be obtained from
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+; rs=rs:rs=rs
+; ss=ss:ss=ss
+> ; ok, ?_ is proved. The active goal now is
+; ?_: WNs rs ss from
+; rs r rs IH:all ss,rs,ss(WNs rs ss ->
+; WNs rs ss -> WNs(rs:+:rs)(ss:+:ss))
+; ss s ss rs ss H:
+; WNs(r::rs)(s::ss)
+; r s rs ss :WN r s
+; :WNs rs ss
+; :WN r s
+; :(r::rs)=rs ->
+; (s::ss)=ss -> WNs rs ss -> WNs(r::rs:+:rs)(s::ss:+:ss)
+; :r=r andb rs=rs
+; :s=s andb ss=ss
+; :WNs rs ss
+; r=r:r=r
+; s=s:s=s
+> ; ok, ?_ is proved. Proof finished.
+> ; ok, inductively defined predicate constant H added
+> ; ?_: all r,s(WN r s -> H r)
+> ; ok, we now have the new goal
+; ?_: WN r s -> H r from
+; r s
+> ; ok, ?_ can be obtained from
+; ?_: all rho,r,s,t,rs(
+; WN(FoldApp(Sub r(Wrap s:))rs)t ->
+; H(FoldApp(Sub r(Wrap s:))rs) -> H(FoldApp(Abs rho r)(s::rs))) from
+; r s :WN r s
+
+; ?_: all rho,r,s(WN r s -> H r -> H(Abs rho r)) from
+; r s :WN r s
+
+; ?_: all n,rs,ss H(FoldApp(Var n)rs) from
+; r s :WN r s
+> ; ok, we now have the new goal
+; ?_: H(FoldApp(Var n)rs) from
+; r s :WN r s
+; n rs ss
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all rho,r,s(WN r s -> H r -> H(Abs rho r)) from
+; r s :WN r s
+> ; ok, we now have the new goal
+; ?_: H(Abs rho r) from
+; r s :WN r s
+; rho r s :WN r s
+; :H r
+> ; ok, ?_ can be obtained from
+; ?_: H r from
+; r s :WN r s
+; rho r s :WN r s
+; :H r
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all rho,r,s,t,rs(
+; WN(FoldApp(Sub r(Wrap s:))rs)t ->
+; H(FoldApp(Sub r(Wrap s:))rs) -> H(FoldApp(Abs rho r)(s::rs))) from
+; r s :WN r s
+> ; ok, we now have the new goal
+; ?_: H(FoldApp(Abs rho r)(s::rs)) from
+; r s :WN r s
+; rho r s t rs :
+; WN(FoldApp(Sub r(Wrap s:))rs)t
+; :H(FoldApp(Sub r(Wrap s:))rs)
+> ; ok, ?_ can be obtained from
+; ?_: H(FoldApp(Sub r(Wrap s:))rs) from
+; r s :WN r s
+; rho r s t rs :
+; WN(FoldApp(Sub r(Wrap s:))rs)t
+; :H(FoldApp(Sub r(Wrap s:))rs)
+> ; ok, ?_ is proved. Proof finished.
+> > > [r,r,algWN]
+ (Rec algWN=>algH)algWN([n,rs,rs]cHVar n rs)
+ ([rho,r,r,algWN]cHAbs rho r)
+ ([rho,r,r,r,rs,algWN]cHBeta rho r r rs)
+> ; ok, variable l is removed
+; ok, variable rho is removed
+; warning: rho was default variable of type type
+; ok, variable sig is removed
+; ok, variable tau is removed
+; ok, variable r is removed
+; warning: r was default variable of type term
+; ok, variable s is removed
+; ok, variable t is removed
+; ok, variable rs is removed
+; warning: rs was default variable of type list term
+; ok, variable ss is removed
+; ok, variable ts is removed
+; ok, variable rhos is removed
+; warning: rhos was default variable of type list type
+; ok, variable sigs is removed
+; ok, variable taus is removed
+; ok, variable theta is removed
+; warning: theta was default variable of type sub
+> ; ok, algebra type removed
+; ok, constructor cHBeta removed
+; ok, constructor cHAbs removed
+; ok, constructor TwoH removed
+; ok, constructor OneH removed
+; ok, constructor cWNBeta removed
+; ok, constructor cWNAbs removed
+; ok, constructor TwoWN removed
+; ok, constructor OneWN removed
+; ok, constructor Abs removed
+; ok, constructor Arrow removed
+; ok, constructor Iota removed
+; ok, program constant IExp removed
+; ok, program constant Exp removed
+; ok, program constant Eta removed
+; ok, program constant Cor removed
+; ok, program constant Typ removed
+; ok, program constant Arrowtyp removed
+; ok, program constant Valtyp removed
+; ok, program constant Argtyp removed
+; ok, algebra sub removed
+; ok, constructor Dot removed
+; ok, constructor Up removed
+; ok, program constant Wrap removed
+; ok, program constant Sub removed
+; ok, program constant Subup removed
+; ok, program constant Sublist removed
+; ok, program constant Mksub removed
+; ok, program constant Sublift removed
+> ; ok, inductively defined predicate constant H removed
+> ; ok, inductively defined predicate constant WN removed
+; ok, inductively defined predicate constant WNs removed
+> > > > > ; ?_: all n ex n all n(n=n -> n=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n ex n all n(Succ n=n -> n=n) from
+; n
+
+; ?_: ex n all n(=n -> n=n) from
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(=n -> =n) from
+; n
+> ; ok, we now have the new goal
+; ?_: =n from
+; n n u:=n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n ex n all n(Succ n=n -> n=n) from
+; n
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n=n -> n=n) from
+; n n
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n=n -> n=n) from
+; n n
+> ; ok, ?_ can be obtained from
+; ?_: all n(Succ n=n -> Succ n=n) from
+; n n
+> ; ok, we now have the new goal
+; ?_: Succ n=n from
+; n n n u:Succ n=n
+> ; ok, ?_ is proved. Proof finished.
+> [n]
+ ([n,n,(nat=>nat)_][if n n (nat=>nat)_])n
+ (([n]n))
+ ([n]([n]n)(Succ n))
+
+[n]n
+
+[n]
+ ([n]
+ [if n
+ (left(([n]n@([n]n))))
+ ([n]left(([n]n@([n]n))(Succ n)))])
+ n
+
+[n]n
+
+> ; ?_: all n ex n all n(n=n -> n=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(
+; ex n all n(n=n -> n=n) ->
+; ex n all n(Succ n=n -> n=n)) from
+; n
+
+; ?_: ex n all n(=n -> n=n) from
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(=n -> =n) from
+; n
+> ; ok, we now have the new goal
+; ?_: =n from
+; n n u:=n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(
+; ex n all n(n=n -> n=n) ->
+; ex n all n(Succ n=n -> n=n)) from
+; n
+> ; ok, we now have the new goal
+; ?_: ex n all n(n=n -> n=n) -> ex n all n(Succ n=n -> n=n) from
+; n n
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n=n -> n=n) from
+; n n :ex n all n(n=n -> n=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(Succ n=n -> Succ n=n) from
+; n n :ex n all n(n=n -> n=n)
+> ; ok, we now have the new goal
+; ?_: Succ n=n from
+; n n :ex n all n(n=n -> n=n)
+; n u:Succ n=n
+> ; ok, ?_ is proved. Proof finished.
+> [n](Rec nat=>nat)n(([n]n))([n,n]([n]n)(Succ n))
+
+[n]n
+
+[n]
+ ([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]left(([n]n@([n]n))(Succ n)))@
+ ([n,n]))
+ n)))
+ n
+
+[n]n
+
+> ; ?_: all n ex n all n(n=n -> n=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(
+; all n(
+; ([n]n)n<([n]n)n -> ex n all n(n=n -> n=n)) ->
+; ex n all n(n=n -> n=n)) from
+; n
+> ; ok, we now have the new goal
+; ?_: all n(([n]n)n<([n]n)n -> ex n all n(n=n -> n=n)) ->
+; ex n all n(n=n -> n=n) from
+; n n
+> ; ok, we now have the new goal
+; ?_: ex n all n(n=n -> n=n) from
+; n n :all n(([n]n)n<([n]n)n -> ex n all n(n=n -> n=n))
+> ; ok, ?_ can be obtained from
+; ?_: all n(n=n -> n=n) from
+; n n :all n(([n]n)n<([n]n)n -> ex n all n(n=n -> n=n))
+> ; ok, we now have the new goal
+; ?_: n=n from
+; n n :all n(([n]n)n<([n]n)n -> ex n all n(n=n -> n=n))
+; n u:n=n
+> ; ok, ?_ is proved. Proof finished.
+> [n](GRec nat nat)([n]n)n([n,(nat=>nat)_]([n]n)n)
+
+[n]n
+
+[n,n]
+ (GRecGuard nat nat)([n]n)n
+ ([n]
+ left(([n]
+ ([(nat=>nat)_]left(([n]n@([n]n))n))@
+ ([(nat=>nat)_,n]@))
+ n))
+ True
+
+[n,n]n
+
+> ; ?_: all n ex n all n(n<n -> n<=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(
+; ex n all n(n<n -> n<=n) ->
+; ex n all n(Succ n<n -> n<=n)) from
+; n
+
+; ?_: ex n all n(<n -> n<=n) from
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(<n -> <=n) from
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(<Succ n -> <=Succ n) from
+; n n
+
+; ?_: < -> <= from
+; n n
+> ; ok, we now have the new goal
+; ?_: <= from
+; n n u:<
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(<Succ n -> <=Succ n) from
+; n n
+> ; ok, we now have the new goal
+; ?_: <=Succ n from
+; n n n u:<Succ n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(
+; ex n all n(n<n -> n<=n) ->
+; ex n all n(Succ n<n -> n<=n)) from
+; n
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n<n -> n<=n) from
+; n n IH:ex n all n(n<n -> n<=n)
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n<n -> n<=n) from
+; n n n v:all n(n<n -> n<=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(Succ n<n -> Succ n<=n) from
+; n n n v:all n(n<n -> n<=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(Succ n<Succ n -> Succ n<=Succ n) from
+; n n n v:all n(n<n -> n<=n)
+; n
+
+; ?_: Succ n< -> Succ n<= from
+; n n n v:all n(n<n -> n<=n)
+; n
+> ; ok, we now have the new goal
+; ?_: Succ n<= from
+; n n n v:all n(n<n -> n<=n)
+; n u:Succ n<
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(Succ n<Succ n -> Succ n<=Succ n) from
+; n n n v:all n(n<n -> n<=n)
+; n
+> ; ok, we now have the new goal
+; ?_: Succ n<=Succ n from
+; n n n v:all n(n<n -> n<=n)
+; n n u:Succ n<Succ n
+> ; ok, ?_ can be obtained from
+; ?_: n<n from
+; n n n v:all n(n<n -> n<=n)
+; n n u:Succ n<Succ n
+> ; ok, ?_ is proved. Proof finished.
+> [n]
+ (Rec nat=>nat)n(([n]n))
+ ([n,n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+[n]
+ ([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ ([n][if n ([n]n)])
+ (right(([n]n@([n]n))(Succ n))n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ ([n][if n ([n]n)])
+ (right(([n]n@([n]n))(Succ n))n)))
+ n)
+ n))
+ n)))
+ n
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+> ; ?_: all n,n(
+; all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n)) ->
+; all n ex n all n(n<n -> n<=n)
+> ; ok, we now have the new goal
+; ?_: all n ex n all n(n<n -> n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+> ; ok, ?_ can be obtained from
+; ?_: all n(
+; ex n all n(n<n -> n<=n) ->
+; ex n all n(Succ n<n -> n<=n)) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n
+
+; ?_: ex n all n(<n -> n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(<n -> <=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n
+> ; ok, ?_ can be obtained from
+; ?_: all n(<Succ n -> <=Succ n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n
+
+; ?_: < -> <= from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n
+> ; ok, we now have the new goal
+; ?_: <= from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n u:<
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(<Succ n -> <=Succ n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n
+> ; ok, we now have the new goal
+; ?_: <=Succ n from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n n u:<Succ n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(
+; ex n all n(n<n -> n<=n) ->
+; ex n all n(Succ n<n -> n<=n)) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n<n -> n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n IH:ex n all n(n<n -> n<=n)
+> ; ok, we now have the new goal
+; ?_: ex n all n(Succ n<n -> n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n n v:all n(n<n -> n<=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(Succ n<n -> Succ n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n n v:all n(n<n -> n<=n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(n<n -> n<=n) from
+; L:all n,n(all n(n<n -> n<=n) -> all n(Succ n<n -> Succ n<=n))
+; n n n v:all n(n<n -> n<=n)
+> ; ok, ?_ is proved. Proof finished.
+> [n]
+ (Rec nat=>nat)n(([n]n))
+ ([n,n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+([(nat=>nat=>nat=>nat)_,n]
+ ([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))n)))
+ n)
+ n))
+ n)))
+ n)@
+([(nat=>nat=>nat=>nat)_,(nat@@nat)_]
+ ([n]
+ (Rec nat=>nat=>nat@@nat@@nat)n([n]@@)
+ ([n,(nat=>nat@@nat@@nat)_,n]
+ [let (nat@@nat@@nat)_
+ (left(n@
+ ([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n)@
+ left(left right(n@
+ ([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n)@
+ right right(n@
+ ([n]
+ (Rec nat=>nat)n
+ left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n))@
+ right(([n]n@([n]n))
+ (Succ
+ left(left right(n@
+ ([n]
+ (Rec nat=>nat)n
+ left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]
+ n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@
+ ([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]
+ n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@
+ ([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n)@
+ right right(n@
+ ([n]
+ (Rec nat=>nat)n
+ left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]
+ n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@
+ ([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]
+ n@
+ ([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@
+ ([n]
+ n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n))))
+ right(left right(n@
+ ([n]
+ (Rec nat=>nat)n
+ left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]n@([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n)@
+ right right(n@
+ ([n]
+ (Rec nat=>nat)n
+ left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@([n]n))
+ (Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))
+ (Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_
+ n
+ n
+ (right(([n]
+ n@([n]n))
+ (Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n@
+ n)))
+ [if (([(nat@@nat@@nat)_]
+ (left(nat@@nat@@nat)_<
+ (nat=>nat=>nat=>nat)_ left(nat@@nat@@nat)_
+ left right(nat@@nat@@nat)_
+ right right(nat@@nat@@nat)_ impb
+ left right(nat@@nat@@nat)_<=
+ (nat=>nat=>nat=>nat)_ left(nat@@nat@@nat)_
+ left right(nat@@nat@@nat)_
+ right right(nat@@nat@@nat)_)impb
+ Succ left(nat@@nat@@nat)_<right right(nat@@nat@@nat)_ impb
+ Succ left right(nat@@nat@@nat)_<=
+ right right(nat@@nat@@nat)_)
+ (nat@@nat@@nat)_)
+ ((nat=>nat@@nat@@nat)_
+ (right(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))
+ n)))
+ n)
+ n))
+ n)
+ (([n]
+ (Rec nat=>nat)n left(([n]n@([n]n)))
+ ([n]
+ left(([n]
+ ([n]
+ left(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))
+ n)))
+ n))@
+ ([n,n]
+ right(([n]
+ left(([n]n@([n]n))(Succ n))@
+ ([n]
+ (nat=>nat=>nat=>nat)_ n n
+ (right(([n]n@([n]n))(Succ n))
+ n)))
+ n)
+ n))
+ n)))
+ n)
+ n))
+ (nat@@nat@@nat)_]]))
+ left(nat@@nat)_
+ right(nat@@nat)_)
+
+([(nat=>nat=>nat=>nat)_,n](Rec nat=>nat)n ([n]Succ))@
+([(nat=>nat=>nat=>nat)_,(nat@@nat)_]
+ (Rec nat=>nat=>nat@@nat@@nat)left(nat@@nat)_([n]@@)
+ ([n,(nat=>nat@@nat@@nat)_,n]
+ [let (nat@@nat@@nat)_
+ (n@(Rec nat=>nat)n ([n]Succ)@n)
+ [if ((left(nat@@nat@@nat)_<
+ (nat=>nat=>nat=>nat)_ left(nat@@nat@@nat)_
+ left right(nat@@nat@@nat)_
+ right right(nat@@nat@@nat)_ impb
+ left right(nat@@nat@@nat)_<=
+ (nat=>nat=>nat=>nat)_ left(nat@@nat@@nat)_
+ left right(nat@@nat@@nat)_
+ right right(nat@@nat@@nat)_)impb
+ Succ left(nat@@nat@@nat)_<right right(nat@@nat@@nat)_ impb
+ Succ left right(nat@@nat@@nat)_<=right right(nat@@nat@@nat)_)
+ ((nat=>nat@@nat@@nat)_
+ ((nat=>nat=>nat=>nat)_ n((Rec nat=>nat)n ([n]Succ))n))
+ (nat@@nat@@nat)_]])
+ right(nat@@nat)_)
+
+> > minlog-load WARNING: file lib/list.scm already loaded !> > ; ok, variable ns: list nat added
+> ; ?_: all ns ex ns all ns(ns=ns -> ns=ns)
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; ex ns all ns(ns=ns -> ns=ns) ->
+; ex ns all ns((n::ns)=ns -> ns=ns)) from
+; ns
+
+; ?_: ex ns all ns((Nil nat)=ns -> ns=ns) from
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: all ns((Nil nat)=ns -> (Nil nat)=ns) from
+; ns
+> ; ok, we now have the new goal
+; ?_: (Nil nat)=ns from
+; ns ns u:(Nil nat)=ns
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; ex ns all ns(ns=ns -> ns=ns) ->
+; ex ns all ns((n::ns)=ns -> ns=ns)) from
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns all ns(ns=ns -> ns=ns) ->
+; ex ns all ns((n::ns)=ns -> ns=ns) from
+; ns n ns
+> ; ok, we now have the new goal
+; ?_: ex ns all ns((n::ns)=ns -> ns=ns) from
+; ns n ns :ex ns all ns(ns=ns -> ns=ns)
+> ; ok, ?_ can be obtained from
+; ?_: all ns((n::ns)=ns -> (n::ns)=ns) from
+; ns n ns :ex ns all ns(ns=ns -> ns=ns)
+> ; ok, we now have the new goal
+; ?_: (n::ns)=ns from
+; ns n ns :ex ns all ns(ns=ns -> ns=ns)
+; ns u:(n::ns)=ns
+> ; ok, ?_ is proved. Proof finished.
+> [ns]
+ (Rec list nat=>list nat)ns(([ns]ns)(Nil nat))
+ ([n,ns,ns]([ns]ns)(n::ns))
+
+[ns]ns
+
+[ns]
+ ([ns]
+ (Rec list nat=>list nat)ns left(([ns]ns@([ns]ns))(Nil nat))
+ ([n,ns]
+ left(([n,ns]
+ ([ns]left(([ns]ns@([ns]ns))(n::ns)))@
+ ([ns,ns](Nil nat)))
+ n
+ ns)))
+ ns
+
+[ns]ns
+
+> ; ?_: all ns ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns)) from
+; ns
+
+; ?_: ex ns all ns(Lh(Nil nat)<Lh ns -> Lh ns<=Lh ns) from
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: all ns(Lh(Nil nat)<Lh ns -> Lh : <=Lh ns) from
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; Lh(Nil nat)<Lh(n::ns) -> Lh : <=Lh(n::ns)) from
+; ns ns
+
+; ?_: Lh(Nil nat)<Lh(Nil nat) -> Lh : <=Lh(Nil nat) from
+; ns ns
+> ; ok, we now have the new goal
+; ?_: Lh : <=Lh(Nil nat) from
+; ns ns u:Lh(Nil nat)<Lh(Nil nat)
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; Lh(Nil nat)<Lh(n::ns) -> Lh : <=Lh(n::ns)) from
+; ns ns
+> ; ok, we now have the new goal
+; ?_: Lh : <=Lh(n::ns) from
+; ns ns n ns u:
+; Lh(Nil nat)<Lh(n::ns)
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns)) from
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns) from
+; ns n ns IH:ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, we now have the new goal
+; ?_: ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ can be obtained from
+; ?_: all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; Lh(n::ns)<Lh(n::ns) -> Lh(::ns)<=Lh(n::ns)) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns
+
+; ?_: Lh(n::ns)<Lh(Nil nat) -> Lh(::ns)<=Lh(Nil nat) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns
+> ; ok, we now have the new goal
+; ?_: Lh(::ns)<=Lh(Nil nat) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns u:Lh(n::ns)<Lh(Nil nat)
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; Lh(n::ns)<Lh(n::ns) -> Lh(::ns)<=Lh(n::ns)) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns
+> ; ok, we now have the new goal
+; ?_: Lh(::ns)<=Lh(n::ns) from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns n ns u:Lh(n::ns)<Lh(n::ns)
+> ; ok, ?_ can be obtained from
+; ?_: Lh ns<Lh ns from
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+; ns n ns u:Lh(n::ns)<Lh(n::ns)
+> ; ok, ?_ is proved. Proof finished.
+> [ns]
+ (Rec list nat=>list nat)ns(([ns]ns):)
+ ([n,ns,ns]
+ ([ns,(list nat=>list nat)_](list nat=>list nat)_ ns)ns
+ ([ns]([ns]ns)(::ns)))
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat))
+
+[ns]
+ ([ns]
+ (Rec list nat=>list nat)ns left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))(::ns))@
+ ([ns]
+ ([ns]
+ [if ns
+ (Nil nat)
+ ([n,ns]right(n@ns))])
+ (right(([ns]ns@([ns]ns))(::ns))ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))(::ns))@
+ ([ns]
+ ([ns]
+ [if ns
+ (Nil nat)
+ ([n,ns]right(n@ns))])
+ (right(([ns]ns@([ns]ns))(::ns))ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat))
+
+> ; ?_: all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns)) ->
+; all ns ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, we now have the new goal
+; ?_: all ns ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns)) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns
+
+; ?_: ex ns all ns(Lh(Nil nat)<Lh ns -> Lh ns<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: all ns(Lh(Nil nat)<Lh ns -> Lh : <=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(
+; Lh(Nil nat)<Lh(n::ns) -> Lh : <=Lh(n::ns)) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns ns
+
+; ?_: Lh(Nil nat)<Lh(Nil nat) -> Lh : <=Lh(Nil nat) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns ns
+> ; ok, we now have the new goal
+; ?_: Lh : <=Lh(Nil nat) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns ns u:Lh(Nil nat)<Lh(Nil nat)
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; Lh(Nil nat)<Lh(n::ns) -> Lh : <=Lh(n::ns)) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns ns
+> ; ok, we now have the new goal
+; ?_: Lh : <=Lh(n::ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns ns n ns u:
+; Lh(Nil nat)<Lh(n::ns)
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(
+; ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns)) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns n ns IH:ex ns all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, we now have the new goal
+; ?_: ex ns all ns(Lh(n::ns)<Lh ns -> Lh ns<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ can be obtained from
+; ?_: all ns(Lh(n::ns)<Lh ns -> Lh(n::ns)<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ can be obtained from
+; ?_: all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) from
+; L:all ns,n,ns(
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns) ->
+; all ns(Lh(n::ns)<Lh ns -> Lh(::ns)<=Lh ns))
+; ns n ns ns v:
+; all ns(Lh ns<Lh ns -> Lh ns<=Lh ns)
+> ; ok, ?_ is proved. Proof finished.
+> [ns]
+ (Rec list nat=>list nat)ns(([ns]ns):)
+ ([n,ns,ns]
+ ([ns,(list nat=>list nat)_](list nat=>list nat)_ ns)ns
+ ([ns]([ns]ns)(n::ns)))
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat)n)
+
+([(list nat=>nat=>list nat=>list nat=>list nat)_,ns]
+ ([ns]
+ (Rec list nat=>list nat)ns left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))(n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))(n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))(n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))(n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns)@
+([(list nat=>nat=>list nat=>list nat=>list nat)_,(list nat@@list nat)_]
+ ([ns]
+ (Rec list nat=>list nat=>list nat@@nat@@list nat@@list nat)ns
+ ([ns](Nil nat)@@(Nil nat)@(Nil nat))
+ ([n,ns,(list nat=>list nat@@nat@@list nat@@list nat)_,ns]
+ [let (list nat@@nat@@list nat@@list nat)_
+ (left right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)@
+ left(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)@
+ left(left right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)@
+ right right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns))@
+ right(([ns]ns@([ns]ns))
+ (left(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)::
+ left(left right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)@
+ right right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::
+ ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns))))
+ right(left right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)@
+ right right right(n@
+ ns@
+ ([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]
+ ns@
+ ([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]
+ ns@
+ ([ns]
+ ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns@
+ ns)))
+ [if (([(list nat@@nat@@list nat@@list nat)_]
+ (Lh left(list nat@@nat@@list nat@@list nat)_<
+ Lh((list nat=>nat=>list nat=>list nat=>list nat)_
+ left(list nat@@nat@@list nat@@list nat)_
+ left right(list nat@@nat@@list nat@@list nat)_
+ left right right(list nat@@nat@@list nat@@list nat)_
+ right right right(list nat@@nat@@list nat@@list nat)_)impb
+ Lh left right right(list nat@@nat@@list nat@@list nat)_<=
+ Lh((list nat=>nat=>list nat=>list nat=>list nat)_
+ left(list nat@@nat@@list nat@@list nat)_
+ left right(list nat@@nat@@list nat@@list nat)_
+ left right right(list nat@@nat@@list nat@@list nat)_
+ right right right(list nat@@nat@@list nat@@list nat)_))impb
+ Lh(left right(list nat@@nat@@list nat@@list nat)_::
+ left(list nat@@nat@@list nat@@list nat)_)<
+ Lh right right right(list nat@@nat@@list nat@@list nat)_ impb
+ Lh(::
+ left right right(list nat@@nat@@list nat@@list nat)_)<=
+ Lh right right right(list nat@@nat@@list nat@@list nat)_)
+ (list nat@@nat@@list nat@@list nat)_)
+ ((list nat=>list nat@@nat@@list nat@@list nat)_
+ (right(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))(n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))(n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)
+ (([ns]
+ (Rec list nat=>list nat)ns
+ left(([ns]ns@([ns]ns)):)
+ ([n,ns]
+ left(([n,ns]
+ ([ns]
+ left(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns))@
+ ([ns,ns]
+ right(([ns]
+ left(([ns]ns@([ns]ns))
+ (n::ns))@
+ ([ns]
+ (list nat=>nat=>list nat=>list nat=>list nat)_
+ ns
+ n
+ ns
+ (right(([ns]ns@([ns]ns))
+ (n::ns))
+ ns)))
+ ns)
+ ns))
+ n
+ ns)))
+ ns)
+ ns))
+ (list nat@@nat@@list nat@@list nat)_]]))
+ left(list nat@@list nat)_
+ right(list nat@@list nat)_)
+
+([(list nat=>nat=>list nat=>list nat=>list nat)_,ns]
+ (Rec list nat=>list nat)ns :([n,ns](Cons nat)n))@
+([(list nat=>nat=>list nat=>list nat=>list nat)_,(list nat@@list nat)_]
+ (Rec list nat=>list nat=>list nat@@nat@@list nat@@list nat)
+ left(list nat@@list nat)_
+ ([ns](Nil nat)@@(Nil nat)@(Nil nat))
+ ([n,ns,(list nat=>list nat@@nat@@list nat@@list nat)_,ns]
+ [let (list nat@@nat@@list nat@@list nat)_
+ (ns@n@(Rec list nat=>list nat)ns :([n,ns](Cons nat)n)@ns)
+ [if ((Lh left(list nat@@nat@@list nat@@list nat)_<
+ Lh((list nat=>nat=>list nat=>list nat=>list nat)_
+ left(list nat@@nat@@list nat@@list nat)_
+ left right(list nat@@nat@@list nat@@list nat)_
+ left right right(list nat@@nat@@list nat@@list nat)_
+ right right right(list nat@@nat@@list nat@@list nat)_)impb
+ Lh left right right(list nat@@nat@@list nat@@list nat)_<=
+ Lh((list nat=>nat=>list nat=>list nat=>list nat)_
+ left(list nat@@nat@@list nat@@list nat)_
+ left right(list nat@@nat@@list nat@@list nat)_
+ left right right(list nat@@nat@@list nat@@list nat)_
+ right right right(list nat@@nat@@list nat@@list nat)_))impb
+ Succ Lh left(list nat@@nat@@list nat@@list nat)_<
+ Lh right right right(list nat@@nat@@list nat@@list nat)_ impb
+ Succ Lh left right right(list nat@@nat@@list nat@@list nat)_<=
+ Lh right right right(list nat@@nat@@list nat@@list nat)_)
+ ((list nat=>list nat@@nat@@list nat@@list nat)_
+ ((list nat=>nat=>list nat=>list nat=>list nat)_ ns n
+ ((Rec list nat=>list nat)ns :([n,ns](Cons nat)n))
+ ns))
+ (list nat@@nat@@list nat@@list nat)_]])
+ right(list nat@@list nat)_)
+
+> ; ok, predicate variable R: (arity nat nat) added
+> ; ?_: R -> all n ex n R(Succ n)(Succ n) -> all n ex n R n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R n n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: all n ex n R(Succ n)n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n
+
+; ?_: ex n R n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n ex n R(Succ n)n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n n Step:ex n R(Succ n)(Succ n)
+> ; ok, we now have the new goal
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n n n Step:R(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: R(Succ n)(Succ n) from
+; Base:R
+; Step:all n ex n R(Succ n)(Succ n)
+; n n n Step:R(Succ n)(Succ n)
+> ; ok, ?_ is proved. Proof finished.
+> [alpha_,(nat=>nat@@alpha)_,n]
+ ([n,(nat@@alpha)_,(nat=>nat@@alpha)_]
+ [if n (nat@@alpha)_ (nat=>nat@@alpha)_])
+ n
+ (([n,alpha_]n@alpha_) alpha_)
+ ([n]
+ ([(nat@@alpha)_]
+ ([(nat@@alpha)_,(nat=>alpha=>nat@@alpha)_]
+ (nat=>alpha=>nat@@alpha)_ left(nat@@alpha)_
+ right(nat@@alpha)_)
+ (nat@@alpha)_
+ ([n,alpha_]
+ ([n,alpha_]n@alpha_)(Succ n)alpha_))
+ ((nat=>nat@@alpha)_ n))
+
+[alpha_,(nat=>nat@@alpha)_,n]
+ [if n
+ (@alpha_)
+ ([n]Succ left((nat=>nat@@alpha)_ n)@right((nat=>nat@@alpha)_ n))]
+
+([alpha_]
+ ([(nat=>nat@@alpha)_,n]
+ ([n]
+ [if n
+ (left(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ )
+ alpha_)
+ ([n]
+ left(([(nat@@alpha)_]
+ left(([n]
+ ([alpha_]
+ left(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ (Succ n))
+ alpha_)@
+ ([alpha_,alpha_]
+ right(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ (Succ n))
+ alpha_
+ alpha_))
+ left(nat@@alpha)_)
+ right(nat@@alpha)_)@
+ ([(nat@@alpha)_,alpha_]
+ right(([n]
+ ([alpha_]
+ left(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ (Succ n))
+ alpha_)@
+ ([alpha_,alpha_]
+ right(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]
+ alpha_))
+ (Succ n))
+ alpha_
+ alpha_))
+ left(nat@@alpha)_)
+ right(nat@@alpha)_
+ alpha_))
+ ((nat=>nat@@alpha)_ n))])
+ n)@
+ ([(nat=>nat@@alpha)_,(nat@@alpha)_]
+ ([n]
+ [if n
+ ([alpha_]@(Inhab alpha))
+ ([n,alpha_]
+ left(n@alpha_)@
+ right(([(nat@@alpha)_]
+ left(([n]
+ ([alpha_]
+ left(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ (Succ n))
+ alpha_)@
+ ([alpha_,alpha_]
+ right(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]
+ alpha_))
+ (Succ n))
+ alpha_
+ alpha_))
+ left(nat@@alpha)_)
+ right(nat@@alpha)_)@
+ ([(nat@@alpha)_,alpha_]
+ right(([n]
+ ([alpha_]
+ left(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]
+ alpha_))
+ (Succ n))
+ alpha_)@
+ ([alpha_,alpha_]
+ right(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]
+ alpha_))
+ (Succ n))
+ alpha_
+ alpha_))
+ left(nat@@alpha)_)
+ right(nat@@alpha)_
+ alpha_))
+ ((nat=>nat@@alpha)_ left(n@alpha_))
+ right(n@alpha_))])
+ left(nat@@alpha)_
+ right(nat@@alpha)_))@
+([alpha_,((nat=>nat@@alpha)@@nat@@alpha)_]
+ ([n]
+ [if n
+ ([alpha_]
+ right(([n]
+ ([alpha_]n@alpha_)@
+ ([alpha_,alpha_]alpha_))
+ )
+ alpha_
+ alpha_)
+ ([n,alpha_](Inhab alpha))])
+ left right((nat=>nat@@alpha)@@nat@@alpha)_
+ right right((nat=>nat@@alpha)@@nat@@alpha)_)
+
+([alpha_]
+ ([(nat=>nat@@alpha)_,n]
+ [if n
+ (@alpha_)
+ ([n]
+ Succ left((nat=>nat@@alpha)_ n)@right((nat=>nat@@alpha)_ n))])@
+ ([(nat=>nat@@alpha)_,(nat@@alpha)_]
+ [if (left(nat@@alpha)_)
+ (@(Inhab alpha))
+ ([n]n@right(nat@@alpha)_)]))@
+([alpha_,((nat=>nat@@alpha)@@nat@@alpha)_]
+ [if (left right((nat=>nat@@alpha)@@nat@@alpha)_)
+ (right right((nat=>nat@@alpha)@@nat@@alpha)_)
+ ([n](Inhab alpha))])
+
+> ; ?_: R^ -> all n ex n R^(Succ n)(Succ n) -> all n ex n R^ n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R^ n n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: all n ex n R^(Succ n)n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n
+
+; ?_: ex n R^ n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R^ from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n ex n R^(Succ n)n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R^(Succ n)n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R^(Succ n)n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n n Step:ex n R^(Succ n)(Succ n)
+> ; ok, we now have the new goal
+; ?_: ex n R^(Succ n)n from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n n n Step:R^(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: R^(Succ n)(Succ n) from
+; Base:R^
+; Step:all n ex n R^(Succ n)(Succ n)
+; n n n Step:R^(Succ n)(Succ n)
+> ; ok, ?_ is proved. Proof finished.
+> [(nat=>nat)_,n]
+ ([n,n,(nat=>nat)_][if n n (nat=>nat)_])n
+ (([n]n))
+ ([n]
+ ([n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+ ((nat=>nat)_ n))
+
+[(nat=>nat)_,n][if n ([n]Succ((nat=>nat)_ n))]
+
+(([(nat=>nat)_,n]
+ ([n]
+ [if n
+ (left(([n]n@([alpha_]alpha_))))
+ ([n]
+ left(([n]
+ left(([n]
+ left(([n]n@([alpha_]alpha_))
+ (Succ n))@
+ ([alpha_]
+ right(([n]n@([alpha_]alpha_))
+ (Succ n))
+ alpha_))
+ n))@
+ ([n,alpha_]
+ right(([n]
+ left(([n]n@([alpha_]alpha_))
+ (Succ n))@
+ ([alpha_]
+ right(([n]n@([alpha_]alpha_))
+ (Succ n))
+ alpha_))
+ n)
+ alpha_))
+ ((nat=>nat)_ n))])
+ n)@
+ ([(nat=>nat)_,(nat@@alpha)_]
+ ([n]
+ [if n
+ ([alpha_]@(Inhab alpha))
+ ([n,alpha_]
+ left(n@alpha_)@
+ right(([n]
+ left(([n]
+ left(([n]n@([alpha_]alpha_))
+ (Succ n))@
+ ([alpha_]
+ right(([n]n@([alpha_]alpha_))
+ (Succ n))
+ alpha_))
+ n))@
+ ([n,alpha_]
+ right(([n]
+ left(([n]n@([alpha_]alpha_))
+ (Succ n))@
+ ([alpha_]
+ right(([n]n@([alpha_]alpha_))
+ (Succ n))
+ alpha_))
+ n)
+ alpha_))
+ ((nat=>nat)_ left(n@alpha_))
+ right(n@alpha_))])
+ left(nat@@alpha)_
+ right(nat@@alpha)_))@
+([((nat=>nat)@@nat@@alpha)_]
+ ([n]
+ [if n
+ ([alpha_]
+ right(([n]n@([alpha_]alpha_)))alpha_)
+ ([n,alpha_](Inhab alpha))])
+ left right((nat=>nat)@@nat@@alpha)_
+ right right((nat=>nat)@@nat@@alpha)_)
+
+(([(nat=>nat)_,n][if n ([n]Succ((nat=>nat)_ n))])@
+ ([(nat=>nat)_,(nat@@alpha)_]
+ [if (left(nat@@alpha)_)
+ (@(Inhab alpha))
+ ([n]n@right(nat@@alpha)_)]))@
+([((nat=>nat)@@nat@@alpha)_]
+ [if (left right((nat=>nat)@@nat@@alpha)_)
+ (right right((nat=>nat)@@nat@@alpha)_)
+ ([n](Inhab alpha))])
+
+> ; ?_: R' -> all n ex n R'(Succ n)(Succ n) -> all n ex n R' n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R' n n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: all n ex n R'(Succ n)n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n
+
+; ?_: ex n R' n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R' from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n ex n R'(Succ n)n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R'(Succ n)n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R'(Succ n)n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n n Step:ex n R'(Succ n)(Succ n)
+> ; ok, we now have the new goal
+; ?_: ex n R'(Succ n)n from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n n n Step:R'(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: R'(Succ n)(Succ n) from
+; Base:R'
+; Step:all n ex n R'(Succ n)(Succ n)
+; n n n Step:R'(Succ n)(Succ n)
+> ; ok, ?_ is proved. Proof finished.
+> [alpha_,(nat=>nat@@alpha)_,n]
+ ([n,(nat@@alpha)_,(nat=>nat@@alpha)_]
+ [if n (nat@@alpha)_ (nat=>nat@@alpha)_])
+ n
+ (([n,alpha_]n@alpha_) alpha_)
+ ([n]
+ ([(nat@@alpha)_]
+ ([(nat@@alpha)_,(nat=>alpha=>nat@@alpha)_]
+ (nat=>alpha=>nat@@alpha)_ left(nat@@alpha)_
+ right(nat@@alpha)_)
+ (nat@@alpha)_
+ ([n,alpha_]
+ ([n,alpha_]n@alpha_)(Succ n)alpha_))
+ ((nat=>nat@@alpha)_ n))
+
+[alpha_,(nat=>nat@@alpha)_,n]
+ [if n
+ (@alpha_)
+ ([n]Succ left((nat=>nat@@alpha)_ n)@right((nat=>nat@@alpha)_ n))]
+
+[alpha_]
+ ([(nat=>nat@@alpha)_,n]
+ ([n]
+ [if n
+ (([n,alpha_]n@alpha_) alpha_)
+ ([n]
+ ([(nat@@alpha)_]
+ ([n,alpha_]
+ ([n,alpha_]n@alpha_)(Succ n)alpha_)
+ left(nat@@alpha)_
+ right(nat@@alpha)_)
+ ((nat=>nat@@alpha)_ n))])
+ n)@
+ ([(nat=>nat@@alpha)_,n]([n][if n ([n]n)])n)
+
+[alpha_]
+ ([(nat=>nat@@alpha)_,n]
+ [if n
+ (@alpha_)
+ ([n]
+ Succ left((nat=>nat@@alpha)_ n)@right((nat=>nat@@alpha)_ n))])@
+ ([(nat=>nat@@alpha)_,n][if n ([n]n)])
+
+> ; ?_: R^' -> all n ex n R^'(Succ n)(Succ n) -> all n ex n R^' n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R^' n n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: all n ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n
+
+; ?_: ex n R^' n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R^' from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n n Step:ex n R^'(Succ n)(Succ n)
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n n n Step:R^'(Succ n)(Succ n)
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Succ n)(Succ n) from
+; Base:R^'
+; Step:all n ex n R^'(Succ n)(Succ n)
+; n n n Step:R^'(Succ n)(Succ n)
+> ; ok, ?_ is proved. Proof finished.
+> [(nat=>nat)_,n]
+ ([n,n,(nat=>nat)_][if n n (nat=>nat)_])n
+ (([n]n))
+ ([n]
+ ([n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+ ((nat=>nat)_ n))
+
+[(nat=>nat)_,n][if n ([n]Succ((nat=>nat)_ n))]
+
+([(nat=>nat)_,n]
+ ([n]
+ [if n
+ (([n]n))
+ ([n]
+ ([n]([n]([n]n)(Succ n))n)((nat=>nat)_ n))])
+ n)@
+([(nat=>nat)_,n]([n][if n ([n]n)])n)
+
+([(nat=>nat)_,n][if n ([n]Succ((nat=>nat)_ n))])@
+([(nat=>nat)_,n][if n ([n]n)])
+
+> ; ?_: R -> all n,n(R n n -> R(Succ n)(Succ n)) -> all n ex n R n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R n n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: all n(ex n R n n -> ex n R(Succ n)n) from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n
+
+; ?_: ex n R n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(ex n R n n -> ex n R(Succ n)n) from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n n IH:ex n R n n
+> ; ok, we now have the new goal
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n n n IH:R n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R(Succ n)n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n n n IH:R n n
+; Step:all n(R n n -> R(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R(Succ n)(Succ n) from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n n n IH:R n n
+; Step:all n(R n n -> R(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R n n from
+; Base:R
+; Step:all n,n(R n n -> R(Succ n)(Succ n))
+; n n n IH:R n n
+; Step:all n(R n n -> R(Succ n)(Succ n))
+> ; ok, ?_ is proved. Proof finished.
+> [alpha_,(nat=>nat=>alpha=>alpha)_,n]
+ (Rec nat=>nat@@alpha)n
+ (([n,alpha_]n@alpha_) alpha_)
+ ([n,(nat@@alpha)_]
+ ([(nat@@alpha)_,(nat=>alpha=>nat@@alpha)_]
+ (nat=>alpha=>nat@@alpha)_ left(nat@@alpha)_
+ right(nat@@alpha)_)
+ (nat@@alpha)_
+ ([n,alpha_]
+ ([(nat=>alpha=>alpha)_]
+ ([n,alpha_]n@alpha_)(Succ n)
+ ((nat=>alpha=>alpha)_ n alpha_))
+ ((nat=>nat=>alpha=>alpha)_ n)))
+
+[alpha_,(nat=>nat=>alpha=>alpha)_,n]
+ (Rec nat=>nat@@alpha)n(@alpha_)
+ ([n,(nat@@alpha)_]
+ Succ left(nat@@alpha)_@
+ (nat=>nat=>alpha=>alpha)_ n left(nat@@alpha)_
+ right(nat@@alpha)_)
+
+> ; ?_: R^' ->
+; all n,n(R^' n n -> R^'(Succ n)(Succ n)) ->
+; all n ex n R^' n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R^' n n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: all n(ex n R^' n n -> ex n R^'(Succ n)n) from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+
+; ?_: ex n R^' n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R^' from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(ex n R^' n n -> ex n R^'(Succ n)n) from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n IH:ex n R^' n n
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:all n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Succ n)(Succ n) from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:all n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R^' n n from
+; Base:R^'
+; Step:all n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:all n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ is proved. Proof finished.
+> [n]
+ (Rec nat=>nat)n(([n]n))
+ ([n,n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+> ; ?_: R^' ->
+; allnc n,n(R^' n n -> R^'(Succ n)(Succ n)) ->
+; all n ex n R^' n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R^' n n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: all n(ex n R^' n n -> ex n R^'(Succ n)n) from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+
+; ?_: ex n R^' n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, ?_ can be obtained from
+; ?_: R^' from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n(ex n R^' n n -> ex n R^'(Succ n)n) from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n IH:ex n R^' n n
+> ; ok, we now have the new goal
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+> ; ok, ?_ can be obtained from
+; ?_: ex n R^'(Succ n)n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:allnc n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Succ n)(Succ n) from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:allnc n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ can be obtained from
+; ?_: R^' n n from
+; Base:R^'
+; Step:allnc n,n(R^' n n -> R^'(Succ n)(Succ n))
+; n n n IH:R^' n n
+; Step:allnc n(R^' n n -> R^'(Succ n)(Succ n))
+> ; ok, ?_ is proved. Proof finished.
+> [n]
+ (Rec nat=>nat)n(([n]n))
+ ([n,n]
+ ([n,(nat=>nat)_](nat=>nat)_ n)n([n]([n]n)(Succ n)))
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+[n]
+ ([n]
+ (Rec nat=>nat)n(([n]n))
+ ([n,n]([n]([n]n)(Succ n))n))
+ n
+
+[n](Rec nat=>nat)n ([n]Succ)
+
+> ; ?_: all n(all n(n<n -> ex n R n n) -> ex n R n n) ->
+; all n ex n R n n
+> ; ok, we now have the new goal
+; ?_: all n ex n R n n from
+; L:all n(all n(n<n -> ex n R n n) -> ex n R n n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(
+; all n(([n]n)n<([n]n)n -> ex n R n n) ->
+; ex n R n n) from
+; L:all n(all n(n<n -> ex n R n n) -> ex n R n n)
+; n
+> ; ok, we now have the new goal
+; ?_: ex n R n n from
+; L:all n(all n(n<n -> ex n R n n) -> ex n R n n)
+; n n GIH:all n(([n]n)n<([n]n)n -> ex n R n n)
+> ; ok, ?_ can be obtained from
+; ?_: all n(n<n -> ex n R n n) from
+; L:all n(all n(n<n -> ex n R n n) -> ex n R n n)
+; n n GIH:all n(([n]n)n<([n]n)n -> ex n R n n)
+> ; ok, ?_ is proved. Proof finished.
+> [(nat=>(nat=>nat@@alpha)=>nat@@alpha)_,n]
+ (GRec nat nat@@alpha)([n]n)n
+ ([n,(nat=>nat@@alpha)_]
+ (nat=>(nat=>nat@@alpha)=>nat@@alpha)_ n
+ (nat=>nat@@alpha)_)
+
+[(nat=>(nat=>nat@@alpha)=>nat@@alpha)_,n]
+ (nat=>(nat=>nat@@alpha)=>nat@@alpha)_ n
+ ([n]
+ (GRecGuard nat nat@@alpha)([n]n)n
+ (nat=>(nat=>nat@@alpha)=>nat@@alpha)_
+ (n<n))
+
+> ; ok, predicate variable R is removed
+; warning: R was default pvariable of arity (arity nat nat)
+> ; ok, predicate variable R: (arity list nat list nat) added
+> ; ?_: R(Nil nat)(:) ->
+; all ns,ns,n(R ns ns -> R(n::ns)(n::ns)) ->
+; all ns ex ns R ns ns
+> ; ok, we now have the new goal
+; ?_: all ns ex ns R ns ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(ex ns R ns ns -> ex ns R(n::ns)ns) from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns
+
+; ?_: ex ns R(Nil nat)ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: R(Nil nat)(:) from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(ex ns R ns ns -> ex ns R(n::ns)ns) from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns R(n::ns)ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns n ns IH:ex ns R ns ns
+> ; ok, we now have the new goal
+; ?_: ex ns R(n::ns)ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns n ns ns IH:
+; R ns ns
+> ; ok, ?_ can be obtained from
+; ?_: ex ns R(n::ns)ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns n ns ns IH:
+; R ns ns
+; Step:all ns,n(R ns ns -> R(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R(n::ns)(n::ns) from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns n ns ns IH:
+; R ns ns
+; Step:all ns,n(R ns ns -> R(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R ns ns from
+; Base:R(Nil nat)(:)
+; Step:all ns,ns,n(R ns ns -> R(n::ns)(n::ns))
+; ns n ns ns IH:
+; R ns ns
+; Step:all ns,n(R ns ns -> R(n::ns)(n::ns))
+> ; ok, ?_ is proved. Proof finished.
+> [alpha_,(list nat=>list nat=>nat=>alpha=>alpha)_,ns]
+ (Rec list nat=>list nat@@alpha)ns
+ (([ns,alpha_]ns@alpha_):alpha_)
+ ([n,ns,(list nat@@alpha)_]
+ ([(list nat@@alpha)_,(list nat=>alpha=>list nat@@alpha)_]
+ (list nat=>alpha=>list nat@@alpha)_
+ left(list nat@@alpha)_
+ right(list nat@@alpha)_)
+ (list nat@@alpha)_
+ ([ns,alpha_]
+ ([(list nat=>nat=>alpha=>alpha)_]
+ ([ns,alpha_]ns@alpha_)(n::ns)
+ ((list nat=>nat=>alpha=>alpha)_ ns n alpha_))
+ ((list nat=>list nat=>nat=>alpha=>alpha)_ ns)))
+
+[alpha_,(list nat=>list nat=>nat=>alpha=>alpha)_,ns]
+ (Rec list nat=>list nat@@alpha)ns(: @alpha_)
+ ([n,ns,(list nat@@alpha)_]
+ (n::left(list nat@@alpha)_)@
+ (list nat=>list nat=>nat=>alpha=>alpha)_ ns
+ left(list nat@@alpha)_
+ n
+ right(list nat@@alpha)_)
+
+> ; ?_: R^'(Nil nat)(:) ->
+; all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns)) ->
+; all ns ex ns R^' ns ns
+> ; ok, we now have the new goal
+; ?_: all ns ex ns R^' ns ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(ex ns R^' ns ns -> ex ns R^'(n::ns)ns) from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+
+; ?_: ex ns R^'(Nil nat)ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Nil nat)(:) from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(ex ns R^' ns ns -> ex ns R^'(n::ns)ns) from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns IH:ex ns R^' ns ns
+> ; ok, we now have the new goal
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+> ; ok, ?_ can be obtained from
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:all ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(n::ns)(n::ns) from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:all ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R^' ns ns from
+; Base:R^'(Nil nat)(:)
+; Step:all ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:all ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ is proved. Proof finished.
+> [ns]
+ (Rec list nat=>list nat)ns(([ns]ns):)
+ ([n,ns,ns]
+ ([ns,(list nat=>list nat)_](list nat=>list nat)_ ns)ns
+ ([ns]([ns]ns)(n::ns)))
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat)n)
+
+> ; ?_: R^'(Nil nat)(:) ->
+; allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns)) ->
+; all ns ex ns R^' ns ns
+> ; ok, we now have the new goal
+; ?_: all ns ex ns R^' ns ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: all n,ns(ex ns R^' ns ns -> ex ns R^'(n::ns)ns) from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+
+; ?_: ex ns R^'(Nil nat)ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Nil nat)(:) from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all n,ns(ex ns R^' ns ns -> ex ns R^'(n::ns)ns) from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns
+> ; ok, we now have the new goal
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns IH:ex ns R^' ns ns
+> ; ok, we now have the new goal
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+> ; ok, ?_ can be obtained from
+; ?_: ex ns R^'(n::ns)ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:allnc ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(n::ns)(n::ns) from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:allnc ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ can be obtained from
+; ?_: R^' ns ns from
+; Base:R^'(Nil nat)(:)
+; Step:allnc ns,ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+; ns n ns ns IH:
+; R^' ns ns
+; Step:allnc ns,n(R^' ns ns -> R^'(n::ns)(n::ns))
+> ; ok, ?_ is proved. Proof finished.
+> [ns]
+ (Rec list nat=>list nat)ns(([ns]ns):)
+ ([n,ns,ns]
+ ([ns,(list nat=>list nat)_](list nat=>list nat)_ ns)ns
+ ([ns]([ns]ns)(n::ns)))
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat)n)
+
+[ns]
+ ([ns]
+ (Rec list nat=>list nat)ns(([ns]ns):)
+ ([n,ns,ns]([ns]([ns]ns)(n::ns))ns))
+ ns
+
+[ns](Rec list nat=>list nat)ns :([n,ns](Cons nat)n)
+
+> ; ok, predicate variable R is removed
+; warning: R was default pvariable of arity (arity list nat list nat)
+> ; ok, variable ns is removed
+; warning: ns was default variable of type list nat
+> ; ok, variable x: alpha added
+> ; ok, variable xs: list alpha added
+> ; ok, predicate variable R: (arity list alpha list alpha) added
+> ; ?_: R(Nil alpha)(Nil alpha) ->
+; all xs,xs,x(R xs xs -> R(x::xs)(x::xs)) ->
+; all xs ex xs R xs xs
+> ; ok, we now have the new goal
+; ?_: all xs ex xs R xs xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: all x,xs(ex xs R xs xs -> ex xs R(x::xs)xs) from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs
+
+; ?_: ex xs R(Nil alpha)xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs
+> ; ok, ?_ can be obtained from
+; ?_: R(Nil alpha)(Nil alpha) from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all x,xs(ex xs R xs xs -> ex xs R(x::xs)xs) from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs
+> ; ok, we now have the new goal
+; ?_: ex xs R(x::xs)xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs x xs IH:ex xs R xs xs
+> ; ok, we now have the new goal
+; ?_: ex xs R(x::xs)xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs x xs xs IH:
+; R xs xs
+> ; ok, ?_ can be obtained from
+; ?_: ex xs R(x::xs)xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs x xs xs IH:
+; R xs xs
+; Step:all xs,x(R xs xs -> R(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R(x::xs)(x::xs) from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs x xs xs IH:
+; R xs xs
+; Step:all xs,x(R xs xs -> R(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R xs xs from
+; Base:R(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R xs xs -> R(x::xs)(x::xs))
+; xs x xs xs IH:
+; R xs xs
+; Step:all xs,x(R xs xs -> R(x::xs)(x::xs))
+> ; ok, ?_ is proved. Proof finished.
+> [alpha_,(list alpha=>list alpha=>alpha=>alpha=>alpha)_,xs]
+ (Rec list alpha=>list alpha@@alpha)xs
+ (([xs,alpha_]xs@alpha_)(Nil alpha)alpha_)
+ ([x,xs,(list alpha@@alpha)_]
+ ([(list alpha@@alpha)_,(list alpha=>alpha=>list alpha@@alpha)_]
+ (list alpha=>alpha=>list alpha@@alpha)_
+ left(list alpha@@alpha)_
+ right(list alpha@@alpha)_)
+ (list alpha@@alpha)_
+ ([xs,alpha_]
+ ([(list alpha=>alpha=>alpha=>alpha)_]
+ ([xs,alpha_]xs@alpha_)(x::xs)
+ ((list alpha=>alpha=>alpha=>alpha)_ xs x alpha_))
+ ((list alpha=>list alpha=>alpha=>alpha=>alpha)_ xs)))
+
+[alpha_,(list alpha=>list alpha=>alpha=>alpha=>alpha)_,xs]
+ (Rec list alpha=>list alpha@@alpha)xs((Nil alpha)@alpha_)
+ ([x,xs,(list alpha@@alpha)_]
+ (x::left(list alpha@@alpha)_)@
+ (list alpha=>list alpha=>alpha=>alpha=>alpha)_ xs
+ left(list alpha@@alpha)_
+ x
+ right(list alpha@@alpha)_)
+
+> ; ?_: R^'(Nil alpha)(Nil alpha) ->
+; all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs)) ->
+; all xs ex xs R^' xs xs
+> ; ok, we now have the new goal
+; ?_: all xs ex xs R^' xs xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: all x,xs(ex xs R^' xs xs -> ex xs R^'(x::xs)xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+
+; ?_: ex xs R^'(Nil alpha)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Nil alpha)(Nil alpha) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all x,xs(ex xs R^' xs xs -> ex xs R^'(x::xs)xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, we now have the new goal
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs IH:ex xs R^' xs xs
+> ; ok, we now have the new goal
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+> ; ok, ?_ can be obtained from
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:all xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(x::xs)(x::xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:all xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R^' xs xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:all xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:all xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ is proved. Proof finished.
+> [xs]
+ (Rec list alpha=>list alpha)xs(([xs]xs)(Nil alpha))
+ ([x,xs,xs]
+ ([xs,(list alpha=>list alpha)_](list alpha=>list alpha)_ xs)
+ xs
+ ([xs]([xs]xs)(x::xs)))
+
+[xs](Rec list alpha=>list alpha)xs(Nil alpha)([x,xs](Cons alpha)x)
+
+> ; ?_: R^'(Nil alpha)(Nil alpha) ->
+; allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs)) ->
+; all xs ex xs R^' xs xs
+> ; ok, we now have the new goal
+; ?_: all xs ex xs R^' xs xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: all x,xs(ex xs R^' xs xs -> ex xs R^'(x::xs)xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+
+; ?_: ex xs R^'(Nil alpha)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, ?_ can be obtained from
+; ?_: R^'(Nil alpha)(Nil alpha) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, ?_ is proved. The active goal now is
+; ?_: all x,xs(ex xs R^' xs xs -> ex xs R^'(x::xs)xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs
+> ; ok, we now have the new goal
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs IH:ex xs R^' xs xs
+> ; ok, we now have the new goal
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+> ; ok, ?_ can be obtained from
+; ?_: ex xs R^'(x::xs)xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:allnc xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R^'(x::xs)(x::xs) from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:allnc xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ can be obtained from
+; ?_: R^' xs xs from
+; Base:R^'(Nil alpha)(Nil alpha)
+; Step:allnc xs,xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+; xs x xs xs IH:
+; R^' xs xs
+; Step:allnc xs,x(R^' xs xs -> R^'(x::xs)(x::xs))
+> ; ok, ?_ is proved. Proof finished.
+> [xs]
+ (Rec list alpha=>list alpha)xs(([xs]xs)(Nil alpha))
+ ([x,xs,xs]
+ ([xs,(list alpha=>list alpha)_](list alpha=>list alpha)_ xs)
+ xs
+ ([xs]([xs]xs)(x::xs)))
+
+[xs](Rec list alpha=>list alpha)xs(Nil alpha)([x,xs](Cons alpha)x)
+
+[xs]
+ ([xs]
+ (Rec list alpha=>list alpha)xs(([xs]xs)(Nil alpha))
+ ([x,xs,xs]([xs]([xs]xs)(x::xs))xs))
+ xs
+
+[xs](Rec list alpha=>list alpha)xs(Nil alpha)([x,xs](Cons alpha)x)
+
+> ; ok, predicate variable R is removed
+; warning: R was default pvariable of arity (arity list alpha list alpha)
+> ; ok, variable x is removed
+; warning: x was default variable of type alpha
+; ok, variable xs is removed
+; warning: xs was default variable of type list alpha
+>
make[3]: *** [Makefile.template:21: .test.test-passed] Error 1
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/examples'
make[2]: *** [Makefile:81: examples/.TEST] Error 2
make[2]: Leaving directory '/build/minlog-4.0.99.20100221'
dh_auto_test: error: make -j1 test returned exit code 2
WARNING: Test suite failures
# Delete test suite outputs
find /build/minlog-4.0.99.20100221/examples \
-name '*.diff' \
-delete
find /build/minlog-4.0.99.20100221/examples \
-name '*.out' \
-delete
find /build/minlog-4.0.99.20100221/examples \
-name '*.nodigits' \
-delete
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
create-stamp debian/debhelper-build-stamp
dh_testroot -O--no-parallel
dh_prep -O--no-parallel
debian/rules override_dh_auto_install
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
dh_auto_install -- DESTDIR=/usr PREFIX=/build/minlog-4.0.99.20100221/debian/minlog
make -j1 install DESTDIR=/build/minlog-4.0.99.20100221/debian/minlog AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" DESTDIR=/usr PREFIX=/build/minlog-4.0.99.20100221/debian/minlog
make[2]: Entering directory '/build/minlog-4.0.99.20100221'
(cd src; make .dep.notags)
make[3]: Entering directory '/build/minlog-4.0.99.20100221/src'
make[3]: Nothing to be done for '.dep.notags'.
make[3]: Leaving directory '/build/minlog-4.0.99.20100221/src'
install --strip-program=true -p -d -m 755 /build/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog /build/minlog-4.0.99.20100221/debian/minlog/usr/bin /build/minlog-4.0.99.20100221/debian/minlog/usr/share/emacs/site-lisp/minlog
install: WARNING: ignoring --strip-program option as -s option was not specified
sed "s%---MINLOGPATH---%"/usr/share/minlog"%g; s%---MINLOGELPATH---%"/usr/share/emacs/site-lisp/minlog"%g" < src/minlog.el > /build/minlog-4.0.99.20100221/debian/minlog/usr/share/emacs/site-lisp/minlog/minlog.el
install --strip-program=true -D -p -m 644 minlog-mode.el /build/minlog-4.0.99.20100221/debian/minlog/usr/share/emacs/site-lisp/minlog/minlog-mode.el
install: WARNING: ignoring --strip-program option as -s option was not specified
sed "s%---MINLOGPATH---%"/usr/share/emacs/site-lisp/minlog"%g" < src/minlog > /build/minlog-4.0.99.20100221/debian/minlog/usr/bin/minlog
chmod a+x /build/minlog-4.0.99.20100221/debian/minlog/usr/bin/minlog
sed "s%---MINLOGPATH---%"/usr/share/minlog"%g; s%(minlog-load \"examples/\" path))%(load (string-append \""/usr/share/doc/minlog"/examples/\" path)))%g" < src/init.scm > /build/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog/init.scm
(cd src; find . -name '*.scm' -type f -exec install --strip-program=true -D -p -m 644 {} /build/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog/src/{} \;)
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
(cd lib; find . -name '*.scm' -type f -exec install --strip-program=true -D -p -m 644 {} /build/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog/lib/{} \;)
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
(cd modules; find . -name '*.scm' -type f -exec install --strip-program=true -D -p -m 644 {} /build/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog/modules/{} \;)
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
(cd examples; find . -type f -a ! -path "*/CVS/*" -a ! -name ".cvsignore" -exec install --strip-program=true -D -p -m 644 {} /build/minlog-4.0.99.20100221/debian/minlog/usr/share/doc/minlog/examples/{} \;)
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
(cd doc; find . -name '*.pdf' -type f -exec install --strip-program=true -D -p -m 644 {} /build/minlog-4.0.99.20100221/debian/minlog/usr/share/doc/minlog/{} \;)
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
install: WARNING: ignoring --strip-program option as -s option was not specified
make[2]: Leaving directory '/build/minlog-4.0.99.20100221'
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
dh_installdocs -O--no-parallel
dh_installchangelogs -O--no-parallel
debian/rules override_dh_installman
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
dh_installman debian/minlog.1
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
dh_installsystemduser -O--no-parallel
dh_perl -O--no-parallel
dh_link -O--no-parallel
dh_strip_nondeterminism -O--no-parallel
debian/rules override_dh_compress
make[1]: Entering directory '/build/minlog-4.0.99.20100221'
dh_compress --exclude=minlog/examples --exclude=.pdf
make[1]: Leaving directory '/build/minlog-4.0.99.20100221'
dh_fixperms -O--no-parallel
dh_missing -O--no-parallel
dh_installdeb -O--no-parallel
dh_gencontrol -O--no-parallel
dh_md5sums -O--no-parallel
dh_builddeb -O--no-parallel
dpkg-deb: building package 'minlog' in '../minlog_4.0.99.20100221-7_all.deb'.
dpkg-genbuildinfo --build=binary -O../minlog_4.0.99.20100221-7_i386.buildinfo
dpkg-genchanges --build=binary -O../minlog_4.0.99.20100221-7_i386.changes
dpkg-genchanges: info: binary-only upload (no source code included)
dpkg-source --after-build .
dpkg-buildpackage: info: binary-only upload (no source included)
dpkg-genchanges: info: not including original source code in upload
I: copying local configuration
I: unmounting dev/ptmx filesystem
I: unmounting dev/pts filesystem
I: unmounting dev/shm filesystem
I: unmounting proc filesystem
I: unmounting sys filesystem
I: cleaning the build env
I: removing directory /srv/workspace/pbuilder/7405 and its subdirectories
I: Current time: Sun Apr 16 11:21:06 -12 2023
I: pbuilder-time-stamp: 1681687266