I: pbuilder: network access will be disabled during build I: Current time: Mon Jun 3 01:47:26 -12 2024 I: pbuilder-time-stamp: 1717422446 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: 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/3314934/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='amd64' DEBIAN_FRONTEND='noninteractive' DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=16' DISTRIBUTION='bookworm' HOME='/root' HOST_ARCH='amd64' IFS=' ' INVOCATION_ID='a5ad353e1534421080f2c4002a771a3f' LANG='C' LANGUAGE='en_US:en' LC_ALL='C' 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='3314934' 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.vaTqmwIr/pbuilderrc_mThs --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.vaTqmwIr/b1 --logfile b1/build.log minlog_4.0.99.20100221-7.dsc' SUDO_GID='111' SUDO_UID='106' SUDO_USER='jenkins' TERM='unknown' TZ='/usr/share/zoneinfo/Etc/GMT+12' USER='root' _='/usr/bin/systemd-run' http_proxy='http://85.184.249.68:3128' I: uname -a Linux ionos15-amd64 6.1.0-0.deb11.6-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.15-1~bpo11+1 (2023-03-16) x86_64 GNU/Linux I: ls -l /bin total 5632 -rwxr-xr-x 1 root root 1265648 Apr 23 2023 bash -rwxr-xr-x 3 root root 39224 Sep 18 2022 bunzip2 -rwxr-xr-x 3 root root 39224 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 39224 Sep 18 2022 bzip2 -rwxr-xr-x 1 root root 14568 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 44016 Sep 20 2022 cat -rwxr-xr-x 1 root root 68656 Sep 20 2022 chgrp -rwxr-xr-x 1 root root 64496 Sep 20 2022 chmod -rwxr-xr-x 1 root root 72752 Sep 20 2022 chown -rwxr-xr-x 1 root root 151152 Sep 20 2022 cp -rwxr-xr-x 1 root root 125640 Jan 5 2023 dash -rwxr-xr-x 1 root root 121904 Sep 20 2022 date -rwxr-xr-x 1 root root 89240 Sep 20 2022 dd -rwxr-xr-x 1 root root 102200 Sep 20 2022 df -rwxr-xr-x 1 root root 151344 Sep 20 2022 dir -rwxr-xr-x 1 root root 88656 Mar 22 2023 dmesg lrwxrwxrwx 1 root root 8 Dec 19 2022 dnsdomainname -> hostname lrwxrwxrwx 1 root root 8 Dec 19 2022 domainname -> hostname -rwxr-xr-x 1 root root 43856 Sep 20 2022 echo -rwxr-xr-x 1 root root 41 Jan 24 2023 egrep -rwxr-xr-x 1 root root 35664 Sep 20 2022 false -rwxr-xr-x 1 root root 41 Jan 24 2023 fgrep -rwxr-xr-x 1 root root 85600 Mar 22 2023 findmnt -rwsr-xr-x 1 root root 35128 Mar 22 2023 fusermount -rwxr-xr-x 1 root root 203152 Jan 24 2023 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 98136 Apr 9 2022 gzip -rwxr-xr-x 1 root root 22680 Dec 19 2022 hostname -rwxr-xr-x 1 root root 72824 Sep 20 2022 ln -rwxr-xr-x 1 root root 53024 Mar 23 2023 login -rwxr-xr-x 1 root root 151344 Sep 20 2022 ls -rwxr-xr-x 1 root root 207168 Mar 22 2023 lsblk -rwxr-xr-x 1 root root 97552 Sep 20 2022 mkdir -rwxr-xr-x 1 root root 72912 Sep 20 2022 mknod -rwxr-xr-x 1 root root 43952 Sep 20 2022 mktemp -rwxr-xr-x 1 root root 59712 Mar 22 2023 more -rwsr-xr-x 1 root root 59704 Mar 22 2023 mount -rwxr-xr-x 1 root root 18744 Mar 22 2023 mountpoint -rwxr-xr-x 1 root root 142968 Sep 20 2022 mv lrwxrwxrwx 1 root root 8 Dec 19 2022 nisdomainname -> hostname lrwxrwxrwx 1 root root 14 Apr 2 2023 pidof -> /sbin/killall5 -rwxr-xr-x 1 root root 43952 Sep 20 2022 pwd lrwxrwxrwx 1 root root 4 Apr 23 2023 rbash -> bash -rwxr-xr-x 1 root root 52112 Sep 20 2022 readlink -rwxr-xr-x 1 root root 72752 Sep 20 2022 rm -rwxr-xr-x 1 root root 56240 Sep 20 2022 rmdir -rwxr-xr-x 1 root root 27560 Nov 2 2022 run-parts -rwxr-xr-x 1 root root 126424 Jan 5 2023 sed lrwxrwxrwx 1 root root 4 Jan 5 2023 sh -> dash -rwxr-xr-x 1 root root 43888 Sep 20 2022 sleep -rwxr-xr-x 1 root root 85008 Sep 20 2022 stty -rwsr-xr-x 1 root root 72000 Mar 22 2023 su -rwxr-xr-x 1 root root 39824 Sep 20 2022 sync -rwxr-xr-x 1 root root 531984 Apr 6 2023 tar -rwxr-xr-x 1 root root 14520 Nov 2 2022 tempfile -rwxr-xr-x 1 root root 109616 Sep 20 2022 touch -rwxr-xr-x 1 root root 35664 Sep 20 2022 true -rwxr-xr-x 1 root root 14568 Mar 22 2023 ulockmgr_server -rwsr-xr-x 1 root root 35128 Mar 22 2023 umount -rwxr-xr-x 1 root root 43888 Sep 20 2022 uname -rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress -rwxr-xr-x 1 root root 151344 Sep 20 2022 vdir -rwxr-xr-x 1 root root 72024 Mar 22 2023 wdctl lrwxrwxrwx 1 root root 8 Dec 19 2022 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/3314934/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: amd64 Maintainer: Debian Pbuilder Team 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 ... 19596 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} 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} 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, 82 newly installed, 0 to remove and 0 not upgraded. Need to get 189 MB of archives. After unpacking 673 MB will be used. Writing extended state information... Get: 1 http://deb.debian.org/debian bookworm/main amd64 sensible-utils all 0.0.17+nmu1 [19.0 kB] Get: 2 http://deb.debian.org/debian bookworm/main amd64 libmagic-mgc amd64 1:5.44-3 [305 kB] Get: 3 http://deb.debian.org/debian bookworm/main amd64 libmagic1 amd64 1:5.44-3 [104 kB] Get: 4 http://deb.debian.org/debian bookworm/main amd64 file amd64 1:5.44-3 [42.5 kB] Get: 5 http://deb.debian.org/debian bookworm/main amd64 gettext-base amd64 0.21-12 [160 kB] Get: 6 http://deb.debian.org/debian bookworm/main amd64 libuchardet0 amd64 0.0.7-1 [67.8 kB] Get: 7 http://deb.debian.org/debian bookworm/main amd64 groff-base amd64 1.22.4-10 [916 kB] Get: 8 http://deb.debian.org/debian bookworm/main amd64 bsdextrautils amd64 2.38.1-5+b1 [86.6 kB] Get: 9 http://deb.debian.org/debian bookworm/main amd64 libpipeline1 amd64 1.5.7-1 [38.5 kB] Get: 10 http://deb.debian.org/debian bookworm/main amd64 man-db amd64 2.11.2-2 [1386 kB] Get: 11 http://deb.debian.org/debian bookworm/main amd64 ucf all 3.0043+nmu1 [55.2 kB] Get: 12 http://deb.debian.org/debian bookworm/main amd64 m4 amd64 1.4.19-3 [287 kB] Get: 13 http://deb.debian.org/debian bookworm/main amd64 autoconf all 2.71-3 [332 kB] Get: 14 http://deb.debian.org/debian bookworm/main amd64 autotools-dev all 20220109.1 [51.6 kB] Get: 15 http://deb.debian.org/debian bookworm/main amd64 automake all 1:1.16.5-1.3 [823 kB] Get: 16 http://deb.debian.org/debian bookworm/main amd64 autopoint all 0.21-12 [495 kB] Get: 17 http://deb.debian.org/debian bookworm/main amd64 libdebhelper-perl all 13.11.4 [81.2 kB] Get: 18 http://deb.debian.org/debian bookworm/main amd64 libtool all 2.4.7-5 [517 kB] Get: 19 http://deb.debian.org/debian bookworm/main amd64 dh-autoreconf all 20 [17.1 kB] Get: 20 http://deb.debian.org/debian bookworm/main amd64 libarchive-zip-perl all 1.68-1 [104 kB] Get: 21 http://deb.debian.org/debian bookworm/main amd64 libsub-override-perl all 0.09-4 [9304 B] Get: 22 http://deb.debian.org/debian bookworm/main amd64 libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB] Get: 23 http://deb.debian.org/debian bookworm/main amd64 dh-strip-nondeterminism all 1.13.1-1 [8620 B] Get: 24 http://deb.debian.org/debian bookworm/main amd64 libelf1 amd64 0.188-2.1 [174 kB] Get: 25 http://deb.debian.org/debian bookworm/main amd64 dwz amd64 0.15-1 [109 kB] Get: 26 http://deb.debian.org/debian bookworm/main amd64 libicu72 amd64 72.1-3 [9376 kB] Get: 27 http://deb.debian.org/debian bookworm/main amd64 libxml2 amd64 2.9.14+dfsg-1.2 [687 kB] Get: 28 http://deb.debian.org/debian bookworm/main amd64 gettext amd64 0.21-12 [1300 kB] Get: 29 http://deb.debian.org/debian bookworm/main amd64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get: 30 http://deb.debian.org/debian bookworm/main amd64 po-debconf all 1.0.21+nmu1 [248 kB] Get: 31 http://deb.debian.org/debian bookworm/main amd64 debhelper all 13.11.4 [942 kB] Get: 32 http://deb.debian.org/debian bookworm/main amd64 fonts-dejavu-core all 2.37-6 [1068 kB] Get: 33 http://deb.debian.org/debian bookworm/main amd64 fontconfig-config amd64 2.14.1-4 [315 kB] Get: 34 http://deb.debian.org/debian bookworm/main amd64 fonts-lmodern all 2.005-1 [4540 kB] Get: 35 http://deb.debian.org/debian bookworm/main amd64 libbrotli1 amd64 1.0.9-2+b6 [275 kB] Get: 36 http://deb.debian.org/debian bookworm/main amd64 libbsd0 amd64 0.11.7-2 [117 kB] Get: 37 http://deb.debian.org/debian bookworm/main amd64 libexpat1 amd64 2.5.0-1 [99.3 kB] Get: 38 http://deb.debian.org/debian bookworm/main amd64 libpng16-16 amd64 1.6.39-2 [276 kB] Get: 39 http://deb.debian.org/debian bookworm/main amd64 libfreetype6 amd64 2.12.1+dfsg-5 [399 kB] Get: 40 http://deb.debian.org/debian bookworm/main amd64 libfontconfig1 amd64 2.14.1-4 [386 kB] Get: 41 http://deb.debian.org/debian bookworm/main amd64 libpixman-1-0 amd64 0.42.2-1 [546 kB] Get: 42 http://deb.debian.org/debian bookworm/main amd64 libxau6 amd64 1:1.0.9-1 [19.7 kB] Get: 43 http://deb.debian.org/debian bookworm/main amd64 libxdmcp6 amd64 1:1.1.2-3 [26.3 kB] Get: 44 http://deb.debian.org/debian bookworm/main amd64 libxcb1 amd64 1.15-1 [144 kB] Get: 45 http://deb.debian.org/debian bookworm/main amd64 libx11-data all 2:1.8.4-2 [292 kB] Get: 46 http://deb.debian.org/debian bookworm/main amd64 libx11-6 amd64 2:1.8.4-2 [759 kB] Get: 47 http://deb.debian.org/debian bookworm/main amd64 libxcb-render0 amd64 1.15-1 [115 kB] Get: 48 http://deb.debian.org/debian bookworm/main amd64 libxcb-shm0 amd64 1.15-1 [105 kB] Get: 49 http://deb.debian.org/debian bookworm/main amd64 libxext6 amd64 2:1.3.4-1+b1 [52.9 kB] Get: 50 http://deb.debian.org/debian bookworm/main amd64 libxrender1 amd64 1:0.9.10-1.1 [33.2 kB] Get: 51 http://deb.debian.org/debian bookworm/main amd64 libcairo2 amd64 1.16.0-7 [575 kB] Get: 52 http://deb.debian.org/debian bookworm/main amd64 libglib2.0-0 amd64 2.74.6-2 [1398 kB] Get: 53 http://deb.debian.org/debian bookworm/main amd64 libgraphite2-3 amd64 1.3.14-1 [81.2 kB] Get: 54 http://deb.debian.org/debian bookworm/main amd64 libharfbuzz0b amd64 6.0.0+dfsg-3 [1945 kB] Get: 55 http://deb.debian.org/debian bookworm/main amd64 x11-common all 1:7.7+23 [252 kB] Get: 56 http://deb.debian.org/debian bookworm/main amd64 libice6 amd64 2:1.0.10-1 [58.5 kB] Get: 57 http://deb.debian.org/debian bookworm/main amd64 libkpathsea6 amd64 2022.20220321.62855-5 [152 kB] Get: 58 http://deb.debian.org/debian bookworm/main amd64 libpaper1 amd64 1.1.29 [12.5 kB] Get: 59 http://deb.debian.org/debian bookworm/main amd64 libpaper-utils amd64 1.1.29 [8868 B] Get: 60 http://deb.debian.org/debian bookworm/main amd64 libptexenc1 amd64 2022.20220321.62855-5 [43.5 kB] Get: 61 http://deb.debian.org/debian bookworm/main amd64 libsm6 amd64 2:1.2.3-1 [35.1 kB] Get: 62 http://deb.debian.org/debian bookworm/main amd64 libsynctex2 amd64 2022.20220321.62855-5 [59.6 kB] Get: 63 http://deb.debian.org/debian bookworm/main amd64 libteckit0 amd64 2.5.11+ds1-1+b1 [335 kB] Get: 64 http://deb.debian.org/debian bookworm/main amd64 libtexlua53-5 amd64 2022.20220321.62855-5 [111 kB] Get: 65 http://deb.debian.org/debian bookworm/main amd64 libtexluajit2 amd64 2022.20220321.62855-5 [246 kB] Get: 66 http://deb.debian.org/debian bookworm/main amd64 libxt6 amd64 1:1.2.1-1.1 [186 kB] Get: 67 http://deb.debian.org/debian bookworm/main amd64 libxmu6 amd64 2:1.1.3-3 [60.1 kB] Get: 68 http://deb.debian.org/debian bookworm/main amd64 libxpm4 amd64 1:3.5.12-1.1 [48.4 kB] Get: 69 http://deb.debian.org/debian bookworm/main amd64 libxaw7 amd64 2:1.0.14-1 [201 kB] Get: 70 http://deb.debian.org/debian bookworm/main amd64 libxi6 amd64 2:1.8-1+b1 [84.2 kB] Get: 71 http://deb.debian.org/debian bookworm/main amd64 libzzip-0-13 amd64 0.13.72+dfsg.1-1.1 [58.3 kB] Get: 72 http://deb.debian.org/debian bookworm/main amd64 racket-common all 8.7+dfsg1-1 [14.9 MB] Get: 73 http://deb.debian.org/debian bookworm/main amd64 racket amd64 8.7+dfsg1-1 [92.5 MB] Get: 74 http://deb.debian.org/debian bookworm/main amd64 t1utils amd64 1.41-4 [62.1 kB] Get: 75 http://deb.debian.org/debian bookworm/main amd64 tex-common all 6.18 [32.5 kB] Get: 76 http://deb.debian.org/debian bookworm/main amd64 texlive-binaries amd64 2022.20220321.62855-5 [10.5 MB] Get: 77 http://deb.debian.org/debian bookworm/main amd64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 78 http://deb.debian.org/debian bookworm/main amd64 texlive-base all 2022.20230122-3 [21.9 MB] Get: 79 http://deb.debian.org/debian bookworm/main amd64 texlive-fonts-recommended all 2022.20230122-3 [4988 kB] Get: 80 http://deb.debian.org/debian bookworm/main amd64 texlive-latex-base all 2022.20230122-3 [1182 kB] Get: 81 http://deb.debian.org/debian bookworm/main amd64 texlive-latex-recommended all 2022.20230122-3 [8880 kB] Get: 82 http://deb.debian.org/debian bookworm/main amd64 texlive all 2022.20230122-3 [18.2 kB] Fetched 189 MB in 2s (83.6 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package sensible-utils. (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 ... 19596 files and directories currently installed.) Preparing to unpack .../00-sensible-utils_0.0.17+nmu1_all.deb ... Unpacking sensible-utils (0.0.17+nmu1) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../01-libmagic-mgc_1%3a5.44-3_amd64.deb ... Unpacking libmagic-mgc (1:5.44-3) ... Selecting previously unselected package libmagic1:amd64. Preparing to unpack .../02-libmagic1_1%3a5.44-3_amd64.deb ... Unpacking libmagic1:amd64 (1:5.44-3) ... Selecting previously unselected package file. Preparing to unpack .../03-file_1%3a5.44-3_amd64.deb ... Unpacking file (1:5.44-3) ... Selecting previously unselected package gettext-base. Preparing to unpack .../04-gettext-base_0.21-12_amd64.deb ... Unpacking gettext-base (0.21-12) ... Selecting previously unselected package libuchardet0:amd64. Preparing to unpack .../05-libuchardet0_0.0.7-1_amd64.deb ... Unpacking libuchardet0:amd64 (0.0.7-1) ... Selecting previously unselected package groff-base. Preparing to unpack .../06-groff-base_1.22.4-10_amd64.deb ... Unpacking groff-base (1.22.4-10) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../07-bsdextrautils_2.38.1-5+b1_amd64.deb ... Unpacking bsdextrautils (2.38.1-5+b1) ... Selecting previously unselected package libpipeline1:amd64. Preparing to unpack .../08-libpipeline1_1.5.7-1_amd64.deb ... Unpacking libpipeline1:amd64 (1.5.7-1) ... Selecting previously unselected package man-db. Preparing to unpack .../09-man-db_2.11.2-2_amd64.deb ... Unpacking man-db (2.11.2-2) ... Selecting previously unselected package ucf. Preparing to unpack .../10-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 .../11-m4_1.4.19-3_amd64.deb ... Unpacking m4 (1.4.19-3) ... Selecting previously unselected package autoconf. Preparing to unpack .../12-autoconf_2.71-3_all.deb ... Unpacking autoconf (2.71-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../13-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../14-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 .../15-autopoint_0.21-12_all.deb ... Unpacking autopoint (0.21-12) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../16-libdebhelper-perl_13.11.4_all.deb ... Unpacking libdebhelper-perl (13.11.4) ... Selecting previously unselected package libtool. Preparing to unpack .../17-libtool_2.4.7-5_all.deb ... Unpacking libtool (2.4.7-5) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../18-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../19-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 .../20-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 .../21-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 .../22-dh-strip-nondeterminism_1.13.1-1_all.deb ... Unpacking dh-strip-nondeterminism (1.13.1-1) ... Selecting previously unselected package libelf1:amd64. Preparing to unpack .../23-libelf1_0.188-2.1_amd64.deb ... Unpacking libelf1:amd64 (0.188-2.1) ... Selecting previously unselected package dwz. Preparing to unpack .../24-dwz_0.15-1_amd64.deb ... Unpacking dwz (0.15-1) ... Selecting previously unselected package libicu72:amd64. Preparing to unpack .../25-libicu72_72.1-3_amd64.deb ... Unpacking libicu72:amd64 (72.1-3) ... Selecting previously unselected package libxml2:amd64. Preparing to unpack .../26-libxml2_2.9.14+dfsg-1.2_amd64.deb ... Unpacking libxml2:amd64 (2.9.14+dfsg-1.2) ... Selecting previously unselected package gettext. Preparing to unpack .../27-gettext_0.21-12_amd64.deb ... Unpacking gettext (0.21-12) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../28-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 .../29-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../30-debhelper_13.11.4_all.deb ... Unpacking debhelper (13.11.4) ... Selecting previously unselected package fonts-dejavu-core. Preparing to unpack .../31-fonts-dejavu-core_2.37-6_all.deb ... Unpacking fonts-dejavu-core (2.37-6) ... Selecting previously unselected package fontconfig-config. Preparing to unpack .../32-fontconfig-config_2.14.1-4_amd64.deb ... Unpacking fontconfig-config (2.14.1-4) ... Selecting previously unselected package fonts-lmodern. Preparing to unpack .../33-fonts-lmodern_2.005-1_all.deb ... Unpacking fonts-lmodern (2.005-1) ... Selecting previously unselected package libbrotli1:amd64. Preparing to unpack .../34-libbrotli1_1.0.9-2+b6_amd64.deb ... Unpacking libbrotli1:amd64 (1.0.9-2+b6) ... Selecting previously unselected package libbsd0:amd64. Preparing to unpack .../35-libbsd0_0.11.7-2_amd64.deb ... Unpacking libbsd0:amd64 (0.11.7-2) ... Selecting previously unselected package libexpat1:amd64. Preparing to unpack .../36-libexpat1_2.5.0-1_amd64.deb ... Unpacking libexpat1:amd64 (2.5.0-1) ... Selecting previously unselected package libpng16-16:amd64. Preparing to unpack .../37-libpng16-16_1.6.39-2_amd64.deb ... Unpacking libpng16-16:amd64 (1.6.39-2) ... Selecting previously unselected package libfreetype6:amd64. Preparing to unpack .../38-libfreetype6_2.12.1+dfsg-5_amd64.deb ... Unpacking libfreetype6:amd64 (2.12.1+dfsg-5) ... Selecting previously unselected package libfontconfig1:amd64. Preparing to unpack .../39-libfontconfig1_2.14.1-4_amd64.deb ... Unpacking libfontconfig1:amd64 (2.14.1-4) ... Selecting previously unselected package libpixman-1-0:amd64. Preparing to unpack .../40-libpixman-1-0_0.42.2-1_amd64.deb ... Unpacking libpixman-1-0:amd64 (0.42.2-1) ... Selecting previously unselected package libxau6:amd64. Preparing to unpack .../41-libxau6_1%3a1.0.9-1_amd64.deb ... Unpacking libxau6:amd64 (1:1.0.9-1) ... Selecting previously unselected package libxdmcp6:amd64. Preparing to unpack .../42-libxdmcp6_1%3a1.1.2-3_amd64.deb ... Unpacking libxdmcp6:amd64 (1:1.1.2-3) ... Selecting previously unselected package libxcb1:amd64. Preparing to unpack .../43-libxcb1_1.15-1_amd64.deb ... Unpacking libxcb1:amd64 (1.15-1) ... Selecting previously unselected package libx11-data. Preparing to unpack .../44-libx11-data_2%3a1.8.4-2_all.deb ... Unpacking libx11-data (2:1.8.4-2) ... Selecting previously unselected package libx11-6:amd64. Preparing to unpack .../45-libx11-6_2%3a1.8.4-2_amd64.deb ... Unpacking libx11-6:amd64 (2:1.8.4-2) ... Selecting previously unselected package libxcb-render0:amd64. Preparing to unpack .../46-libxcb-render0_1.15-1_amd64.deb ... Unpacking libxcb-render0:amd64 (1.15-1) ... Selecting previously unselected package libxcb-shm0:amd64. Preparing to unpack .../47-libxcb-shm0_1.15-1_amd64.deb ... Unpacking libxcb-shm0:amd64 (1.15-1) ... Selecting previously unselected package libxext6:amd64. Preparing to unpack .../48-libxext6_2%3a1.3.4-1+b1_amd64.deb ... Unpacking libxext6:amd64 (2:1.3.4-1+b1) ... Selecting previously unselected package libxrender1:amd64. Preparing to unpack .../49-libxrender1_1%3a0.9.10-1.1_amd64.deb ... Unpacking libxrender1:amd64 (1:0.9.10-1.1) ... Selecting previously unselected package libcairo2:amd64. Preparing to unpack .../50-libcairo2_1.16.0-7_amd64.deb ... Unpacking libcairo2:amd64 (1.16.0-7) ... Selecting previously unselected package libglib2.0-0:amd64. Preparing to unpack .../51-libglib2.0-0_2.74.6-2_amd64.deb ... Unpacking libglib2.0-0:amd64 (2.74.6-2) ... Selecting previously unselected package libgraphite2-3:amd64. Preparing to unpack .../52-libgraphite2-3_1.3.14-1_amd64.deb ... Unpacking libgraphite2-3:amd64 (1.3.14-1) ... Selecting previously unselected package libharfbuzz0b:amd64. Preparing to unpack .../53-libharfbuzz0b_6.0.0+dfsg-3_amd64.deb ... Unpacking libharfbuzz0b:amd64 (6.0.0+dfsg-3) ... Selecting previously unselected package x11-common. Preparing to unpack .../54-x11-common_1%3a7.7+23_all.deb ... Unpacking x11-common (1:7.7+23) ... Selecting previously unselected package libice6:amd64. Preparing to unpack .../55-libice6_2%3a1.0.10-1_amd64.deb ... Unpacking libice6:amd64 (2:1.0.10-1) ... Selecting previously unselected package libkpathsea6:amd64. Preparing to unpack .../56-libkpathsea6_2022.20220321.62855-5_amd64.deb ... Unpacking libkpathsea6:amd64 (2022.20220321.62855-5) ... Selecting previously unselected package libpaper1:amd64. Preparing to unpack .../57-libpaper1_1.1.29_amd64.deb ... Unpacking libpaper1:amd64 (1.1.29) ... Selecting previously unselected package libpaper-utils. Preparing to unpack .../58-libpaper-utils_1.1.29_amd64.deb ... Unpacking libpaper-utils (1.1.29) ... Selecting previously unselected package libptexenc1:amd64. Preparing to unpack .../59-libptexenc1_2022.20220321.62855-5_amd64.deb ... Unpacking libptexenc1:amd64 (2022.20220321.62855-5) ... Selecting previously unselected package libsm6:amd64. Preparing to unpack .../60-libsm6_2%3a1.2.3-1_amd64.deb ... Unpacking libsm6:amd64 (2:1.2.3-1) ... Selecting previously unselected package libsynctex2:amd64. Preparing to unpack .../61-libsynctex2_2022.20220321.62855-5_amd64.deb ... Unpacking libsynctex2:amd64 (2022.20220321.62855-5) ... Selecting previously unselected package libteckit0:amd64. Preparing to unpack .../62-libteckit0_2.5.11+ds1-1+b1_amd64.deb ... Unpacking libteckit0:amd64 (2.5.11+ds1-1+b1) ... Selecting previously unselected package libtexlua53-5:amd64. Preparing to unpack .../63-libtexlua53-5_2022.20220321.62855-5_amd64.deb ... Unpacking libtexlua53-5:amd64 (2022.20220321.62855-5) ... Selecting previously unselected package libtexluajit2:amd64. Preparing to unpack .../64-libtexluajit2_2022.20220321.62855-5_amd64.deb ... Unpacking libtexluajit2:amd64 (2022.20220321.62855-5) ... Selecting previously unselected package libxt6:amd64. Preparing to unpack .../65-libxt6_1%3a1.2.1-1.1_amd64.deb ... Unpacking libxt6:amd64 (1:1.2.1-1.1) ... Selecting previously unselected package libxmu6:amd64. Preparing to unpack .../66-libxmu6_2%3a1.1.3-3_amd64.deb ... Unpacking libxmu6:amd64 (2:1.1.3-3) ... Selecting previously unselected package libxpm4:amd64. Preparing to unpack .../67-libxpm4_1%3a3.5.12-1.1_amd64.deb ... Unpacking libxpm4:amd64 (1:3.5.12-1.1) ... Selecting previously unselected package libxaw7:amd64. Preparing to unpack .../68-libxaw7_2%3a1.0.14-1_amd64.deb ... Unpacking libxaw7:amd64 (2:1.0.14-1) ... Selecting previously unselected package libxi6:amd64. Preparing to unpack .../69-libxi6_2%3a1.8-1+b1_amd64.deb ... Unpacking libxi6:amd64 (2:1.8-1+b1) ... Selecting previously unselected package libzzip-0-13:amd64. Preparing to unpack .../70-libzzip-0-13_0.13.72+dfsg.1-1.1_amd64.deb ... Unpacking libzzip-0-13:amd64 (0.13.72+dfsg.1-1.1) ... Selecting previously unselected package racket-common. Preparing to unpack .../71-racket-common_8.7+dfsg1-1_all.deb ... Unpacking racket-common (8.7+dfsg1-1) ... Selecting previously unselected package racket. Preparing to unpack .../72-racket_8.7+dfsg1-1_amd64.deb ... Unpacking racket (8.7+dfsg1-1) ... Selecting previously unselected package t1utils. Preparing to unpack .../73-t1utils_1.41-4_amd64.deb ... Unpacking t1utils (1.41-4) ... Selecting previously unselected package tex-common. Preparing to unpack .../74-tex-common_6.18_all.deb ... Unpacking tex-common (6.18) ... Selecting previously unselected package texlive-binaries. Preparing to unpack .../75-texlive-binaries_2022.20220321.62855-5_amd64.deb ... Unpacking texlive-binaries (2022.20220321.62855-5) ... Selecting previously unselected package xdg-utils. Preparing to unpack .../76-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 .../77-texlive-base_2022.20230122-3_all.deb ... Unpacking texlive-base (2022.20230122-3) ... Selecting previously unselected package texlive-fonts-recommended. Preparing to unpack .../78-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 .../79-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 .../80-texlive-latex-recommended_2022.20230122-3_all.deb ... Unpacking texlive-latex-recommended (2022.20230122-3) ... Selecting previously unselected package texlive. Preparing to unpack .../81-texlive_2022.20230122-3_all.deb ... Unpacking texlive (2022.20230122-3) ... Setting up libexpat1:amd64 (2.5.0-1) ... Setting up libpipeline1:amd64 (1.5.7-1) ... Setting up libgraphite2-3:amd64 (1.3.14-1) ... Setting up libpixman-1-0:amd64 (0.42.2-1) ... Setting up libxau6:amd64 (1:1.0.9-1) ... Setting up libicu72:amd64 (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:amd64 (2.74.6-2) ... No schema files found: doing nothing. Setting up libtexluajit2:amd64 (2022.20220321.62855-5) ... Setting up libdebhelper-perl (13.11.4) ... Setting up libbrotli1:amd64 (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:amd64 (1:5.44-3) ... Setting up gettext-base (0.21-12) ... Setting up m4 (1.4.19-3) ... Setting up libzzip-0-13:amd64 (0.13.72+dfsg.1-1.1) ... Setting up file (1:5.44-3) ... Setting up autotools-dev (20220109.1) ... Setting up libx11-data (2:1.8.4-2) ... Setting up libteckit0:amd64 (2.5.11+ds1-1+b1) ... Setting up t1utils (1.41-4) ... Setting up libtexlua53-5:amd64 (2022.20220321.62855-5) ... Setting up libpng16-16:amd64 (1.6.39-2) ... Setting up autopoint (0.21-12) ... Setting up fonts-dejavu-core (2.37-6) ... Setting up libkpathsea6:amd64 (2022.20220321.62855-5) ... Setting up autoconf (2.71-3) ... Setting up sensible-utils (0.0.17+nmu1) ... Setting up libuchardet0:amd64 (0.0.7-1) ... Setting up fonts-lmodern (2.005-1) ... Setting up libsub-override-perl (0.09-4) ... Setting up libbsd0:amd64 (0.11.7-2) ... Setting up racket-common (8.7+dfsg1-1) ... Setting up libelf1:amd64 (0.188-2.1) ... Setting up libxml2:amd64 (2.9.14+dfsg-1.2) ... 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:amd64 (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:amd64 (2:1.0.10-1) ... Setting up libxdmcp6:amd64 (1:1.1.2-3) ... Setting up libxcb1:amd64 (1.15-1) ... Setting up gettext (0.21-12) ... Setting up libtool (2.4.7-5) ... Setting up libxcb-render0:amd64 (1.15-1) ... Setting up fontconfig-config (2.14.1-4) ... Setting up libxcb-shm0:amd64 (1.15-1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libptexenc1:amd64 (2022.20220321.62855-5) ... Setting up libfreetype6:amd64 (2.12.1+dfsg-5) ... 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:amd64 (2:1.8.4-2) ... Setting up libharfbuzz0b:amd64 (6.0.0+dfsg-3) ... Setting up libfontconfig1:amd64 (2.14.1-4) ... Setting up libsm6:amd64 (2:1.2.3-1) ... Setting up libpaper1:amd64 (1.1.29) ... Creating config file /etc/papersize with new version Setting up libxpm4:amd64 (1:3.5.12-1.1) ... Setting up libxrender1:amd64 (1:0.9.10-1.1) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up libxext6:amd64 (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:amd64 (1.16.0-7) ... Setting up tex-common (6.18) ... update-language: texlive-base not installed and configured, doing nothing! Setting up libxt6:amd64 (1:1.2.1-1.1) ... Setting up libxmu6:amd64 (2:1.1.3-3) ... Setting up libxi6:amd64 (2:1.8-1+b1) ... Setting up debhelper (13.11.4) ... Setting up libxaw7:amd64 (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-9) ... 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 dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 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 2024-06-03 01:49:00.545429402 -1200 +++ test.save.nodigits 2024-06-03 01:49:00.557429402 -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 ; 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 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 ; 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 ; 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) +> ; ok, ?_ can be obtained from +; ?_: all n( +; ex n all n(n n<=n) -> +; ex n all n(Succ n n<=n)) from +; n + +; ?_: ex n all n( n<=n) from +; n +> ; ok, ?_ can be obtained from +; ?_: all n( <=n) from +; n +> ; ok, ?_ can be obtained from +; ?_: all 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) from +; n n +> ; ok, we now have the new goal +; ?_: <=Succ n from +; n n n u: ; ok, ?_ is proved. The active goal now is +; ?_: all n( +; ex n all n(n n<=n) -> +; ex n all n(Succ n n<=n)) from +; n +> ; ok, we now have the new goal +; ?_: ex n all n(Succ n n<=n) from +; n n IH:ex n all n(n n<=n) +> ; ok, we now have the new goal +; ?_: ex n all n(Succ n n<=n) from +; n n n v:all n(n n<=n) +> ; ok, ?_ can be obtained from +; ?_: all n(Succ n Succ n<=n) from +; n n n v:all n(n n<=n) +> ; ok, ?_ can be obtained from +; ?_: all n(Succ n Succ n<=Succ n) from +; n n n v:all n(n n<=n) +; n + +; ?_: Succ n< -> Succ n<= from +; n n n v:all 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 u:Succ n< +> ; ok, ?_ is proved. The active goal now is +; ?_: all n(Succ n Succ n<=Succ n) from +; n n n v:all 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 u:Succ n ; ok, ?_ can be obtained from +; ?_: n n<=n) +; n n u: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) -> all n(Succ n Succ n<=n)) -> +; all n ex n all n(n n<=n) +> ; ok, we now have the new goal +; ?_: all n ex n all n(n n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +> ; ok, ?_ can be obtained from +; ?_: all n( +; ex n all n(n n<=n) -> +; ex n all n(Succ n n<=n)) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n + +; ?_: ex n all n( n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n +> ; ok, ?_ can be obtained from +; ?_: all n( <=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n +> ; ok, ?_ can be obtained from +; ?_: all n( <=Succ n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n + +; ?_: < -> <= from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n +> ; ok, we now have the new goal +; ?_: <= from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n u:< +> ; ok, ?_ is proved. The active goal now is +; ?_: all n( <=Succ n) from +; L:all n,n(all n(n n<=n) -> all n(Succ 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) -> all n(Succ n Succ n<=n)) +; n n n u: ; ok, ?_ is proved. The active goal now is +; ?_: all n( +; ex n all n(n n<=n) -> +; ex n all n(Succ n n<=n)) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n +> ; ok, we now have the new goal +; ?_: ex n all n(Succ n n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n IH:ex n all n(n n<=n) +> ; ok, we now have the new goal +; ?_: ex n all n(Succ n n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n n v:all n(n n<=n) +> ; ok, ?_ can be obtained from +; ?_: all n(Succ n Succ n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n n v:all n(n n<=n) +> ; ok, ?_ can be obtained from +; ?_: all n(n n<=n) from +; L:all n,n(all n(n n<=n) -> all n(Succ n Succ n<=n)) +; n n n v:all 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)_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)_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) +> ; ok, ?_ can be obtained from +; ?_: all n,ns( +; ex ns all ns(Lh ns Lh ns<=Lh ns) -> +; ex ns all ns(Lh(n::ns) Lh ns<=Lh ns)) from +; ns + +; ?_: ex ns all ns(Lh(Nil nat) Lh ns<=Lh ns) from +; ns +> ; ok, ?_ can be obtained from +; ?_: all ns(Lh(Nil nat) Lh : <=Lh ns) from +; ns +> ; ok, ?_ can be obtained from +; ?_: all n,ns( +; Lh(Nil nat) Lh : <=Lh(n::ns)) from +; ns ns + +; ?_: 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) ; ok, ?_ is proved. The active goal now is +; ?_: all n,ns( +; Lh(Nil nat) 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) ; ok, ?_ is proved. The active goal now is +; ?_: all n,ns( +; ex ns all ns(Lh ns Lh ns<=Lh ns) -> +; ex ns all ns(Lh(n::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) from +; ns n ns IH:ex ns all 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) from +; ns n ns ns v: +; all ns(Lh ns Lh ns<=Lh ns) +> ; ok, ?_ can be obtained from +; ?_: all ns(Lh(n::ns) Lh(::ns)<=Lh ns) from +; ns n ns ns v: +; all ns(Lh ns Lh ns<=Lh ns) +> ; ok, ?_ can be obtained from +; ?_: all n,ns( +; Lh(n::ns) Lh(::ns)<=Lh(n::ns)) from +; ns n ns ns v: +; all ns(Lh ns Lh ns<=Lh ns) +; ns + +; ?_: Lh(n::ns) Lh(::ns)<=Lh(Nil nat) from +; ns n ns ns v: +; all 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) +; ns u:Lh(n::ns) ; ok, ?_ is proved. The active goal now is +; ?_: all n,ns( +; Lh(n::ns) Lh(::ns)<=Lh(n::ns)) from +; ns n ns ns v: +; all 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) +; ns n ns u:Lh(n::ns) ; ok, ?_ can be obtained from +; ?_: Lh ns Lh ns<=Lh ns) +; ns n ns u: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) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) -> +; all ns ex ns all 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) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +> ; ok, ?_ can be obtained from +; ?_: all n,ns( +; ex ns all ns(Lh ns Lh ns<=Lh ns) -> +; ex ns all ns(Lh(n::ns) Lh ns<=Lh ns)) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns + +; ?_: ex ns all ns(Lh(Nil nat) Lh ns<=Lh ns) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns +> ; ok, ?_ can be obtained from +; ?_: all ns(Lh(Nil nat) Lh : <=Lh ns) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns +> ; ok, ?_ can be obtained from +; ?_: all n,ns( +; Lh(Nil nat) Lh : <=Lh(n::ns)) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns ns + +; ?_: Lh(Nil nat) Lh : <=Lh(Nil nat) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::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) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns ns u:Lh(Nil nat) ; ok, ?_ is proved. The active goal now is +; ?_: all n,ns( +; Lh(Nil nat) Lh : <=Lh(n::ns)) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::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) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns ns n ns u: +; Lh(Nil nat) ; ok, ?_ is proved. The active goal now is +; ?_: all n,ns( +; ex ns all ns(Lh ns Lh ns<=Lh ns) -> +; ex ns all ns(Lh(n::ns) Lh ns<=Lh ns)) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns +> ; ok, we now have the new goal +; ?_: ex ns all ns(Lh(n::ns) Lh ns<=Lh ns) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns n ns IH:ex ns all 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) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns n ns ns v: +; all ns(Lh ns Lh ns<=Lh ns) +> ; ok, ?_ can be obtained from +; ?_: all ns(Lh(n::ns) Lh(n::ns)<=Lh ns) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns n ns ns v: +; all ns(Lh ns Lh ns<=Lh ns) +> ; ok, ?_ can be obtained from +; ?_: all ns(Lh ns Lh ns<=Lh ns) from +; L:all ns,n,ns( +; all ns(Lh ns Lh ns<=Lh ns) -> +; all ns(Lh(n::ns) Lh(::ns)<=Lh ns)) +; ns n ns ns v: +; all 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 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 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 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 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 ex n R n n) from +; L:all n(all 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 ; 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_amd64.buildinfo dpkg-genchanges --build=binary -O../minlog_4.0.99.20100221-7_amd64.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/3314934 and its subdirectories I: Current time: Mon Jun 3 01:49:11 -12 2024 I: pbuilder-time-stamp: 1717422551