Diff of the two buildlogs: -- --- b1/build.log 2024-01-07 20:28:58.661456353 +0000 +++ b2/build.log 2024-01-07 20:57:14.375806580 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Jan 7 07:40:00 -12 2024 -I: pbuilder-time-stamp: 1704656400 +I: Current time: Mon Jan 8 10:29:33 +14 2024 +I: pbuilder-time-stamp: 1704659373 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -28,49 +28,81 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3277/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/21898/tmp/hooks/D01_modify_environment starting +debug: Running on virt32b. +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 Jan 7 20:29 /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/21898/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/21898/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='armhf' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 ' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='armhf' + 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]="15" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.15(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=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='80272241316145838f670eaaca6ab1a1' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='3277' - PS1='# ' - PS2='> ' + INVOCATION_ID=1acfb70af34148cf83ead5e44b77f87f + 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=21898 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.hllxnchh/pbuilderrc_aENG --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.hllxnchh/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='113' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://10.0.0.15:3142/' + 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.hllxnchh/pbuilderrc_NuRn --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.hllxnchh/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=112 + SUDO_UID=106 + 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 virt64b 6.1.0-17-arm64 #1 SMP Debian 6.1.69-1 (2023-12-30) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-17-armmp-lpae #1 SMP Debian 6.1.69-1 (2023-12-30) armv7l GNU/Linux I: ls -l /bin total 4964 -rwxr-xr-x 1 root root 838488 Apr 23 2023 bash @@ -130,7 +162,7 @@ -rwxr-xr-x 1 root root 67600 Sep 20 2022 rmdir -rwxr-xr-x 1 root root 14152 Jul 28 23:46 run-parts -rwxr-xr-x 1 root root 133372 Jan 5 2023 sed - lrwxrwxrwx 1 root root 4 Jan 5 2023 sh -> dash + lrwxrwxrwx 1 root root 9 Jan 7 20:29 sh -> /bin/bash -rwxr-xr-x 1 root root 67584 Sep 20 2022 sleep -rwxr-xr-x 1 root root 67644 Sep 20 2022 stty -rwsr-xr-x 1 root root 50800 Mar 23 2023 su @@ -156,7 +188,7 @@ -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew -I: user script /srv/workspace/pbuilder/3277/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/21898/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -378,7 +410,7 @@ Get: 180 http://deb.debian.org/debian bookworm/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 181 http://deb.debian.org/debian bookworm/main armhf texlive-base all 2022.20230122-3 [21.9 MB] Get: 182 http://deb.debian.org/debian bookworm/main armhf texlive-latex-base all 2022.20230122-3 [1182 kB] -Fetched 170 MB in 16s (10.8 MB/s) +Fetched 170 MB in 16s (10.6 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libargon2-1:armhf. (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 ... 17881 files and directories currently installed.) @@ -989,8 +1021,8 @@ Setting up tzdata (2023c-5+deb12u1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Jan 7 19:43:50 UTC 2024. -Universal Time is now: Sun Jan 7 19:43:50 UTC 2024. +Local time is now: Sun Jan 7 20:31:43 UTC 2024. +Universal Time is now: Sun Jan 7 20:31:43 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libdconf1:armhf (0.40.0-4) ... @@ -1176,7 +1208,11 @@ fakeroot is already the newest version (1.31-1.2). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/21898/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bookworm +I: user script /srv/workspace/pbuilder/21898/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && 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 > ../hol88_2.02.19940316dfsg-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1430,9 +1466,24 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1440,16 +1491,22 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ @@ -1457,34 +1514,25 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1492,36 +1540,24 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' find -name X.tex -exec rm -rf {} \; dh_clean -X./ml/site.ml.orig -X./contrib/tooltool/Makefile.orig \ -X./contrib/tooltool/events.c.orig -X./contrib/tooltool/func_fix.c.orig \ @@ -1569,7 +1605,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 07:50:43 -12 2024 +Mon Jan 8 10:36:05 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2807,7 +2843,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 # mem = - : (* -> * list -> bool) @@ -2945,7 +2981,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #.............start address -T 0x7a8e48 () : void @@ -3104,7 +3140,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #.............start address -T 0x7a8e48 () : void @@ -3296,7 +3332,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 # concat = - : (string -> string -> string) @@ -3406,7 +3442,7 @@ start address -T 0x7f53c0 ;; Finished loading "lisp/f-ol-net" start address -T 0x6fd6b0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 7/1/24 + version 2.02 (GCL) created 8/1/24 #...start address -T 0x6f2da8 () : void @@ -3735,7 +3771,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 ###########################() : void @@ -3748,7 +3784,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 ################################################################################################() : void @@ -3893,7 +3929,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 ############################() : void @@ -3936,7 +3972,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 ############################Theory ind loaded () : void @@ -3973,7 +4009,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4014,7 +4050,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4416,7 +4452,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4484,7 +4520,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4689,7 +4725,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4813,7 +4849,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4899,7 +4935,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -4992,7 +5028,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5061,7 +5097,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5166,7 +5202,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5401,7 +5437,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5427,7 +5463,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5555,7 +5591,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5603,7 +5639,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5670,7 +5706,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5729,7 +5765,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5785,7 +5821,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre3 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5798,7 +5834,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 8/1/24 #() : void @@ -5850,7 +5886,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ##########################() : void @@ -5881,7 +5917,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ##############################() : void @@ -5968,7 +6004,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #######################################################################() : void @@ -6121,7 +6157,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ###########################() : void @@ -6156,7 +6192,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #############################() : void @@ -6217,7 +6253,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ###########################Theory arithmetic loaded () : void @@ -6712,7 +6748,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ##################################() : void @@ -6859,7 +6895,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #################################Theory list loaded () : void @@ -7198,7 +7234,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ###############################Theory list loaded () : void @@ -8695,7 +8731,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #############################() : void @@ -9079,7 +9115,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ############################() : void @@ -9377,7 +9413,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ############################() : void @@ -9517,7 +9553,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ############################################() : void @@ -9614,7 +9650,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 ##################################() : void @@ -9644,7 +9680,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -9661,7 +9697,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #Theory num loaded () : void @@ -9680,7 +9716,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -9837,7 +9873,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 # @@ -9875,7 +9911,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 # @@ -9909,7 +9945,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -9994,7 +10030,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -10035,7 +10071,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -10219,7 +10255,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 # define_load_lib_function = - : (string list -> void -> void) @@ -10295,7 +10331,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre3 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10308,7 +10344,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #() : void @@ -10372,11 +10408,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 07:59:38 -12 2024 +Mon Jan 8 10:41:38 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 07:59:39 -12 2024 +Mon Jan 8 10:41:38 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10399,7 +10435,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -10483,7 +10519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -10589,7 +10625,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11339,7 +11375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11362,7 +11398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11405,7 +11441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11441,7 +11477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11493,7 +11529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11525,7 +11561,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11563,7 +11599,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11591,7 +11627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11668,7 +11704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11690,7 +11726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11744,7 +11780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11793,7 +11829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11944,7 +11980,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -11988,7 +12024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12063,7 +12099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12113,7 +12149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12176,7 +12212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12229,7 +12265,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12275,7 +12311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12363,7 +12399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12401,7 +12437,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12462,7 +12498,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12526,7 +12562,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12552,7 +12588,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12577,7 +12613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12616,7 +12652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -12692,7 +12728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13429,7 +13465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13452,7 +13488,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13495,7 +13531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13530,7 +13566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13571,7 +13607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13634,7 +13670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13657,7 +13693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13682,7 +13718,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13709,7 +13745,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -13745,7 +13781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14277,7 +14313,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14300,7 +14336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14334,7 +14370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14389,7 +14425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14480,7 +14516,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14649,7 +14685,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -14803,7 +14839,7 @@ WOSET_TRANS_LESS = |- !l. woset l ==> (!x y z. less l(x,y) /\ l(y,z) ==> less l(x,z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 144 WOSET = @@ -14902,7 +14938,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (?f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 444 WO_RECURSE = @@ -14968,11 +15004,11 @@ Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -15001,7 +15037,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1172 EXTEND_FL = @@ -15040,11 +15076,11 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = @@ -15065,7 +15101,7 @@ WO_FL_RESTRICT = |- !l. woset l ==> (!P. fl(\(x,y). P x /\ P y /\ l(x,y))x = P x /\ fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -15076,14 +15112,14 @@ |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2506 ZL = |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -15102,7 +15138,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1083 () : void @@ -15112,7 +15148,7 @@ File mk_wellorder loaded () : void -Run time: 1.0s +Run time: 0.9s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15121,7 +15157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -15252,7 +15288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -15301,12 +15337,12 @@ Intermediate theorems generated: 2 GROUP_EXTENDS_MONOID = ... |- IS_MONOID(monoid(fn g)(id g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 144 IDENTITY_UNIQUE = ... |- !f. (!a. (fn g a f = a) /\ (fn g f a = a)) ==> (f = id g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 144 ":(*)group" : type @@ -15344,7 +15380,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -15436,12 +15472,12 @@ Run time: 0.2s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sun Jan 7 08:02:41 -12 2024 +===> abs_theory rebuilt on Mon Jan 8 10:44:00 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -15614,7 +15650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -15764,13 +15800,13 @@ trat_sucint = |- (trat_sucint 0 = trat_1) /\ (!n. trat_sucint(SUC n) = (trat_sucint n) trat_add trat_1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 trat_eq = |- !x y x' y'. (x,y) trat_eq (x',y') = ((SUC x) * (SUC y') = (SUC x') * (SUC y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 TRAT_EQ_REFL = |- !p. p trat_eq p @@ -15950,13 +15986,13 @@ Run time: 0.0s TRAT_ARCH = |- !h. ?n d. (trat_sucint n) trat_eq (h trat_add d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 TRAT_SUCINT = |- (trat_sucint 0) trat_eq trat_1 /\ (!n. (trat_sucint(SUC n)) trat_eq ((trat_sucint n) trat_add trat_1)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 37 TRAT_EQ_EQUIV = |- !p q. p trat_eq q = ($trat_eq p = $trat_eq q) @@ -16041,7 +16077,7 @@ File hrat.ml loaded () : void -Run time: 0.5s +Run time: 0.4s Intermediate theorems generated: 11032 #\ @@ -16051,7 +16087,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -16242,7 +16278,7 @@ HRAT_LT_RADD = |- !x y z. (x hrat_add z) hrat_lt (y hrat_add z) = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 21 HRAT_LT_MUL2 = @@ -16328,7 +16364,7 @@ Intermediate theorems generated: 221 hreal_tydef = |- ?rep. TYPE_DEFINITION isacut rep -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 4 hreal_tybij = @@ -16361,7 +16397,7 @@ Intermediate theorems generated: 37 CUT_DOWN = |- !X x y. cut X x /\ y hrat_lt x ==> cut X y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 49 CUT_UP = |- !X x. cut X x ==> (?y. cut X y /\ x hrat_lt y) @@ -16404,7 +16440,7 @@ CUT_NEARTOP_MUL = |- !X u. hrat_1 hrat_lt u ==> (?x. cut X x /\ ~cut X(u hrat_mul x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 234 hreal_1 = |- hreal_1 = hreal(cut_of_hrat hrat_1) @@ -16447,7 +16483,7 @@ isacut (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 502 HREAL_ADD_ISACUT = @@ -16457,7 +16493,7 @@ HREAL_MUL_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X @@ -16482,7 +16518,7 @@ |- !X Y Z. X hreal_mul (Y hreal_add Z) = (X hreal_mul Y) hreal_add (X hreal_mul Z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 HREAL_MUL_LID = |- !X. hreal_1 hreal_mul X = X @@ -16551,7 +16587,7 @@ File hreal.ml loaded () : void -Run time: 0.6s +Run time: 0.5s Intermediate theorems generated: 10456 #\ @@ -16561,7 +16597,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -16721,11 +16757,11 @@ Intermediate theorems generated: 23 HREAL_LT_ADDR = |- !x y. ~(x hreal_add y) hreal_lt x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 HREAL_LT_GT = |- !x y. x hreal_lt y ==> ~y hreal_lt x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 66 Theorem HREAL_ADD_SYM autoloading from theory `HREAL` ... @@ -16888,7 +16924,7 @@ TREAL_MUL_LINV = |- !x. ~x treal_eq treal_0 ==> ((treal_inv x) treal_mul x) treal_eq treal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x @@ -16896,7 +16932,7 @@ Intermediate theorems generated: 48 TREAL_LT_REFL = |- !x. ~x treal_lt x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 TREAL_LT_TRANS = @@ -17109,7 +17145,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -17309,7 +17345,7 @@ Intermediate theorems generated: 14 REAL_ADD_RINV = |- !x. x + (-- x) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 14 REAL_MUL_RID = |- !x. x * (& 1) = x @@ -17337,7 +17373,7 @@ Intermediate theorems generated: 21 REAL_ADD_RID_UNIQ = |- !x y. (x + y = x) = (y = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_LNEG_UNIQ = |- !x y. (x + y = & 0) = (x = -- y) @@ -17413,7 +17449,7 @@ Intermediate theorems generated: 28 REAL_LTE_TOTAL = |- !x y. x < y \/ y <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 27 REAL_LE_REFL = |- !x. x <= x @@ -17425,7 +17461,7 @@ Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 125 REAL_LT_IMP_LE = |- !x y. x < y ==> x <= y @@ -17493,7 +17529,7 @@ Intermediate theorems generated: 6 REAL_LT_01 = |- (& 0) < (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 REAL_LE_LADD = |- !x y z. (x + y) <= (x + z) = y <= z @@ -17569,11 +17605,11 @@ Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 32 REAL_SUB_LT = |- !x y. (& 0) < (x - y) = y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 REAL_SUB_LE = |- !x y. (& 0) <= (x - y) = y <= x @@ -17629,7 +17665,7 @@ Intermediate theorems generated: 87 REAL_LT_RMUL_0 = |- !x y. (& 0) < y ==> ((& 0) < (x * y) = (& 0) < x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) @@ -17641,7 +17677,7 @@ Intermediate theorems generated: 22 REAL_LT_RMUL_IMP = |- !x y z. x < y /\ (& 0) < z ==> (x * z) < (y * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 REAL_LT_LMUL_IMP = |- !x y z. y < z /\ (& 0) < x ==> (x * y) < (x * z) @@ -17694,7 +17730,7 @@ Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... LESS_EQ_MONO = |- !n m. (SUC n) num_le (SUC m) = n num_le m @@ -17705,7 +17741,7 @@ Run time: 0.0s REAL_LE = |- !m n. (& m) <= (& n) = m num_le n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -17770,7 +17806,7 @@ Intermediate theorems generated: 90 REAL_NZ_IMP_LT = |- !n. ~(n = 0) ==> (& 0) < (& n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 REAL_LT_RDIV_0 = |- !y z. (& 0) < z ==> ((& 0) < (y / z) = (& 0) < y) @@ -17778,7 +17814,7 @@ Intermediate theorems generated: 40 REAL_LT_RDIV = |- !x y z. (& 0) < z ==> ((x / z) < (y / z) = x < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 44 REAL_LT_FRACTION_0 = @@ -17835,7 +17871,7 @@ Intermediate theorems generated: 51 REAL_DOWN = |- !x. (& 0) < x ==> (?y. (& 0) < y /\ y < x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 REAL_DOWN2 = @@ -17844,7 +17880,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -17884,7 +17920,7 @@ Intermediate theorems generated: 20 REAL_SUB_RZERO = |- !x. x - (& 0) = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 REAL_LET_ADD2 = |- !w x y z. w <= x /\ y < z ==> (w + y) < (x + z) @@ -17892,7 +17928,7 @@ Intermediate theorems generated: 58 REAL_LTE_ADD2 = |- !w x y z. w < x /\ y <= z ==> (w + y) < (x + z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 REAL_LET_ADD = |- !x y. (& 0) <= x /\ (& 0) < y ==> (& 0) < (x + y) @@ -17935,7 +17971,7 @@ Intermediate theorems generated: 24 REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 REAL_INV_MUL = @@ -17966,7 +18002,7 @@ Intermediate theorems generated: 36 REAL_MEAN = |- !x y. x < y ==> (?z. x < z /\ z < y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) @@ -17977,7 +18013,7 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> (x1 * y1) <= (x2 * y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 345 REAL_LE_LDIV = |- !x y z. (& 0) < x /\ y <= (z * x) ==> (y / x) <= z @@ -18007,7 +18043,7 @@ Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) @@ -18138,11 +18174,11 @@ Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -18176,7 +18212,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -18196,11 +18232,11 @@ Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 83 POW_PLUS1 = @@ -18233,11 +18269,11 @@ Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -18257,7 +18293,7 @@ Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) @@ -18265,7 +18301,7 @@ Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -18292,7 +18328,7 @@ |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -18303,7 +18339,7 @@ Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 SUP_LEMMA3 = @@ -18319,7 +18355,7 @@ Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 REAL_SUP = @@ -18346,7 +18382,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 15 REAL_SUP_UBOUND_LE = @@ -18356,7 +18392,7 @@ Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 342 Theorem PRE autoloading from theory `prim_rec` ... @@ -18381,7 +18417,7 @@ Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Sum = @@ -18394,7 +18430,7 @@ Intermediate theorems generated: 109 SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) @@ -18420,7 +18456,7 @@ |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r = g r)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 82 SUM_POS = |- !f. (!n. (& 0) <= (f n)) ==> (!m n. (& 0) <= (Sum(m,n)f)) @@ -18435,7 +18471,7 @@ SUM_ABS = |- !f m n. abs(Sum(m,n)(\m. abs(f m))) = Sum(m,n)(\m. abs(f m)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) @@ -18463,7 +18499,7 @@ SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) @@ -18501,7 +18537,7 @@ SUM_NSUB = |- !n f c. (Sum(0,n)f) - ((& n) * c) = Sum(0,n)(\p. (f p) - c) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 239 Theorem LESS_SUC autoloading from theory `prim_rec` ... @@ -18512,7 +18548,7 @@ |- !f K m n. (!p. m num_le p /\ p num_lt (m num_add n) ==> (f p) <= K) ==> (Sum(m,n)f) <= ((& n) * K) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 226 SUM_GROUP = @@ -18604,7 +18640,7 @@ File real.ml loaded () : void -Run time: 2.9s +Run time: 2.8s Intermediate theorems generated: 23746 #\ @@ -18614,7 +18650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -18698,7 +18734,7 @@ Intermediate theorems generated: 11 () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -18736,7 +18772,7 @@ Intermediate theorems generated: 16 COMPL_MEM = |- !S x. S x = ~re_compl S x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 23 SUBSET_ANTISYM = |- !P Q. P re_subset Q /\ Q re_subset P = (P = Q) @@ -18855,7 +18891,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 560 metric_tybij = @@ -18943,7 +18979,7 @@ Intermediate theorems generated: 38 ball = |- !m x e. B m(x,e) = (\y. (dist m(x,y)) < e) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -19048,7 +19084,7 @@ Intermediate theorems generated: 34 MR1_SUB_LE = |- !x d. (& 0) <= d ==> (dist mr1(x,x - d) = d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -19108,7 +19144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -19213,7 +19249,7 @@ Intermediate theorems generated: 30 () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -19230,7 +19266,7 @@ |- !s l top g. (s tends l)(top,g) = (!N. neigh top(N,l) ==> (?n. g n n /\ (!m. g m n ==> N(s m)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 bounded = @@ -19352,7 +19388,7 @@ (x --> x0)(mtop d,g) = (!e. (& 0) < e ==> (?n. g n n /\ (!m. g m n ==> (dist d(x m,x0)) < e))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 373 Theorem METRIC_TRIANGLE autoloading from theory `TOPOLOGY` ... @@ -19370,7 +19406,7 @@ Theorem REAL_LT_ADD2 autoloading from theory `REAL` ... REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) -Run time: 0.0s +Run time: 0.1s Theorem METRIC_NZ autoloading from theory `TOPOLOGY` ... METRIC_NZ = |- !m x y. ~(x = y) ==> (& 0) < (dist m(x,y)) @@ -19482,7 +19518,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19497,7 +19533,7 @@ Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT autoloading from theory `REAL` ... REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -19657,7 +19693,7 @@ |- !g k x. (x --> (& 0))(mtop mr1,g) ==> ((\n. k * (x n)) --> (& 0))(mtop mr1,g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 506 Theorem REAL_ADD_ASSOC autoloading from theory `REAL` ... @@ -19733,7 +19769,7 @@ (!x y x0 y0. (x --> x0)(mtop mr1,g) /\ (y --> y0)(mtop mr1,g) ==> ((\n. (x n) * (y n)) --> (x0 * y0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 338 Theorem REAL_INV_NZ autoloading from theory `REAL` ... @@ -19776,7 +19812,7 @@ (!x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) --> (inv x0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1253 NET_DIV = @@ -19823,7 +19859,7 @@ (y --> y0)(mtop mr1,g) /\ (?N. g N N /\ (!n. g n N ==> (x n) <= (y n))) ==> x0 <= y0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 400 () : void @@ -19833,7 +19869,7 @@ File nets.ml loaded () : void -Run time: 0.6s +Run time: 0.5s Intermediate theorems generated: 7389 #\ @@ -19843,7 +19879,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -19917,7 +19953,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s real_interface_map = [(`--`, `real_neg`); @@ -20140,7 +20176,7 @@ Intermediate theorems generated: 36 subseq = |- !f. subseq f = (!m n. m num_lt n ==> (f m) num_lt (f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... @@ -20256,7 +20292,7 @@ Run time: 0.0s SEQ_BOUNDED = |- !s. bounded(mr1,$num_ge)s = (?k. !n. (abs(s n)) < k) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 273 Theorem REAL_LE_NEG autoloading from theory `REAL` ... @@ -20310,7 +20346,7 @@ Intermediate theorems generated: 1 SEQ_CBOUNDED = |- !f. cauchy f ==> bounded(mr1,$num_ge)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 110 Theorem REAL_LE_RADD autoloading from theory `REAL` ... @@ -20378,7 +20414,7 @@ Intermediate theorems generated: 39 SEQ_BCONV = |- !f. bounded(mr1,$num_ge)f /\ mono f ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... @@ -20416,7 +20452,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20466,7 +20502,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20550,7 +20586,7 @@ SEQ_INV0 = |- !f. (!y. ?N. !n. n num_ge N ==> (f n) > y) ==> (\n. inv(f n)) --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 423 Theorem POW_0 autoloading from theory `REAL` ... @@ -20648,7 +20684,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20683,7 +20719,7 @@ Theorem ABS_N autoloading from theory `REAL` ... ABS_N = |- !n. abs(& n) = & n -Run time: 0.1s +Run time: 0.0s Theorem REAL_MUL_RZERO autoloading from theory `REAL` ... REAL_MUL_RZERO = |- !x. x * (& 0) = & 0 @@ -20833,7 +20869,7 @@ SUM_POS_GEN = |- !f m. (!n. m num_le n ==> (& 0) <= (f n)) ==> (!n. (& 0) <= (Sum(m,n)f)) -Run time: 0.1s +Run time: 0.0s SER_POS_LE = |- !f n. @@ -20851,7 +20887,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) < (f m)) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 209 Theorem LESS_REFL autoloading from theory `prim_rec` ... @@ -20923,7 +20959,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -20971,7 +21007,7 @@ |- !f. summable f = (!e. (& 0) < e ==> (?N. !m n. m num_ge N ==> (abs(Sum(m,n)f)) < e)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) @@ -21060,7 +21096,7 @@ |- !x. ~(x = & 1) ==> (!n. Sum(0,n)(\n'. x pow n') = ((x pow n) - (& 1)) / (x - (& 1))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 411 Theorem REAL_NEG_INV autoloading from theory `REAL` ... @@ -21127,7 +21163,7 @@ File seq.ml loaded () : void -Run time: 1.3s +Run time: 1.1s Intermediate theorems generated: 18704 #\ @@ -21137,7 +21173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -21211,7 +21247,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -21434,7 +21470,7 @@ |- !g x x0. (x tends x0)(mtop mr1,g) = ((\n. (x n) - x0) tends (& 0))(mtop mr1,g) -Run time: 0.0s +Run time: 0.1s LIM_NULL = |- !f l x. (f --> l)x = ((\x. (f x) - l) --> (& 0))x Run time: 0.0s @@ -21453,7 +21489,7 @@ Run time: 0.0s LIM_UNIQ = |- !f l m x. (f --> l)x /\ (f --> m)x ==> (l = m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 36 LIM_EQUAL = @@ -21563,7 +21599,7 @@ Intermediate theorems generated: 29 CONT_NEG = |- !x. f contl x ==> (\x. --(f x)) contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 CONT_INV = |- !x. f contl x /\ ~(f x = & 0) ==> (\x. inv(f x)) contl x @@ -21595,7 +21631,7 @@ Theorem REAL_ADD_SYM autoloading from theory `REAL` ... REAL_ADD_SYM = |- !x y. x + y = y + x -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE_RADD autoloading from theory `REAL` ... REAL_LE_RADD = |- !x y z. (x + z) <= (y + z) = x <= y @@ -21667,7 +21703,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21701,7 +21737,7 @@ Run time: 0.0s DIFF_CONST = |- !k x. ((\x. k) diffl (& 0))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 59 Theorem REAL_RDISTRIB autoloading from theory `REAL` ... @@ -21813,7 +21849,7 @@ (?k d. (& 0) < d /\ (!x. (& 0) < (abs(x - x0)) /\ (abs(x - x0)) < d ==> (abs(f x)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 362 Theorem REAL_MUL_LID autoloading from theory `REAL` ... @@ -21829,7 +21865,7 @@ ((f(g(x + h))) - (f(g x))) / h = (((f(g(x + h))) - (f(g x))) / ((g(x + h)) - (g x))) * (((g(x + h)) - (g x)) / h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 170 Theorem REAL_LT_RADD autoloading from theory `REAL` ... @@ -21867,7 +21903,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21875,7 +21911,7 @@ Run time: 0.0s DIFF_X = |- !x. ((\x. x) diffl (& 1))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 Theorem REAL_MUL_RID autoloading from theory `REAL` ... @@ -21950,7 +21986,7 @@ DIFF_XM1 = |- !x. ~(x = & 0) ==> ((\x. inv x) diffl (--((inv x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 818 Theorem POW_INV autoloading from theory `REAL` ... @@ -21983,7 +22019,7 @@ ((\x. (f x) / (g x)) diffl (((l * (g x)) - (m * (f x))) / ((g x) pow 2))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 293 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -22024,7 +22060,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22044,7 +22080,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -22081,7 +22117,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22128,7 +22164,7 @@ |- !f x l. (f diffl l)x /\ l < (& 0) ==> (?d. (& 0) < d /\ (!h. (& 0) < h /\ h < d ==> (f x) < (f(x - h)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 469 Theorem REAL_ADD_SUB2 autoloading from theory `REAL` ... @@ -22221,7 +22257,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22230,7 +22266,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -22253,7 +22289,7 @@ File lim.ml loaded () : void -Run time: 1.2s +Run time: 1.1s Intermediate theorems generated: 21608 #\ @@ -22263,7 +22299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -22433,7 +22469,7 @@ |- !n x y. Sum(0,SUC n)(\p. (x pow p) * (y pow ((SUC n) num_sub p))) = y * (Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 223 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -22741,7 +22777,7 @@ summable(\n. (diffs c n) * (x pow n)) ==> (\n. (& n) * ((c n) * (x pow (n num_sub 1)))) sums (suminf(\n. (diffs c n) * (x pow n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 180 Theorem SUB_ADD autoloading from theory `arithmetic` ... @@ -22906,7 +22942,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22981,7 +23017,7 @@ (& 0) < k /\ (!h. (& 0) < (abs h) /\ (abs h) < k ==> (abs(f h)) <= (K * (abs h))) ==> (f tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 917 Theorem SER_LE autoloading from theory `SEQ` ... @@ -23115,7 +23151,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2494 () : void @@ -23125,7 +23161,7 @@ File powser.ml loaded () : void -Run time: 0.7s +Run time: 0.5s Intermediate theorems generated: 8507 #\ @@ -23135,7 +23171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -23299,11 +23335,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23541,7 +23577,7 @@ c < (& 1) /\ (!n. n num_ge N ==> (abs(f(SUC n))) <= (c * (abs(f n)))) ==> summable f -Run time: 0.1s +Run time: 0.0s Theorem SUMMABLE_SUM autoloading from theory `SEQ` ... SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) @@ -23700,7 +23736,7 @@ Theorem SUM_UNIQ autoloading from theory `SEQ` ... SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) -Run time: 0.1s +Run time: 0.0s SIN_NEGLEMMA = |- !x. @@ -23835,7 +23871,7 @@ Run time: 0.0s EXP_LE_X = |- !x. (& 0) <= x ==> ((& 1) + x) <= (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 420 EXP_LT_1 = |- !x. (& 0) < x ==> (& 1) < (exp x) @@ -23860,7 +23896,7 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 @@ -24113,7 +24149,7 @@ Run time: 0.0s ROOT_1 = |- !n. root(SUC n)(& 1) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 ROOT_POW_POS = |- !n x. (& 0) <= x ==> ((root(SUC n)x) pow (SUC n) = x) @@ -24141,7 +24177,7 @@ Run time: 0.0s SIN_0 = |- sin(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -24195,7 +24231,7 @@ Run time: 0.0s SIN_BOUND = |- !x. (abs(sin x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem ABS_BOUNDS autoloading from theory `REAL` ... @@ -24292,7 +24328,7 @@ Intermediate theorems generated: 29 COS_DOUBLE = |- !x. cos((& 2) * x) = ((cos x) pow 2) - ((sin x) pow 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 Theorem ODD_DOUBLE autoloading from theory `arithmetic` ... @@ -24364,7 +24400,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24476,7 +24512,7 @@ Run time: 0.0s PI_POS = |- (& 0) < pi -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 31 Theorem REAL_LT_GT autoloading from theory `REAL` ... @@ -24540,7 +24576,7 @@ Intermediate theorems generated: 53 COS_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 450 Theorem REAL_LT_NEG autoloading from theory `REAL` ... @@ -24549,7 +24585,7 @@ COS_POS_PI = |- !x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 143 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -24637,7 +24673,7 @@ |- !x. (& 0) <= x /\ (cos x = & 0) ==> (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 675 Theorem REAL_LE_ADDR autoloading from theory `REAL` ... @@ -24680,7 +24716,7 @@ (sin x = & 0) = (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 319 tan = |- !x. tan x = (sin x) / (cos x) @@ -24709,7 +24745,7 @@ Theorem REAL_LDISTRIB autoloading from theory `REAL` ... REAL_LDISTRIB = |- !x y z. x * (y + z) = (x * y) + (x * z) -Run time: 0.0s +Run time: 0.1s Theorem REAL_SUB_LDISTRIB autoloading from theory `REAL` ... REAL_SUB_LDISTRIB = |- !x y z. x * (y - z) = (x * y) - (x * z) @@ -24743,7 +24779,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24789,7 +24825,7 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1046 TAN_TOTAL_POS = @@ -24808,7 +24844,7 @@ Theorem REAL_LE_NEGL autoloading from theory `REAL` ... REAL_LE_NEGL = |- !x. (-- x) <= x = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Theorem REAL_LE_NEGTOTAL autoloading from theory `REAL` ... REAL_LE_NEGTOTAL = |- !x. (& 0) <= x \/ (& 0) <= (-- x) @@ -24843,7 +24879,7 @@ (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) /\ (sin(asn y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 ASN_SIN = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (sin(asn y) = y) @@ -24866,7 +24902,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi /\ (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) @@ -24905,13 +24941,13 @@ Intermediate theorems generated: 103 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File transc.ml loaded () : void -Run time: 1.9s +Run time: 1.7s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24924,7 +24960,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -24946,7 +24982,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25012,7 +25048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25044,7 +25080,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25153,7 +25189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25306,7 +25342,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25379,7 +25415,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25459,7 +25495,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25616,7 +25652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25771,7 +25807,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -25988,7 +26024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26010,7 +26046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26029,7 +26065,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26074,7 +26110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26139,7 +26175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26189,7 +26225,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26259,7 +26295,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26329,7 +26365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26365,7 +26401,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26418,7 +26454,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26490,7 +26526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26569,7 +26605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26764,7 +26800,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -26801,7 +26837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -27487,7 +27523,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -27959,7 +27995,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -28223,7 +28259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -28468,7 +28504,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -28932,7 +28968,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29400,7 +29436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29456,7 +29492,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29546,7 +29582,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29745,7 +29781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29777,7 +29813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -29911,7 +29947,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30214,7 +30250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30246,7 +30282,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30285,7 +30321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30317,7 +30353,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30478,7 +30514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30611,7 +30647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30800,7 +30836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30860,7 +30896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -30985,7 +31021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -31096,7 +31132,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -31121,7 +31157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -31149,7 +31185,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -31262,7 +31298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -31765,7 +31801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32013,7 +32049,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32239,7 +32275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32281,7 +32317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32313,7 +32349,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32536,7 +32572,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -32929,7 +32965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -33042,7 +33078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -33545,7 +33581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -33793,7 +33829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34019,7 +34055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34054,7 +34090,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34093,7 +34129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34130,7 +34166,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34151,7 +34187,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34248,7 +34284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34270,7 +34306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34766,7 +34802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34789,7 +34825,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34867,7 +34903,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34926,7 +34962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34970,7 +35006,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -34988,7 +35024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35015,7 +35051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35059,7 +35095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35172,7 +35208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35219,7 +35255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35258,7 +35294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35332,7 +35368,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35421,7 +35457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35492,7 +35528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35562,7 +35598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35611,7 +35647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35652,7 +35688,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35693,7 +35729,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35717,7 +35753,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35818,7 +35854,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35839,7 +35875,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -35864,7 +35900,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36490,7 +36526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36567,7 +36603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36594,7 +36630,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36711,7 +36747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36806,7 +36842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -36892,7 +36928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37007,7 +37043,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37100,7 +37136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37276,7 +37312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37380,7 +37416,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37675,7 +37711,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37778,7 +37814,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37846,7 +37882,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -37908,7 +37944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -38088,7 +38124,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -38129,7 +38165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -38159,7 +38195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -38185,7 +38221,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -38703,7 +38739,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -39240,7 +39276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -39428,7 +39464,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 8/1/24 =============================================================================== #false : bool @@ -39446,10 +39482,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sun Jan 7 08:16:52 -12 2024 +Mon Jan 8 10:51:58 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 08:16:52 -12 2024 +Mon Jan 8 10:51:58 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39467,22 +39503,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 8/1/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 7/1/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 8/1/24 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 8/1/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41219,7 +41255,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -42985,7 +43021,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44729,7 +44765,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44984,7 +45020,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45221,7 +45257,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45399,7 +45435,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45588,7 +45624,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45707,7 +45743,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45823,7 +45859,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46063,7 +46099,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46404,7 +46440,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46611,7 +46647,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46954,7 +46990,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47146,7 +47182,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47414,7 +47450,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47575,7 +47611,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47720,7 +47756,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47872,7 +47908,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48028,7 +48064,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48206,7 +48242,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48402,7 +48438,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48627,7 +48663,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48889,7 +48925,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.07:0824' -> endpages.ps +' TeX output 2024.01.08:1055' -> endpages.ps @@ -48953,7 +48989,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.07:0824' -> titlepages.ps +' TeX output 2024.01.08:1055' -> titlepages.ps @@ -49074,10 +49110,12 @@ dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_fixperms dh_makeshlibs dh_installdeb @@ -49086,15 +49124,16 @@ dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_armhf.buildinfo @@ -49104,12 +49143,14 @@ 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/21898/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/21898/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/3277 and its subdirectories -I: Current time: Sun Jan 7 08:28:52 -12 2024 -I: pbuilder-time-stamp: 1704659332 +I: removing directory /srv/workspace/pbuilder/21898 and its subdirectories +I: Current time: Mon Jan 8 10:57:05 +14 2024 +I: pbuilder-time-stamp: 1704661025