I: pbuilder: network access will be disabled during build I: Current time: Fri Apr 5 15:21:33 +14 2024 I: pbuilder-time-stamp: 1712280093 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration W: --override-config is not set; not updating apt.conf Read the manpage for details. I: mounting /proc filesystem I: mounting /sys filesystem I: creating /{dev,run}/shm I: mounting /dev/pts filesystem I: redirecting /dev/ptmx to /dev/pts/ptmx I: policy-rc.d already exists I: Copying source file I: copying [minlog_4.0.99.20100221-7.dsc] I: copying [./minlog_4.0.99.20100221.orig.tar.gz] I: copying [./minlog_4.0.99.20100221-7.debian.tar.xz] I: Extracting source gpgv: Signature made Thu Dec 31 23:07:33 2020 gpgv: using EDDSA key 658073613BFCC5C7E2E45D45DC518FC87F9716AA gpgv: issuer "vagrant@reproducible-builds.org" gpgv: Can't check signature: No public key dpkg-source: warning: cannot verify inline signature for ./minlog_4.0.99.20100221-7.dsc: no acceptable signature found dpkg-source: info: extracting minlog in minlog-4.0.99.20100221 dpkg-source: info: unpacking minlog_4.0.99.20100221.orig.tar.gz dpkg-source: info: unpacking minlog_4.0.99.20100221-7.debian.tar.xz I: Not using root during the build. I: Installing the build-deps I: user script /srv/workspace/pbuilder/21219/tmp/hooks/D01_modify_environment starting debug: Running on virt32z. I: Changing host+domainname to test build reproducibility I: Adding a custom variable just for the fun of it... I: Changing /bin/sh to bash '/bin/sh' -> '/bin/bash' lrwxrwxrwx 1 root root 9 Apr 5 01:21 /bin/sh -> /bin/bash I: Setting pbuilder2's login shell to /bin/bash I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other I: user script /srv/workspace/pbuilder/21219/tmp/hooks/D01_modify_environment finished I: user script /srv/workspace/pbuilder/21219/tmp/hooks/D02_print_environment starting I: set BASH=/bin/sh BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath BASH_ALIASES=() BASH_ARGC=() BASH_ARGV=() BASH_CMDS=() BASH_LINENO=([0]="12" [1]="0") BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") BASH_VERSINFO=([0]="5" [1]="2" [2]="21" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") BASH_VERSION='5.2.21(1)-release' BUILDDIR=/build/reproducible-path BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' BUILDUSERNAME=pbuilder2 BUILD_ARCH=armhf DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' DIRSTACK=() DISTRIBUTION=trixie EUID=0 FUNCNAME=([0]="Echo" [1]="main") GROUPS=() HOME=/root HOSTNAME=i-capture-the-hostname HOSTTYPE=arm HOST_ARCH=armhf IFS=' ' INVOCATION_ID=1e178cde85c44062aa56a227f5153852 LANG=C LANGUAGE=it_CH:it LC_ALL=C MACHTYPE=arm-unknown-linux-gnueabihf MAIL=/var/mail/root OPTERR=1 OPTIND=1 OSTYPE=linux-gnueabihf PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path PBCURRENTCOMMANDLINEOPERATION=build PBUILDER_OPERATION=build PBUILDER_PKGDATADIR=/usr/share/pbuilder PBUILDER_PKGLIBDIR=/usr/lib/pbuilder PBUILDER_SYSCONFDIR=/etc PIPESTATUS=([0]="0") POSIXLY_CORRECT=y PPID=21219 PS4='+ ' PWD=/ SHELL=/bin/bash SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix SHLVL=3 SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.LjwEz7vW/pbuilderrc_jKDN --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.LjwEz7vW/b2 --logfile b2/build.log minlog_4.0.99.20100221-7.dsc' SUDO_GID=110 SUDO_UID=103 SUDO_USER=jenkins TERM=unknown TZ=/usr/share/zoneinfo/Etc/GMT-14 UID=0 USER=root _='I: set' http_proxy=http://10.0.0.15:3142/ I: uname -a Linux i-capture-the-hostname 6.1.0-18-armmp-lpae #1 SMP Debian 6.1.76-1 (2024-02-01) armv7l GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Apr 4 11:25 /bin -> usr/bin I: user script /srv/workspace/pbuilder/21219/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy Version: 0.invalid.0 Architecture: armhf Maintainer: Debian Pbuilder Team Description: Dummy package to satisfy dependencies with aptitude - created by pbuilder This package was created automatically by pbuilder to satisfy the build-dependencies of the package being currently built. Depends: debhelper-compat (= 13), racket, texlive (>= 2007-11) dpkg-deb: building package 'pbuilder-satisfydepends-dummy' in '/tmp/satisfydepends-aptitude/pbuilder-satisfydepends-dummy.deb'. Selecting previously unselected package pbuilder-satisfydepends-dummy. (Reading database ... 19637 files and directories currently installed.) Preparing to unpack .../pbuilder-satisfydepends-dummy.deb ... Unpacking pbuilder-satisfydepends-dummy (0.invalid.0) ... dpkg: pbuilder-satisfydepends-dummy: dependency problems, but configuring anyway as you requested: pbuilder-satisfydepends-dummy depends on debhelper-compat (= 13); however: Package debhelper-compat is not installed. pbuilder-satisfydepends-dummy depends on racket; however: Package racket is not installed. pbuilder-satisfydepends-dummy depends on texlive (>= 2007-11); however: Package texlive is not installed. Setting up pbuilder-satisfydepends-dummy (0.invalid.0) ... Reading package lists... Building dependency tree... Reading state information... Initializing package states... Writing extended state information... Building tag database... pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0) pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0) The following NEW packages will be installed: autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} debhelper{a} dh-autoreconf{a} dh-strip-nondeterminism{a} dwz{a} file{a} fontconfig-config{a} fonts-dejavu-core{a} fonts-dejavu-mono{a} fonts-lmodern{a} gettext{a} gettext-base{a} groff-base{a} intltool-debian{a} libarchive-zip-perl{a} libbrotli1{a} libbsd0{a} libcairo2{a} libdebhelper-perl{a} libelf1{a} libexpat1{a} libfile-stripnondeterminism-perl{a} libfontconfig1{a} libfreetype6{a} libglib2.0-0{a} libgraphite2-3{a} libharfbuzz0b{a} libice6{a} libicu72{a} libkpathsea6{a} libmagic-mgc{a} libmagic1{a} libpaper-utils{a} libpaper1{a} libpipeline1{a} libpixman-1-0{a} libpng16-16{a} libpotrace0{a} libptexenc1{a} libsm6{a} libsub-override-perl{a} libsynctex2{a} libteckit0{a} libtexlua53-5{a} libtool{a} libuchardet0{a} libx11-6{a} libx11-data{a} libxau6{a} libxaw7{a} libxcb-render0{a} libxcb-shm0{a} libxcb1{a} libxdmcp6{a} libxext6{a} libxi6{a} libxml2{a} libxmu6{a} libxpm4{a} libxrender1{a} libxt6{a} libzzip-0-13{a} m4{a} man-db{a} po-debconf{a} racket{a} racket-common{a} sensible-utils{a} t1utils{a} tex-common{a} texlive{a} texlive-base{a} texlive-binaries{a} texlive-fonts-recommended{a} texlive-latex-base{a} texlive-latex-recommended{a} ucf{a} x11-common{a} xdg-utils{a} The following packages are RECOMMENDED but will NOT be installed: curl dvisvgm libarchive-cpio-perl libfile-mimeinfo-perl libgdk-pixbuf-2.0-0 libgdk-pixbuf-xlib-2.0-0 libglib2.0-data libgtk2.0-0 libjpeg62-turbo libltdl-dev libmail-sendmail-perl libnet-dbus-perl libpangocairo-1.0-0 libx11-protocol-perl lmodern lynx racket-doc shared-mime-info tex-gyre tipa wget x11-utils x11-xserver-utils xdg-user-dirs 0 packages upgraded, 83 newly installed, 0 to remove and 0 not upgraded. Need to get 207 MB of archives. After unpacking 702 MB will be used. Writing extended state information... Get: 1 http://deb.debian.org/debian trixie/main armhf sensible-utils all 0.0.22 [22.4 kB] Get: 2 http://deb.debian.org/debian trixie/main armhf libmagic-mgc armhf 1:5.45-2+b1 [314 kB] Get: 3 http://deb.debian.org/debian trixie/main armhf libmagic1 armhf 1:5.45-2+b1 [97.9 kB] Get: 4 http://deb.debian.org/debian trixie/main armhf file armhf 1:5.45-2+b1 [42.2 kB] Get: 5 http://deb.debian.org/debian trixie/main armhf gettext-base armhf 0.21-14+b1 [157 kB] Get: 6 http://deb.debian.org/debian trixie/main armhf libuchardet0 armhf 0.0.8-1+b1 [65.7 kB] Get: 7 http://deb.debian.org/debian trixie/main armhf groff-base armhf 1.23.0-3 [1088 kB] Get: 8 http://deb.debian.org/debian trixie/main armhf bsdextrautils armhf 2.39.3-6 [81.2 kB] Get: 9 http://deb.debian.org/debian trixie/main armhf libpipeline1 armhf 1.5.7-1+b2 [33.4 kB] Get: 10 http://deb.debian.org/debian trixie/main armhf man-db armhf 2.12.0-3 [1367 kB] Get: 11 http://deb.debian.org/debian trixie/main armhf ucf all 3.0043+nmu1 [55.2 kB] Get: 12 http://deb.debian.org/debian trixie/main armhf m4 armhf 1.4.19-4 [264 kB] Get: 13 http://deb.debian.org/debian trixie/main armhf autoconf all 2.71-3 [332 kB] Get: 14 http://deb.debian.org/debian trixie/main armhf autotools-dev all 20220109.1 [51.6 kB] Get: 15 http://deb.debian.org/debian trixie/main armhf automake all 1:1.16.5-1.3 [823 kB] Get: 16 http://deb.debian.org/debian trixie/main armhf autopoint all 0.21-14 [496 kB] Get: 17 http://deb.debian.org/debian trixie/main armhf libdebhelper-perl all 13.15.3 [88.0 kB] Get: 18 http://deb.debian.org/debian trixie/main armhf libtool all 2.4.7-7 [517 kB] Get: 19 http://deb.debian.org/debian trixie/main armhf dh-autoreconf all 20 [17.1 kB] Get: 20 http://deb.debian.org/debian trixie/main armhf libarchive-zip-perl all 1.68-1 [104 kB] Get: 21 http://deb.debian.org/debian trixie/main armhf libsub-override-perl all 0.10-1 [10.6 kB] Get: 22 http://deb.debian.org/debian trixie/main armhf libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB] Get: 23 http://deb.debian.org/debian trixie/main armhf dh-strip-nondeterminism all 1.13.1-1 [8620 B] Get: 24 http://deb.debian.org/debian trixie/main armhf libelf1 armhf 0.190-1+b1 [171 kB] Get: 25 http://deb.debian.org/debian trixie/main armhf dwz armhf 0.15-1 [101 kB] Get: 26 http://deb.debian.org/debian trixie/main armhf libicu72 armhf 72.1-4+b1 [9070 kB] Get: 27 http://deb.debian.org/debian trixie/main armhf libxml2 armhf 2.9.14+dfsg-1.3+b2 [599 kB] Get: 28 http://deb.debian.org/debian trixie/main armhf gettext armhf 0.21-14+b1 [1230 kB] Get: 29 http://deb.debian.org/debian trixie/main armhf intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get: 30 http://deb.debian.org/debian trixie/main armhf po-debconf all 1.0.21+nmu1 [248 kB] Get: 31 http://deb.debian.org/debian trixie/main armhf debhelper all 13.15.3 [901 kB] Get: 32 http://deb.debian.org/debian trixie/main armhf fonts-dejavu-mono all 2.37-8 [489 kB] Get: 33 http://deb.debian.org/debian trixie/main armhf fonts-dejavu-core all 2.37-8 [840 kB] Get: 34 http://deb.debian.org/debian trixie/main armhf fontconfig-config armhf 2.15.0-1.1 [317 kB] Get: 35 http://deb.debian.org/debian trixie/main armhf fonts-lmodern all 2.005-1 [4540 kB] Get: 36 http://deb.debian.org/debian trixie/main armhf libbrotli1 armhf 1.1.0-2+b3 [284 kB] Get: 37 http://deb.debian.org/debian trixie/main armhf libbsd0 armhf 0.12.2-1 [127 kB] Get: 38 http://deb.debian.org/debian trixie/main armhf libexpat1 armhf 2.5.0-2+b2 [80.2 kB] Get: 39 http://deb.debian.org/debian trixie/main armhf libpng16-16 armhf 1.6.43-1 [262 kB] Get: 40 http://deb.debian.org/debian trixie/main armhf libfreetype6 armhf 2.13.2+dfsg-1+b1 [371 kB] Get: 41 http://deb.debian.org/debian trixie/main armhf libfontconfig1 armhf 2.15.0-1.1 [370 kB] Get: 42 http://deb.debian.org/debian trixie/main armhf libpixman-1-0 armhf 0.42.2-1+b1 [476 kB] Get: 43 http://deb.debian.org/debian trixie/main armhf libxau6 armhf 1:1.0.9-1 [19.0 kB] Get: 44 http://deb.debian.org/debian trixie/main armhf libxdmcp6 armhf 1:1.1.2-3 [24.9 kB] Get: 45 http://deb.debian.org/debian trixie/main armhf libxcb1 armhf 1.15-1 [140 kB] Get: 46 http://deb.debian.org/debian trixie/main armhf libx11-data all 2:1.8.7-1 [328 kB] Get: 47 http://deb.debian.org/debian trixie/main armhf libx11-6 armhf 2:1.8.7-1 [735 kB] Get: 48 http://deb.debian.org/debian trixie/main armhf libxcb-render0 armhf 1.15-1 [114 kB] Get: 49 http://deb.debian.org/debian trixie/main armhf libxcb-shm0 armhf 1.15-1 [106 kB] Get: 50 http://deb.debian.org/debian trixie/main armhf libxext6 armhf 2:1.3.4-1+b1 [47.8 kB] Get: 51 http://deb.debian.org/debian trixie/main armhf libxrender1 armhf 1:0.9.10-1.1 [30.1 kB] Get: 52 http://deb.debian.org/debian trixie/main armhf libcairo2 armhf 1.18.0-1+b1 [441 kB] Get: 53 http://deb.debian.org/debian trixie/main armhf libglib2.0-0 armhf 2.78.4-1 [1281 kB] Get: 54 http://deb.debian.org/debian trixie/main armhf libgraphite2-3 armhf 1.3.14-2 [63.2 kB] Get: 55 http://deb.debian.org/debian trixie/main armhf libharfbuzz0b armhf 8.3.0-2 [2155 kB] Get: 56 http://deb.debian.org/debian trixie/main armhf x11-common all 1:7.7+23 [252 kB] Get: 57 http://deb.debian.org/debian trixie/main armhf libice6 armhf 2:1.0.10-1 [51.9 kB] Get: 58 http://deb.debian.org/debian trixie/main armhf libkpathsea6 armhf 2023.20230311.66589-9 [144 kB] Get: 59 http://deb.debian.org/debian trixie/main armhf libpaper1 armhf 1.1.29 [11.9 kB] Get: 60 http://deb.debian.org/debian trixie/main armhf libpaper-utils armhf 1.1.29 [8400 B] Get: 61 http://deb.debian.org/debian trixie/main armhf libpotrace0 armhf 1.16-2+b1 [22.6 kB] Get: 62 http://deb.debian.org/debian trixie/main armhf libptexenc1 armhf 2023.20230311.66589-9 [42.8 kB] Get: 63 http://deb.debian.org/debian trixie/main armhf libsm6 armhf 2:1.2.3-1 [33.0 kB] Get: 64 http://deb.debian.org/debian trixie/main armhf libsynctex2 armhf 2023.20230311.66589-9 [48.5 kB] Get: 65 http://deb.debian.org/debian trixie/main armhf libteckit0 armhf 2.5.12+ds1-1 [259 kB] Get: 66 http://deb.debian.org/debian trixie/main armhf libtexlua53-5 armhf 2023.20230311.66589-9 [82.2 kB] Get: 67 http://deb.debian.org/debian trixie/main armhf libxt6 armhf 1:1.2.1-1.1 [157 kB] Get: 68 http://deb.debian.org/debian trixie/main armhf libxmu6 armhf 2:1.1.3-3 [52.6 kB] Get: 69 http://deb.debian.org/debian trixie/main armhf libxpm4 armhf 1:3.5.17-1 [49.5 kB] Get: 70 http://deb.debian.org/debian trixie/main armhf libxaw7 armhf 2:1.0.14-1 [167 kB] Get: 71 http://deb.debian.org/debian trixie/main armhf libxi6 armhf 2:1.8.1-1 [73.8 kB] Get: 72 http://deb.debian.org/debian trixie/main armhf libzzip-0-13 armhf 0.13.72+dfsg.1-1.1+b1 [52.3 kB] Get: 73 http://deb.debian.org/debian trixie/main armhf racket-common all 8.12+dfsg1-7 [15.6 MB] Get: 74 http://deb.debian.org/debian trixie/main armhf racket armhf 8.12+dfsg1-7 [114 MB] Get: 75 http://deb.debian.org/debian trixie/main armhf t1utils armhf 1.41-4 [54.7 kB] Get: 76 http://deb.debian.org/debian trixie/main armhf tex-common all 6.18 [32.5 kB] Get: 77 http://deb.debian.org/debian trixie/main armhf texlive-binaries armhf 2023.20230311.66589-9 [6071 kB] Get: 78 http://deb.debian.org/debian trixie/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 79 http://deb.debian.org/debian trixie/main armhf texlive-base all 2023.20240207-1 [22.0 MB] Get: 80 http://deb.debian.org/debian trixie/main armhf texlive-fonts-recommended all 2023.20240207-1 [4990 kB] Get: 81 http://deb.debian.org/debian trixie/main armhf texlive-latex-base all 2023.20240207-1 [1255 kB] Get: 82 http://deb.debian.org/debian trixie/main armhf texlive-latex-recommended all 2023.20240207-1 [8843 kB] Get: 83 http://deb.debian.org/debian trixie/main armhf texlive all 2023.20240207-1 [18.2 kB] Fetched 207 MB in 2s (86.8 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package sensible-utils. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19637 files and directories currently installed.) Preparing to unpack .../00-sensible-utils_0.0.22_all.deb ... Unpacking sensible-utils (0.0.22) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../01-libmagic-mgc_1%3a5.45-2+b1_armhf.deb ... Unpacking libmagic-mgc (1:5.45-2+b1) ... Selecting previously unselected package libmagic1:armhf. Preparing to unpack .../02-libmagic1_1%3a5.45-2+b1_armhf.deb ... Unpacking libmagic1:armhf (1:5.45-2+b1) ... Selecting previously unselected package file. Preparing to unpack .../03-file_1%3a5.45-2+b1_armhf.deb ... Unpacking file (1:5.45-2+b1) ... Selecting previously unselected package gettext-base. Preparing to unpack .../04-gettext-base_0.21-14+b1_armhf.deb ... Unpacking gettext-base (0.21-14+b1) ... Selecting previously unselected package libuchardet0:armhf. Preparing to unpack .../05-libuchardet0_0.0.8-1+b1_armhf.deb ... Unpacking libuchardet0:armhf (0.0.8-1+b1) ... Selecting previously unselected package groff-base. Preparing to unpack .../06-groff-base_1.23.0-3_armhf.deb ... Unpacking groff-base (1.23.0-3) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../07-bsdextrautils_2.39.3-6_armhf.deb ... Unpacking bsdextrautils (2.39.3-6) ... Selecting previously unselected package libpipeline1:armhf. Preparing to unpack .../08-libpipeline1_1.5.7-1+b2_armhf.deb ... Unpacking libpipeline1:armhf (1.5.7-1+b2) ... Selecting previously unselected package man-db. Preparing to unpack .../09-man-db_2.12.0-3_armhf.deb ... Unpacking man-db (2.12.0-3) ... Selecting previously unselected package ucf. Preparing to unpack .../10-ucf_3.0043+nmu1_all.deb ... Moving old data out of the way Unpacking ucf (3.0043+nmu1) ... Selecting previously unselected package m4. Preparing to unpack .../11-m4_1.4.19-4_armhf.deb ... Unpacking m4 (1.4.19-4) ... Selecting previously unselected package autoconf. Preparing to unpack .../12-autoconf_2.71-3_all.deb ... Unpacking autoconf (2.71-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../13-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../14-automake_1%3a1.16.5-1.3_all.deb ... Unpacking automake (1:1.16.5-1.3) ... Selecting previously unselected package autopoint. Preparing to unpack .../15-autopoint_0.21-14_all.deb ... Unpacking autopoint (0.21-14) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../16-libdebhelper-perl_13.15.3_all.deb ... Unpacking libdebhelper-perl (13.15.3) ... Selecting previously unselected package libtool. Preparing to unpack .../17-libtool_2.4.7-7_all.deb ... Unpacking libtool (2.4.7-7) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../18-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../19-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libsub-override-perl. Preparing to unpack .../20-libsub-override-perl_0.10-1_all.deb ... Unpacking libsub-override-perl (0.10-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../21-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../22-dh-strip-nondeterminism_1.13.1-1_all.deb ... Unpacking dh-strip-nondeterminism (1.13.1-1) ... Selecting previously unselected package libelf1:armhf. Preparing to unpack .../23-libelf1_0.190-1+b1_armhf.deb ... Unpacking libelf1:armhf (0.190-1+b1) ... Selecting previously unselected package dwz. Preparing to unpack .../24-dwz_0.15-1_armhf.deb ... Unpacking dwz (0.15-1) ... Selecting previously unselected package libicu72:armhf. Preparing to unpack .../25-libicu72_72.1-4+b1_armhf.deb ... Unpacking libicu72:armhf (72.1-4+b1) ... Selecting previously unselected package libxml2:armhf. Preparing to unpack .../26-libxml2_2.9.14+dfsg-1.3+b2_armhf.deb ... Unpacking libxml2:armhf (2.9.14+dfsg-1.3+b2) ... Selecting previously unselected package gettext. Preparing to unpack .../27-gettext_0.21-14+b1_armhf.deb ... Unpacking gettext (0.21-14+b1) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../28-intltool-debian_0.35.0+20060710.6_all.deb ... Unpacking intltool-debian (0.35.0+20060710.6) ... Selecting previously unselected package po-debconf. Preparing to unpack .../29-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../30-debhelper_13.15.3_all.deb ... Unpacking debhelper (13.15.3) ... Selecting previously unselected package fonts-dejavu-mono. Preparing to unpack .../31-fonts-dejavu-mono_2.37-8_all.deb ... Unpacking fonts-dejavu-mono (2.37-8) ... Selecting previously unselected package fonts-dejavu-core. Preparing to unpack .../32-fonts-dejavu-core_2.37-8_all.deb ... Unpacking fonts-dejavu-core (2.37-8) ... Selecting previously unselected package fontconfig-config. Preparing to unpack .../33-fontconfig-config_2.15.0-1.1_armhf.deb ... Unpacking fontconfig-config (2.15.0-1.1) ... Selecting previously unselected package fonts-lmodern. Preparing to unpack .../34-fonts-lmodern_2.005-1_all.deb ... Unpacking fonts-lmodern (2.005-1) ... Selecting previously unselected package libbrotli1:armhf. Preparing to unpack .../35-libbrotli1_1.1.0-2+b3_armhf.deb ... Unpacking libbrotli1:armhf (1.1.0-2+b3) ... Selecting previously unselected package libbsd0:armhf. Preparing to unpack .../36-libbsd0_0.12.2-1_armhf.deb ... Unpacking libbsd0:armhf (0.12.2-1) ... Selecting previously unselected package libexpat1:armhf. Preparing to unpack .../37-libexpat1_2.5.0-2+b2_armhf.deb ... Unpacking libexpat1:armhf (2.5.0-2+b2) ... Selecting previously unselected package libpng16-16:armhf. Preparing to unpack .../38-libpng16-16_1.6.43-1_armhf.deb ... Unpacking libpng16-16:armhf (1.6.43-1) ... Selecting previously unselected package libfreetype6:armhf. Preparing to unpack .../39-libfreetype6_2.13.2+dfsg-1+b1_armhf.deb ... Unpacking libfreetype6:armhf (2.13.2+dfsg-1+b1) ... Selecting previously unselected package libfontconfig1:armhf. Preparing to unpack .../40-libfontconfig1_2.15.0-1.1_armhf.deb ... Unpacking libfontconfig1:armhf (2.15.0-1.1) ... Selecting previously unselected package libpixman-1-0:armhf. Preparing to unpack .../41-libpixman-1-0_0.42.2-1+b1_armhf.deb ... Unpacking libpixman-1-0:armhf (0.42.2-1+b1) ... Selecting previously unselected package libxau6:armhf. Preparing to unpack .../42-libxau6_1%3a1.0.9-1_armhf.deb ... Unpacking libxau6:armhf (1:1.0.9-1) ... Selecting previously unselected package libxdmcp6:armhf. Preparing to unpack .../43-libxdmcp6_1%3a1.1.2-3_armhf.deb ... Unpacking libxdmcp6:armhf (1:1.1.2-3) ... Selecting previously unselected package libxcb1:armhf. Preparing to unpack .../44-libxcb1_1.15-1_armhf.deb ... Unpacking libxcb1:armhf (1.15-1) ... Selecting previously unselected package libx11-data. Preparing to unpack .../45-libx11-data_2%3a1.8.7-1_all.deb ... Unpacking libx11-data (2:1.8.7-1) ... Selecting previously unselected package libx11-6:armhf. Preparing to unpack .../46-libx11-6_2%3a1.8.7-1_armhf.deb ... Unpacking libx11-6:armhf (2:1.8.7-1) ... Selecting previously unselected package libxcb-render0:armhf. Preparing to unpack .../47-libxcb-render0_1.15-1_armhf.deb ... Unpacking libxcb-render0:armhf (1.15-1) ... Selecting previously unselected package libxcb-shm0:armhf. Preparing to unpack .../48-libxcb-shm0_1.15-1_armhf.deb ... Unpacking libxcb-shm0:armhf (1.15-1) ... Selecting previously unselected package libxext6:armhf. Preparing to unpack .../49-libxext6_2%3a1.3.4-1+b1_armhf.deb ... Unpacking libxext6:armhf (2:1.3.4-1+b1) ... Selecting previously unselected package libxrender1:armhf. Preparing to unpack .../50-libxrender1_1%3a0.9.10-1.1_armhf.deb ... Unpacking libxrender1:armhf (1:0.9.10-1.1) ... Selecting previously unselected package libcairo2:armhf. Preparing to unpack .../51-libcairo2_1.18.0-1+b1_armhf.deb ... Unpacking libcairo2:armhf (1.18.0-1+b1) ... Selecting previously unselected package libglib2.0-0:armhf. Preparing to unpack .../52-libglib2.0-0_2.78.4-1_armhf.deb ... Unpacking libglib2.0-0:armhf (2.78.4-1) ... Selecting previously unselected package libgraphite2-3:armhf. Preparing to unpack .../53-libgraphite2-3_1.3.14-2_armhf.deb ... Unpacking libgraphite2-3:armhf (1.3.14-2) ... Selecting previously unselected package libharfbuzz0b:armhf. Preparing to unpack .../54-libharfbuzz0b_8.3.0-2_armhf.deb ... Unpacking libharfbuzz0b:armhf (8.3.0-2) ... Selecting previously unselected package x11-common. Preparing to unpack .../55-x11-common_1%3a7.7+23_all.deb ... Unpacking x11-common (1:7.7+23) ... Selecting previously unselected package libice6:armhf. Preparing to unpack .../56-libice6_2%3a1.0.10-1_armhf.deb ... Unpacking libice6:armhf (2:1.0.10-1) ... Selecting previously unselected package libkpathsea6:armhf. Preparing to unpack .../57-libkpathsea6_2023.20230311.66589-9_armhf.deb ... Unpacking libkpathsea6:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libpaper1:armhf. Preparing to unpack .../58-libpaper1_1.1.29_armhf.deb ... Unpacking libpaper1:armhf (1.1.29) ... Selecting previously unselected package libpaper-utils. Preparing to unpack .../59-libpaper-utils_1.1.29_armhf.deb ... Unpacking libpaper-utils (1.1.29) ... Selecting previously unselected package libpotrace0:armhf. Preparing to unpack .../60-libpotrace0_1.16-2+b1_armhf.deb ... Unpacking libpotrace0:armhf (1.16-2+b1) ... Selecting previously unselected package libptexenc1:armhf. Preparing to unpack .../61-libptexenc1_2023.20230311.66589-9_armhf.deb ... Unpacking libptexenc1:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libsm6:armhf. Preparing to unpack .../62-libsm6_2%3a1.2.3-1_armhf.deb ... Unpacking libsm6:armhf (2:1.2.3-1) ... Selecting previously unselected package libsynctex2:armhf. Preparing to unpack .../63-libsynctex2_2023.20230311.66589-9_armhf.deb ... Unpacking libsynctex2:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libteckit0:armhf. Preparing to unpack .../64-libteckit0_2.5.12+ds1-1_armhf.deb ... Unpacking libteckit0:armhf (2.5.12+ds1-1) ... Selecting previously unselected package libtexlua53-5:armhf. Preparing to unpack .../65-libtexlua53-5_2023.20230311.66589-9_armhf.deb ... Unpacking libtexlua53-5:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libxt6:armhf. Preparing to unpack .../66-libxt6_1%3a1.2.1-1.1_armhf.deb ... Unpacking libxt6:armhf (1:1.2.1-1.1) ... Selecting previously unselected package libxmu6:armhf. Preparing to unpack .../67-libxmu6_2%3a1.1.3-3_armhf.deb ... Unpacking libxmu6:armhf (2:1.1.3-3) ... Selecting previously unselected package libxpm4:armhf. Preparing to unpack .../68-libxpm4_1%3a3.5.17-1_armhf.deb ... Unpacking libxpm4:armhf (1:3.5.17-1) ... Selecting previously unselected package libxaw7:armhf. Preparing to unpack .../69-libxaw7_2%3a1.0.14-1_armhf.deb ... Unpacking libxaw7:armhf (2:1.0.14-1) ... Selecting previously unselected package libxi6:armhf. Preparing to unpack .../70-libxi6_2%3a1.8.1-1_armhf.deb ... Unpacking libxi6:armhf (2:1.8.1-1) ... Selecting previously unselected package libzzip-0-13:armhf. Preparing to unpack .../71-libzzip-0-13_0.13.72+dfsg.1-1.1+b1_armhf.deb ... Unpacking libzzip-0-13:armhf (0.13.72+dfsg.1-1.1+b1) ... Selecting previously unselected package racket-common. Preparing to unpack .../72-racket-common_8.12+dfsg1-7_all.deb ... Unpacking racket-common (8.12+dfsg1-7) ... Selecting previously unselected package racket. Preparing to unpack .../73-racket_8.12+dfsg1-7_armhf.deb ... Unpacking racket (8.12+dfsg1-7) ... Selecting previously unselected package t1utils. Preparing to unpack .../74-t1utils_1.41-4_armhf.deb ... Unpacking t1utils (1.41-4) ... Selecting previously unselected package tex-common. Preparing to unpack .../75-tex-common_6.18_all.deb ... Unpacking tex-common (6.18) ... Selecting previously unselected package texlive-binaries. Preparing to unpack .../76-texlive-binaries_2023.20230311.66589-9_armhf.deb ... Unpacking texlive-binaries (2023.20230311.66589-9) ... Selecting previously unselected package xdg-utils. Preparing to unpack .../77-xdg-utils_1.1.3-4.1_all.deb ... Unpacking xdg-utils (1.1.3-4.1) ... Selecting previously unselected package texlive-base. Preparing to unpack .../78-texlive-base_2023.20240207-1_all.deb ... Unpacking texlive-base (2023.20240207-1) ... Selecting previously unselected package texlive-fonts-recommended. Preparing to unpack .../79-texlive-fonts-recommended_2023.20240207-1_all.deb ... Unpacking texlive-fonts-recommended (2023.20240207-1) ... Selecting previously unselected package texlive-latex-base. Preparing to unpack .../80-texlive-latex-base_2023.20240207-1_all.deb ... Unpacking texlive-latex-base (2023.20240207-1) ... Selecting previously unselected package texlive-latex-recommended. Preparing to unpack .../81-texlive-latex-recommended_2023.20240207-1_all.deb ... Unpacking texlive-latex-recommended (2023.20240207-1) ... Selecting previously unselected package texlive. Preparing to unpack .../82-texlive_2023.20240207-1_all.deb ... Unpacking texlive (2023.20240207-1) ... Setting up libexpat1:armhf (2.5.0-2+b2) ... Setting up libpipeline1:armhf (1.5.7-1+b2) ... Setting up libgraphite2-3:armhf (1.3.14-2) ... Setting up libpixman-1-0:armhf (0.42.2-1+b1) ... Setting up libxau6:armhf (1:1.0.9-1) ... Setting up libicu72:armhf (72.1-4+b1) ... Setting up bsdextrautils (2.39.3-6) ... Setting up libmagic-mgc (1:5.45-2+b1) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libglib2.0-0:armhf (2.78.4-1) ... No schema files found: doing nothing. Setting up libdebhelper-perl (13.15.3) ... Setting up libbrotli1:armhf (1.1.0-2+b3) ... Setting up x11-common (1:7.7+23) ... invoke-rc.d: could not determine current runlevel Setting up X socket directories... /tmp/.X11-unix /tmp/.ICE-unix. Setting up libmagic1:armhf (1:5.45-2+b1) ... Setting up gettext-base (0.21-14+b1) ... Setting up m4 (1.4.19-4) ... Setting up libzzip-0-13:armhf (0.13.72+dfsg.1-1.1+b1) ... Setting up file (1:5.45-2+b1) ... Setting up autotools-dev (20220109.1) ... Setting up libx11-data (2:1.8.7-1) ... Setting up libteckit0:armhf (2.5.12+ds1-1) ... Setting up t1utils (1.41-4) ... Setting up libtexlua53-5:armhf (2023.20230311.66589-9) ... Setting up fonts-dejavu-mono (2.37-8) ... Setting up libpng16-16:armhf (1.6.43-1) ... Setting up autopoint (0.21-14) ... Setting up fonts-dejavu-core (2.37-8) ... Setting up libkpathsea6:armhf (2023.20230311.66589-9) ... Setting up autoconf (2.71-3) ... Setting up sensible-utils (0.0.22) ... Setting up libuchardet0:armhf (0.0.8-1+b1) ... Setting up fonts-lmodern (2.005-1) ... Setting up libsub-override-perl (0.10-1) ... Setting up libbsd0:armhf (0.12.2-1) ... Setting up racket-common (8.12+dfsg1-7) ... Setting up libelf1:armhf (0.190-1+b1) ... Setting up libxml2:armhf (2.9.14+dfsg-1.3+b2) ... Setting up xdg-utils (1.1.3-4.1) ... update-alternatives: using /usr/bin/xdg-open to provide /usr/bin/open (open) in auto mode Setting up libsynctex2:armhf (2023.20230311.66589-9) ... Setting up libpotrace0:armhf (1.16-2+b1) ... Setting up automake (1:1.16.5-1.3) ... update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode Setting up libfile-stripnondeterminism-perl (1.13.1-1) ... Setting up libice6:armhf (2:1.0.10-1) ... Setting up libxdmcp6:armhf (1:1.1.2-3) ... Setting up libxcb1:armhf (1.15-1) ... Setting up gettext (0.21-14+b1) ... Setting up libtool (2.4.7-7) ... Setting up libxcb-render0:armhf (1.15-1) ... Setting up fontconfig-config (2.15.0-1.1) ... Setting up libxcb-shm0:armhf (1.15-1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libptexenc1:armhf (2023.20230311.66589-9) ... Setting up libfreetype6:armhf (2.13.2+dfsg-1+b1) ... Setting up racket (8.12+dfsg1-7) ... Setting up ucf (3.0043+nmu1) ... Setting up dh-strip-nondeterminism (1.13.1-1) ... Setting up dwz (0.15-1) ... Setting up groff-base (1.23.0-3) ... Setting up libx11-6:armhf (2:1.8.7-1) ... Setting up libharfbuzz0b:armhf (8.3.0-2) ... Setting up libfontconfig1:armhf (2.15.0-1.1) ... Setting up libsm6:armhf (2:1.2.3-1) ... Setting up libpaper1:armhf (1.1.29) ... Creating config file /etc/papersize with new version Setting up libxpm4:armhf (1:3.5.17-1) ... Setting up libxrender1:armhf (1:0.9.10-1.1) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up libxext6:armhf (2:1.3.4-1+b1) ... Setting up libpaper-utils (1.1.29) ... Setting up man-db (2.12.0-3) ... Not building database; man-db/auto-update is not 'true'. Setting up libcairo2:armhf (1.18.0-1+b1) ... Setting up tex-common (6.18) ... update-language: texlive-base not installed and configured, doing nothing! Setting up libxt6:armhf (1:1.2.1-1.1) ... Setting up libxmu6:armhf (2:1.1.3-3) ... Setting up libxi6:armhf (2:1.8.1-1) ... Setting up debhelper (13.15.3) ... Setting up libxaw7:armhf (2:1.0.14-1) ... Setting up texlive-binaries (2023.20230311.66589-9) ... update-alternatives: using /usr/bin/xdvi-xaw to provide /usr/bin/xdvi.bin (xdvi.bin) in auto mode update-alternatives: using /usr/bin/bibtex.original to provide /usr/bin/bibtex (bibtex) in auto mode Setting up texlive-base (2023.20240207-1) ... tl-paper: setting paper size for dvips to a4: /var/lib/texmf/dvips/config/config-paper.ps tl-paper: setting paper size for dvipdfmx to a4: /var/lib/texmf/dvipdfmx/dvipdfmx-paper.cfg tl-paper: setting paper size for xdvi to a4: /var/lib/texmf/xdvi/XDvi-paper tl-paper: setting paper size for pdftex to a4: /var/lib/texmf/tex/generic/tex-ini-files/pdftexconfig.tex Setting up texlive-latex-base (2023.20240207-1) ... Setting up texlive-latex-recommended (2023.20240207-1) ... Setting up texlive-fonts-recommended (2023.20240207-1) ... Setting up texlive (2023.20240207-1) ... Processing triggers for libc-bin (2.37-15) ... Processing triggers for tex-common (6.18) ... Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Building format(s) --all. This may take some time... done. Reading package lists... Building dependency tree... Reading state information... Reading extended state information... Initializing package states... Writing extended state information... Building tag database... -> Finished parsing the build-deps I: Building the package I: user script /srv/workspace/pbuilder/21219/tmp/hooks/A99_set_merged_usr starting Not re-configuring usrmerge for trixie I: user script /srv/workspace/pbuilder/21219/tmp/hooks/A99_set_merged_usr finished hostname: Name or service not known I: Running cd /build/reproducible-path/minlog-4.0.99.20100221/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../minlog_4.0.99.20100221-7_source.changes dpkg-buildpackage: info: source package minlog dpkg-buildpackage: info: source version 4.0.99.20100221-7 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Vagrant Cascadian dpkg-source --before-build . dpkg-buildpackage: info: host architecture armhf debian/rules clean dh clean --no-parallel dh_auto_clean -O--no-parallel make -j1 clean make[1]: Entering directory '/build/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/src' rm -rf .dep .dep.* rm -rf TAGS rm -rf *~ *% rm -rf grammar.log make[2]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/src' (cd doc; make clean) make[2]: Entering directory '/build/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/doc' (cd examples; make clean) make[2]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed (cd classical; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/classical' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/classical' (cd hounif; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/hounif' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/hounif' (cd prop; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/prop' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/prop' (cd quant; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/quant' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/quant' (cd warshall; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/warshall' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/warshall' (cd dijkstra; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/dijkstra' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/dijkstra' (cd bar; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/bar' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/bar' (cd dc; make clean) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/dc' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/dc' (cd arith; make clean) make[3]: Entering directory '/build/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/examples/arith/quotrem' rm -f *~ core *.diff *.out .TEST *.nodigits .*.test-passed make[4]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/arith/quotrem' make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples/arith' make[2]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/examples' make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_autoreconf_clean -O--no-parallel dh_clean -O--no-parallel debian/rules binary dh binary --no-parallel dh_update_autotools_config -O--no-parallel dh_autoreconf -O--no-parallel dh_auto_configure -O--no-parallel dh_auto_build -O--no-parallel make -j1 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[2]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/src' make[2]: Nothing to be done for '.dep.notags'. make[2]: Leaving directory '/build/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/doc' pdflatex mlcf >> /dev/null bibtex -terse mlcf makeindex -q mlcf pdflatex mlcf >> /dev/null pdflatex mlcf >> /dev/null pdflatex mpcref.tex >> /dev/null kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 tcrm1095 mktexpk: Running mf-nowin -progname=mf \mode:=ljfour; mag:=1+0/600; nonstopmode; input tcrm1095 This is METAFONT, Version 2.71828182 (TeX Live 2023/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/reproducible-path/minlog-4.0.99.20100221/debian/.debhelper/generated/_source/home/.texlive2023/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/reproducible-path/minlog-4.0.99.20100221/doc' make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' debian/rules override_dh_auto_test make[1]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_auto_test || echo 'WARNING: Test suite failures' make -j1 test make[2]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/src' make[3]: Nothing to be done for '.dep.notags'. make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/src' (cd examples; make .TEST) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/examples' cat test.scm | petite -- ..//init.scm | sed "1d;2d" > test.out /bin/sh: line 1: petite: command 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/reproducible-path/minlog-4.0.99.20100221/examples --- test.out.nodigits 2024-04-05 01:29:10.047140775 +0000 +++ test.save.nodigits 2024-04-05 01:29:10.067140027 +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/reproducible-path/minlog-4.0.99.20100221/examples' make[2]: *** [Makefile:81: examples/.TEST] Error 2 make[2]: Leaving directory '/build/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/examples \ -name '*.diff' \ -delete find /build/reproducible-path/minlog-4.0.99.20100221/examples \ -name '*.out' \ -delete find /build/reproducible-path/minlog-4.0.99.20100221/examples \ -name '*.nodigits' \ -delete make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' create-stamp debian/debhelper-build-stamp dh_testroot -O--no-parallel dh_prep -O--no-parallel debian/rules override_dh_auto_install make[1]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_auto_install -- DESTDIR=/usr PREFIX=/build/reproducible-path/minlog-4.0.99.20100221/debian/minlog make -j1 install DESTDIR=/build/reproducible-path/minlog-4.0.99.20100221/debian/minlog AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" DESTDIR=/usr PREFIX=/build/reproducible-path/minlog-4.0.99.20100221/debian/minlog make[2]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' (cd src; make .dep.notags) make[3]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221/src' make[3]: Nothing to be done for '.dep.notags'. make[3]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221/src' install --strip-program=true -p -d -m 755 /build/reproducible-path/minlog-4.0.99.20100221/debian/minlog/usr/share/minlog /build/reproducible-path/minlog-4.0.99.20100221/debian/minlog/usr/bin /build/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221/debian/minlog/usr/bin/minlog chmod a+x /build/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/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/reproducible-path/minlog-4.0.99.20100221' make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_installdocs -O--no-parallel dh_installchangelogs -O--no-parallel debian/rules override_dh_installman make[1]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_installman debian/minlog.1 make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_installsystemduser -O--no-parallel dh_perl -O--no-parallel dh_link -O--no-parallel dh_strip_nondeterminism -O--no-parallel debian/rules override_dh_compress make[1]: Entering directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_compress --exclude=minlog/examples --exclude=.pdf make[1]: Leaving directory '/build/reproducible-path/minlog-4.0.99.20100221' dh_fixperms -O--no-parallel dh_missing -O--no-parallel dh_installdeb -O--no-parallel dh_gencontrol -O--no-parallel dh_md5sums -O--no-parallel dh_builddeb -O--no-parallel dpkg-deb: building package 'minlog' in '../minlog_4.0.99.20100221-7_all.deb'. dpkg-genbuildinfo --build=binary -O../minlog_4.0.99.20100221-7_armhf.buildinfo dpkg-genchanges --build=binary -O../minlog_4.0.99.20100221-7_armhf.changes dpkg-genchanges: info: binary-only upload (no source code included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: not including original source code in upload I: copying local configuration I: user script /srv/workspace/pbuilder/21219/tmp/hooks/B01_cleanup starting I: user script /srv/workspace/pbuilder/21219/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env I: removing directory /srv/workspace/pbuilder/21219 and its subdirectories I: Current time: Fri Apr 5 15:29:36 +14 2024 I: pbuilder-time-stamp: 1712280576