Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/m/minlog/minlog_4.0.99.20100221-7_all.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/minlog-4.0.99.20100221-7kbgvyr_u/minlog_4.0.99.20100221-7_all.buildinfo Get source package info: minlog=4.0.99.20100221-7 Source URL: http://snapshot.notset.fr/mr/package/minlog/4.0.99.20100221-7/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.69-14 automake=1:1.16.3-1 autopoint=0.21-3 autotools-dev=20180224.1+nmu1 base-files=11 base-passwd=3.5.48 bash=5.1-1 binutils=2.35.1-6 binutils-common=2.35.1-6 binutils-x86-64-linux-gnu=2.35.1-6 bsdextrautils=2.36.1-4 bsdutils=1:2.36.1-4 build-essential=12.8 bzip2=1.0.8-4 coreutils=8.32-4+b1 cpp=4:10.2.0-1 cpp-10=10.2.1-3 dash=0.5.11+git20200708+dd9ef66-5 debconf=1.5.74 debhelper=13.3.1 debianutils=4.11.2 dh-autoreconf=19 dh-strip-nondeterminism=1.9.0-1 diffutils=1:3.7-3 dpkg=1.20.5 dpkg-dev=1.20.5 dwz=0.13+20201015-2 file=1:5.39-3 findutils=4.7.0+git20201010-2 fontconfig-config=2.13.1-4.2 fonts-dejavu-core=2.37-2 fonts-lmodern=2.004.5-6.1 g++=4:10.2.0-1 g++-10=10.2.1-3 gcc=4:10.2.0-1 gcc-10=10.2.1-3 gcc-10-base=10.2.1-3 gettext=0.21-3 gettext-base=0.21-3 grep=3.6-1 groff-base=1.22.4-5 gzip=1.10-2 hostname=3.23 init-system-helpers=1.60 intltool-debian=0.35.0+20060710.5 libacl1=2.2.53-9 libarchive-zip-perl=1.68-1 libasan6=10.2.1-3 libatomic1=10.2.1-3 libattr1=1:2.4.48-6 libaudit-common=1:3.0-1 libaudit1=1:3.0-1 libbinutils=2.35.1-6 libblkid1=2.36.1-4 libbrotli1=1.0.9-2+b2 libbsd0=0.10.0-1 libbz2-1.0=1.0.8-4 libc-bin=2.31-6 libc-dev-bin=2.31-6 libc6=2.31-6 libc6-dev=2.31-6 libcairo2=1.16.0-4 libcap-ng0=0.7.9-2.2+b1 libcc1-0=10.2.1-3 libcom-err2=1.45.6-1 libcrypt-dev=1:4.4.17-1 libcrypt1=1:4.4.17-1 libctf-nobfd0=2.35.1-6 libctf0=2.35.1-6 libdb5.3=5.3.28+dfsg1-0.6 libdebconfclient0=0.255 libdebhelper-perl=13.3.1 libdpkg-perl=1.20.5 libelf1=0.182-2 libexpat1=2.2.10-1 libffi7=3.3-5 libfile-stripnondeterminism-perl=1.9.0-1 libfontconfig1=2.13.1-4.2 libfreetype6=2.10.4+dfsg-1 libgcc-10-dev=10.2.1-3 libgcc-s1=10.2.1-3 libgcrypt20=1.8.7-2 libgdbm-compat4=1.18.1-5.1 libgdbm6=1.18.1-5.1 libglib2.0-0=2.66.4-1 libgmp10=2:6.2.1+dfsg-1 libgomp1=10.2.1-3 libgpg-error0=1.38-2 libgraphite2-3=1.3.14-1 libgssapi-krb5-2=1.18.3-4 libharfbuzz0b=2.6.7-1 libice6=2:1.0.10-1 libicu67=67.1-5 libisl23=0.23-1 libitm1=10.2.1-3 libk5crypto3=1.18.3-4 libkeyutils1=1.6.1-2 libkpathsea6=2020.20200327.54578-5 libkrb5-3=1.18.3-4 libkrb5support0=1.18.3-4 liblsan0=10.2.1-3 liblz4-1=1.9.3-1 liblzma5=5.2.4-1+b1 libmagic-mgc=1:5.39-3 libmagic1=1:5.39-3 libmount1=2.36.1-4 libmpc3=1.2.0-1 libmpfr6=4.1.0-3 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-2 libpam-modules-bin=1.4.0-2 libpam-runtime=1.4.0-2 libpam0g=1.4.0-2 libpaper-utils=1.1.28+b1 libpaper1=1.1.28+b1 libpcre2-8-0=10.36-2 libpcre3=2:8.39-13 libperl5.32=5.32.0-6 libpipeline1=1.5.3-1 libpixman-1-0=0.40.0-1 libpng16-16=1.6.37-3 libptexenc1=2020.20200327.54578-5 libquadmath0=10.2.1-3 libseccomp2=2.5.1-1 libselinux1=3.1-2+b2 libsigsegv2=2.12-3 libsm6=2:1.2.3-1 libsmartcols1=2.36.1-4 libssl1.1=1.1.1i-1 libstdc++-10-dev=10.2.1-3 libstdc++6=10.2.1-3 libsub-override-perl=0.09-2 libsynctex2=2020.20200327.54578-5 libsystemd0=247.2-3 libteckit0=2.5.10+ds1-3 libtexlua53=2020.20200327.54578-5 libtexluajit2=2020.20200327.54578-5 libtinfo6=6.2+20201114-1 libtirpc-common=1.2.6-3 libtirpc-dev=1.2.6-3 libtirpc3=1.2.6-3 libtool=2.4.6-14 libtsan0=10.2.1-3 libubsan1=10.2.1-3 libuchardet0=0.0.7-1 libudev1=247.2-3 libunistring2=0.9.10-4 libuuid1=2.36.1-4 libx11-6=2:1.6.12-1 libx11-data=2:1.6.12-1 libxau6=1:1.0.8-1+b2 libxaw7=2:1.0.13-1.1 libxcb-render0=1.14-2.1 libxcb-shm0=1.14-2.1 libxcb1=1.14-2.1 libxdmcp6=1:1.1.2-3 libxext6=2:1.3.3-1.1 libxi6=2:1.7.10-1 libxml2=2.9.10+dfsg-6.3+b1 libxmu6=2:1.1.2-2+b3 libxpm4=1:3.5.12-1 libxrender1=1:0.9.10-1 libxt6=1:1.2.0-1 libzstd1=1.4.8+dfsg-1 libzzip-0-13=0.13.62-3.2 linux-libc-dev=5.9.15-1 login=1:4.8.1-1 lsb-base=11.1.0 m4=1.4.18-4 make=4.3-4 man-db=2.9.3-2 mawk=1.3.4.20200120-2 ncurses-base=6.2+20201114-1 ncurses-bin=6.2+20201114-1 patch=2.7.6-6 perl=5.32.0-6 perl-base=5.32.0-6 perl-modules-5.32=5.32.0-6 po-debconf=1.0.21+nmu1 racket=7.9+dfsg1-1 racket-common=7.9+dfsg1-1 sed=4.7-1 sensible-utils=0.0.12+nmu1 sysvinit-utils=2.96-5 t1utils=1.41-4 tar=1.32+dfsg-1 tex-common=6.15 texlive=2020.20201203-2 texlive-base=2020.20201203-2 texlive-binaries=2020.20200327.54578-5 texlive-fonts-recommended=2020.20201203-2 texlive-latex-base=2020.20201203-2 texlive-latex-recommended=2020.20201203-2 ucf=3.0043 util-linux=2.36.1-4 x11-common=1:7.7+21 xdg-utils=1.1.3-2 xz-utils=5.2.4-1+b1 zlib1g=1:1.2.11.dfsg-2 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20210106T142920Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20201230T203527Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d minlog=4.0.99.20100221-7 && mkdir -p /build/minlog-X70YFG && dpkg-source --no-check -x /*.dsc /build/minlog-X70YFG/minlog-4.0.99.20100221 && chown -R builduser:builduser /build/minlog-X70YFG" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/minlog-X70YFG/minlog-4.0.99.20100221 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1609455882" dpkg-buildpackage -uc -a amd64 --build=all" --customize-hook=sync-out /build/minlog-X70YFG /tmp/minlog-4.0.99.20100221-7kbgvyr_u bullseye /dev/null deb http://snapshot.notset.fr/archive/debian/20201230T203527Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: tar I: using /tmp/mmdebstrap.I0IkCPlFbf as tempdir I: running apt-get update... I: downloading packages with apt... I: extracting archives... I: installing essential packages... I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "apt-get --yes install fakeroot util-linux"' exec /tmp/mmdebstrap.I0IkCPlFbf Reading package lists... Building dependency tree... util-linux is already the newest version (2.36.1-4). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 134 kB of archives. After this operation, 397 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20201230T203527Z unstable/main amd64 libfakeroot amd64 1.25.3-1.1 [47.0 kB] Get:2 http://snapshot.notset.fr/archive/debian/20201230T203527Z unstable/main amd64 fakeroot amd64 1.25.3-1.1 [87.0 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 134 kB in 0s (1071 kB/s) Selecting previously unselected package libfakeroot:amd64. (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 ... 4648 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.25.3-1.1_amd64.deb ... Unpacking libfakeroot:amd64 (1.25.3-1.1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.25.3-1.1_amd64.deb ... Unpacking fakeroot (1.25.3-1.1) ... Setting up libfakeroot:amd64 (1.25.3-1.1) ... Setting up fakeroot (1.25.3-1.1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.31-6) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20210106T142920Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20201230T203527Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.I0IkCPlFbf Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm InRelease [81.6 kB] Get:2 http://snapshot.notset.fr/archive/debian/20210106T142920Z unstable InRelease [153 kB] Hit:3 http://snapshot.notset.fr/archive/debian/20201230T203527Z unstable InRelease Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Get:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources [11.4 MB] Get:5 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages [11.1 MB] Ign:6 http://snapshot.notset.fr/archive/debian/20210106T142920Z unstable/main amd64 Packages Ign:6 http://snapshot.notset.fr/archive/debian/20210106T142920Z unstable/main amd64 Packages Ign:6 http://snapshot.notset.fr/archive/debian/20210106T142920Z unstable/main amd64 Packages Get:6 http://snapshot.notset.fr/archive/debian/20210106T142920Z unstable/main amd64 Packages [11.6 MB] Fetched 34.3 MB in 32s (1083 kB/s) Reading package lists... I: installing remaining packages inside the chroot... I: running --customize-hook in shell: sh -c 'chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash' exec /tmp/mmdebstrap.I0IkCPlFbf I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d minlog=4.0.99.20100221-7 && mkdir -p /build/minlog-X70YFG && dpkg-source --no-check -x /*.dsc /build/minlog-X70YFG/minlog-4.0.99.20100221 && chown -R builduser:builduser /build/minlog-X70YFG"' exec /tmp/mmdebstrap.I0IkCPlFbf Reading package lists... NOTICE: 'minlog' packaging is maintained in the 'Git' version control system at: https://git.dgit.debian.org/minlog.git Please use: git clone https://git.dgit.debian.org/minlog.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 1187 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main minlog 4.0.99.20100221-7 (dsc) [1464 B] Get:2 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main minlog 4.0.99.20100221-7 (tar) [1181 kB] Get:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main minlog 4.0.99.20100221-7 (diff) [4616 B] Fetched 1187 kB in 1s (1116 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'minlog_4.0.99.20100221-7.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting minlog in /build/minlog-X70YFG/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: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/minlog-X70YFG/minlog-4.0.99.20100221 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1609455882" dpkg-buildpackage -uc -a amd64 --build=all"' exec /tmp/mmdebstrap.I0IkCPlFbf 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 . debian/rules clean dh clean --no-parallel dh_auto_clean -O--no-parallel make -j1 clean make[1]: Entering directory '/build/minlog-X70YFG/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-X70YFG/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-X70YFG/minlog-4.0.99.20100221/src' (cd doc; make clean) make[2]: Entering directory '/build/minlog-X70YFG/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-X70YFG/minlog-4.0.99.20100221/doc' (cd examples; make clean) make[2]: Entering directory '/build/minlog-X70YFG/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-X70YFG/minlog-4.0.99.20100221/examples/classical' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/classical' (cd hounif; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/hounif' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/hounif' (cd prop; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/prop' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/prop' (cd quant; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/quant' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/quant' (cd warshall; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/warshall' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/warshall' (cd dijkstra; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/dijkstra' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/dijkstra' (cd bar; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/bar' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/bar' (cd dc; make clean) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/dc' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/dc' (cd arith; make clean) make[3]: Entering directory '/build/minlog-X70YFG/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-X70YFG/minlog-4.0.99.20100221/examples/arith/quotrem' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[4]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/arith/quotrem' make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples/arith' make[2]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/examples' make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_autoreconf_clean -O--no-parallel dh_clean -O--no-parallel debian/rules binary-indep dh binary-indep --no-parallel dh_update_autotools_config -i -O--no-parallel dh_autoreconf -i -O--no-parallel dh_auto_configure -i -O--no-parallel dh_auto_build -i -O--no-parallel make -j1 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[2]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/src' make[2]: Nothing to be done for '.dep.notags'. make[2]: Leaving directory '/build/minlog-X70YFG/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-X70YFG/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.7182818 (TeX Live 2020/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-X70YFG/minlog-4.0.99.20100221/debian/.debhelper/generated/_source/home/.texlive2020/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-X70YFG/minlog-4.0.99.20100221/doc' make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' debian/rules override_dh_auto_test make[1]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_auto_test || echo 'WARNING: Test suite failures' make -j1 test make[2]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/src' make[3]: Nothing to be done for '.dep.notags'. make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/src' (cd examples; make .TEST) make[3]: Entering directory '/build/minlog-X70YFG/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-X70YFG/minlog-4.0.99.20100221/examples --- test.out.nodigits 2021-10-09 09:27:28.910883481 +0000 +++ test.save.nodigits 2021-10-09 09:27:28.970883078 +0000 @@ -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-X70YFG/minlog-4.0.99.20100221/examples' make[2]: *** [Makefile:81: examples/.TEST] Error 2 make[2]: Leaving directory '/build/minlog-X70YFG/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-X70YFG/minlog-4.0.99.20100221/examples \ -name '*.diff' \ -delete find /build/minlog-X70YFG/minlog-4.0.99.20100221/examples \ -name '*.out' \ -delete find /build/minlog-X70YFG/minlog-4.0.99.20100221/examples \ -name '*.nodigits' \ -delete make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' create-stamp debian/debhelper-build-stamp dh_testroot -i -O--no-parallel dh_prep -i -O--no-parallel debian/rules override_dh_auto_install make[1]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_auto_install -- DESTDIR=/usr PREFIX=/build/minlog-X70YFG/minlog-4.0.99.20100221/debian/minlog make -j1 install DESTDIR=/build/minlog-X70YFG/minlog-4.0.99.20100221/debian/minlog AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" DESTDIR=/usr PREFIX=/build/minlog-X70YFG/minlog-4.0.99.20100221/debian/minlog make[2]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[3]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/src' make[3]: Nothing to be done for '.dep.notags'. make[3]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221/src' install --strip-program=true -p -d -m 755 /build/minlog-X70YFG/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog /build/minlog-X70YFG/minlog-4.0.99.20100221/debian/minlog/usr/bin /build/minlog-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/minlog-4.0.99.20100221/debian/minlog/usr/bin/minlog chmod a+x /build/minlog-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/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-X70YFG/minlog-4.0.99.20100221' make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_installdocs -i -O--no-parallel dh_installchangelogs -i -O--no-parallel debian/rules override_dh_installman make[1]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_installman debian/minlog.1 make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_installsystemduser -i -O--no-parallel dh_perl -i -O--no-parallel dh_link -i -O--no-parallel dh_strip_nondeterminism -i -O--no-parallel debian/rules override_dh_compress make[1]: Entering directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_compress --exclude=minlog/examples --exclude=.pdf make[1]: Leaving directory '/build/minlog-X70YFG/minlog-4.0.99.20100221' dh_fixperms -i -O--no-parallel dh_missing -i -O--no-parallel dh_installdeb -i -O--no-parallel dh_gencontrol -i -O--no-parallel dh_md5sums -i -O--no-parallel dh_builddeb -i -O--no-parallel dpkg-deb: building package 'minlog' in '../minlog_4.0.99.20100221-7_all.deb'. dpkg-genbuildinfo --build=all dpkg-genchanges --build=all >../minlog_4.0.99.20100221-7_all.changes dpkg-genchanges: info: binary-only arch-indep upload (source code and arch-specific packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/minlog-X70YFG /tmp/minlog-4.0.99.20100221-7kbgvyr_u I: cleaning package lists and apt cache... I: creating tarball... I: done I: removing tempdir /tmp/mmdebstrap.I0IkCPlFbf... I: success in 577.6503 seconds md5: minlog_4.0.99.20100221-7_all.deb: OK sha1: minlog_4.0.99.20100221-7_all.deb: OK sha256: minlog_4.0.99.20100221-7_all.deb: OK Checksums: OK