Diff of the two buildlogs: -- --- b1/build.log 2024-11-07 00:00:57.718794335 +0000 +++ b2/build.log 2024-11-07 00:33:16.937703104 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Nov 6 11:30:23 -12 2024 -I: pbuilder-time-stamp: 1730935823 +I: Current time: Thu Nov 7 14:01:35 +14 2024 +I: pbuilder-time-stamp: 1730937695 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -28,52 +28,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/6008/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/6687/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 Nov 7 00:01 /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/6687/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/6687/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='trixie' - 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]="32" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.32(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='c1a771b87992445da3456e63e9d4d2e8' - 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='6008' - PS1='# ' - PS2='> ' + INVOCATION_ID=fc7df2004ae744dd8e567ea37728582f + 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=6687 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.TJl2Afud/pbuilderrc_lTIi --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.TJl2Afud/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='114' - SUDO_UID='108' - 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.TJl2Afud/pbuilderrc_Yyrl --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.TJl2Afud/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 virt64a 6.1.0-26-arm64 #1 SMP Debian 6.1.112-1 (2024-09-30) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-26-armmp-lpae #1 SMP Debian 6.1.112-1 (2024-09-30) armv7l GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Aug 4 21:30 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/6008/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/6687/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -304,7 +336,7 @@ Get: 189 http://deb.debian.org/debian trixie/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 190 http://deb.debian.org/debian trixie/main armhf texlive-base all 2024.20240829-2 [22.7 MB] Get: 191 http://deb.debian.org/debian trixie/main armhf texlive-latex-base all 2024.20240829-2 [1273 kB] -Fetched 172 MB in 4s (46.3 MB/s) +Fetched 172 MB in 4s (46.5 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libapparmor1: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 ... 19690 files and directories currently installed.) @@ -944,8 +976,8 @@ Setting up tzdata (2024a-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Nov 6 23:31:53 UTC 2024. -Universal Time is now: Wed Nov 6 23:31:53 UTC 2024. +Local time is now: Thu Nov 7 00:03:01 UTC 2024. +Universal Time is now: Thu Nov 7 00:03:01 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.12-1) ... @@ -1144,7 +1176,11 @@ fakeroot is already the newest version (1.36-1). 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/6687/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/6687/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 @@ -1398,6 +1434,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/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/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; \ @@ -1405,59 +1459,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/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/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/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/numeral/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/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/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/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/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]: 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/pred_sets/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/finite_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/finite_sets/Manual' +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/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/abs_theory/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/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/reals/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ @@ -1465,31 +1482,50 @@ 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/reduce/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/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/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/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/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/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]: 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; \ + 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/numeral/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/unwind/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/more_arithmetic/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/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/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' 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 \ @@ -1499,16 +1535,6 @@ -X./contrib/Xhelp/xholhelp.h.orig -X./contrib/Xhelp/hol_thm.orig dh_clean: warning: Compatibility levels before 10 are deprecated (level 9 in use) for i in $(find Library -name "*.sve") ; do mv $i $(echo $i | sed "s,\.sve,,1"); done -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! -libfakeroot internal error: payload not recognized! rm -f debian/hol88.install debian/hol88-library.install debian/hol88-source.install debian/hol88-help.install debian/hol88-library-source.install debian/hol88-library-help.install debian/hol88-contrib-source.install debian/hol88-contrib-help.install debian/hol88-doc.install debian/hol88.links debian/hol88-library.links debian/hol88.sh find -name "*.dvi" -exec rm {} \; rm -f Manual/Tutorial/ack.tex Manual/Reference/ack.tex Manual/Description/ack.tex @@ -1547,7 +1573,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Nov 6 11:38:34 -12 2024 +Thu Nov 7 14:10:11 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2785,7 +2811,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 # mem = - : (* -> * list -> bool) @@ -2923,7 +2949,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #.............start address -T 0x88a938 () : void @@ -3082,7 +3108,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #.............start address -T 0x88a938 () : void @@ -3274,7 +3300,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 # concat = - : (string -> string -> string) @@ -3384,7 +3410,7 @@ start address -T 0x887950 ;; Finished loading "lisp/f-ol-net" start address -T 0x6c49c0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 6/11/24 + version 2.02 (GCL) created 7/11/24 #...start address -T 0x730bb0 () : void @@ -3713,7 +3739,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 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 ###########################() : void @@ -3726,7 +3752,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 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 ################################################################################################() : void @@ -3871,7 +3897,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 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 ############################() : void @@ -3914,7 +3940,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 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 ############################Theory ind loaded () : void @@ -3951,7 +3977,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3992,7 +4018,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4394,7 +4420,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4462,7 +4488,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4667,7 +4693,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4791,7 +4817,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4877,7 +4903,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -4970,7 +4996,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5039,7 +5065,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5144,7 +5170,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5379,7 +5405,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5405,7 +5431,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5533,7 +5559,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5581,7 +5607,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5648,7 +5674,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5707,7 +5733,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5763,7 +5789,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 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5776,7 +5802,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #() : void @@ -5828,7 +5854,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ##########################() : void @@ -5859,7 +5885,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ##############################() : void @@ -5946,7 +5972,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #######################################################################() : void @@ -6099,7 +6125,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ###########################() : void @@ -6134,7 +6160,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #############################() : void @@ -6195,7 +6221,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ###########################Theory arithmetic loaded () : void @@ -6690,7 +6716,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ##################################() : void @@ -6837,7 +6863,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #################################Theory list loaded () : void @@ -7176,7 +7202,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ###############################Theory list loaded () : void @@ -8673,7 +8699,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #############################() : void @@ -9057,7 +9083,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ############################() : void @@ -9355,7 +9381,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ############################() : void @@ -9495,7 +9521,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ############################################() : void @@ -9592,7 +9618,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 ##################################() : void @@ -9622,7 +9648,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -9639,7 +9665,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #Theory num loaded () : void @@ -9658,7 +9684,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -9815,7 +9841,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 # @@ -9853,7 +9879,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 # @@ -9887,7 +9913,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -9972,7 +9998,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -10013,7 +10039,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -10197,7 +10223,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 # define_load_lib_function = - : (string list -> void -> void) @@ -10273,7 +10299,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 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10286,7 +10312,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 6/11/24 +BASIC-HOL version 2.02 (GCL) created 7/11/24 #() : void @@ -10350,11 +10376,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Nov 6 11:44:34 -12 2024 +Thu Nov 7 14:16:14 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Nov 6 11:44:34 -12 2024 +Thu Nov 7 14:16:14 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10377,7 +10403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -10461,7 +10487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -10567,7 +10593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11317,7 +11343,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11340,7 +11366,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11383,7 +11409,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11419,7 +11445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11471,7 +11497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11503,7 +11529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11541,7 +11567,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11569,7 +11595,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11646,7 +11672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11668,7 +11694,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11722,7 +11748,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11771,7 +11797,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11922,7 +11948,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -11966,7 +11992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12041,7 +12067,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12091,7 +12117,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12154,7 +12180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12207,7 +12233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12253,7 +12279,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12341,7 +12367,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12379,7 +12405,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12440,7 +12466,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12504,7 +12530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12530,7 +12556,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12555,7 +12581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12594,7 +12620,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -12670,7 +12696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13407,7 +13433,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13430,7 +13456,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13473,7 +13499,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13508,7 +13534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13549,7 +13575,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13612,7 +13638,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13635,7 +13661,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13660,7 +13686,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13687,7 +13713,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -13723,7 +13749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14255,7 +14281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14278,7 +14304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14312,7 +14338,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14367,7 +14393,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14458,7 +14484,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14627,7 +14653,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -14860,7 +14886,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14890,7 +14916,7 @@ (!f g x. (!y. less l(ms y,ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... @@ -14930,7 +14956,7 @@ |- !h ms. (!f g x. (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) @@ -14950,7 +14976,7 @@ Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -14967,7 +14993,7 @@ INSEG_PROPER_SUBSET = |- !l m. m inseg l /\ ~(l = m) ==> (?x y. l(x,y) /\ ~m(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 213 INSEG_PROPER_SUBSET_FL = @@ -14989,7 +15015,7 @@ EXTEND_INSEG = |- !l a. woset l /\ fl l a ==> (\(x,y). l(x,y) /\ l(y,a)) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 EXTEND_LINSEG = @@ -15002,7 +15028,7 @@ ORDINAL_CHAINED = |- !l m. ordinal l /\ ordinal m ==> m inseg l \/ l inseg m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 997 FL_SUC = @@ -15022,12 +15048,12 @@ Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = |- !l x. ordinal l ==> fl l x ==> fl(Union ordinal)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 ORDINAL_UP = @@ -15080,7 +15106,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1083 () : void @@ -15090,7 +15116,7 @@ File mk_wellorder loaded () : void -Run time: 0.9s +Run time: 1.0s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15099,7 +15125,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -15217,20 +15243,20 @@ Intermediate theorems generated: 4 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File ../../Library/abs_theory/monoid_def.ml loaded () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 614 Making ../../Library/abs_theory/group_def.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -15279,7 +15305,7 @@ Intermediate theorems generated: 2 GROUP_EXTENDS_MONOID = ... |- IS_MONOID(monoid(fn g)(id g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 144 IDENTITY_UNIQUE = @@ -15322,7 +15348,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -15372,7 +15398,7 @@ Run time: 0.0s GROUP_THOBS = |- IS_GROUP(group(\x y. ~(x = y))F I) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f @@ -15380,7 +15406,7 @@ Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 732 |- !a. I(I a) = a @@ -15414,12 +15440,12 @@ Run time: 0.2s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Wed Nov 6 11:47:14 -12 2024 +===> abs_theory rebuilt on Thu Nov 7 14:18:45 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -15592,7 +15618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -15772,7 +15798,7 @@ Run time: 0.0s TRAT_EQ_TRANS = |- !p q r. p trat_eq q /\ q trat_eq r ==> p trat_eq r -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 152 TRAT_EQ_AP = |- !p q. (p = q) ==> p trat_eq q @@ -15788,7 +15814,7 @@ Intermediate theorems generated: 62 TRAT_MUL_SYM_EQ = |- !h i. h trat_mul i = i trat_mul h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 58 TRAT_INV_WELLDEFINED = @@ -15860,7 +15886,7 @@ Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 @@ -15872,7 +15898,7 @@ Run time: 0.0s TRAT_NOZERO = |- !h i. ~(h trat_add i) trat_eq h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... @@ -16000,7 +16026,7 @@ HRAT_ADD_TOTAL = |- !h i. (h = i) \/ (?d. h = i hrat_add d) \/ (?d. i = h hrat_add d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 5 HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16013,7 +16039,7 @@ Run time: 0.0s () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 @@ -16029,7 +16055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -16215,7 +16241,7 @@ HRAT_LT_LADD = |- !x y z. (z hrat_add x) hrat_lt (z hrat_add y) = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 77 HRAT_LT_RADD = @@ -16231,7 +16257,7 @@ HRAT_LT_LMUL = |- !x y z. (z hrat_mul x) hrat_lt (z hrat_mul y) = x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 149 HRAT_LT_RMUL = @@ -16343,11 +16369,11 @@ Intermediate theorems generated: 49 CUT_UP = |- !X x. cut X x ==> (?y. cut X y /\ x hrat_lt y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 42 CUT_UBOUND = |- !X x y. ~cut X x /\ x hrat_lt y ==> ~cut X y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y @@ -16417,7 +16443,7 @@ Intermediate theorems generated: 2 hreal_lt = |- !X Y. X hreal_lt Y = ~(X = Y) /\ (!x. cut X x ==> cut Y x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 HREAL_INV_ISACUT = @@ -16425,7 +16451,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 = @@ -16448,12 +16474,12 @@ HREAL_ADD_ASSOC = |- !X Y Z. X hreal_add (Y hreal_add Z) = (X hreal_add Y) hreal_add Z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 490 HREAL_MUL_ASSOC = |- !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 490 HREAL_LDISTRIB = @@ -16481,7 +16507,7 @@ Intermediate theorems generated: 2 HREAL_LT_LEMMA = |- !X Y. X hreal_lt Y ==> (?x. ~cut X x /\ cut Y x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 210 HREAL_SUB_ISACUT = @@ -16505,7 +16531,7 @@ HREAL_ADD_TOTAL = |- !X Y. (X = Y) \/ (?D. Y = X hreal_add D) \/ (?D. X = Y hreal_add D) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 HREAL_SUP_ISACUT = @@ -16539,7 +16565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -16719,7 +16745,7 @@ HREAL_LT_LADD = |- !x y z. (x hreal_add y) hreal_lt (x hreal_add z) = y hreal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 77 CANCEL_CONV = - : ((thm # thm # thm list) -> conv) @@ -16824,7 +16850,7 @@ TREAL_MUL_ASSOC = |- !x y z. x treal_mul (y treal_mul z) = (x treal_mul y) treal_mul z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 388 TREAL_LDISTRIB = @@ -16866,7 +16892,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 @@ -16891,7 +16917,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -16916,7 +16942,7 @@ TREAL_BIJ_WELLDEF = |- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1446 TREAL_NEG_WELLDEF = @@ -16940,7 +16966,7 @@ TREAL_MUL_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 TREAL_MUL_WELLDEF = @@ -16969,7 +16995,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -16998,7 +17024,7 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -17068,7 +17094,7 @@ |- !x y z. y real_lt z ==> (x real_add y) real_lt (x real_add z); |- !x y. r0 real_lt x /\ r0 real_lt y ==> r0 real_lt (x real_mul y)] : thm list -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -17087,7 +17113,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -17383,7 +17409,7 @@ Intermediate theorems generated: 19 REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 55 REAL_LET_TOTAL = |- !x y. x <= y \/ y < x @@ -17399,7 +17425,7 @@ Intermediate theorems generated: 21 REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) @@ -17463,11 +17489,11 @@ Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 REAL_LE_01 = |- (& 0) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 6 REAL_LT_01 = |- (& 0) < (& 1) @@ -17519,7 +17545,7 @@ Intermediate theorems generated: 16 REAL_SUB_REFL = |- !x. x - x = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_SUB_0 = |- !x y. (x - y = & 0) = (x = y) @@ -17547,7 +17573,7 @@ Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 REAL_SUB_LT = |- !x y. (& 0) < (x - y) = y < x @@ -17607,7 +17633,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) @@ -17631,7 +17657,7 @@ Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17672,7 +17698,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 @@ -17687,7 +17713,7 @@ Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 Theorem LESS_EQUAL_ANTISYM autoloading from theory `arithmetic` ... @@ -17744,7 +17770,7 @@ Intermediate theorems generated: 20 REAL_LT_NZ = |- !n. ~(& n = & 0) = (& 0) < (& n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 90 REAL_NZ_IMP_LT = |- !n. ~(n = 0) ==> (& 0) < (& n) @@ -17761,7 +17787,7 @@ REAL_LT_FRACTION_0 = |- !n d. ~(n = 0) ==> ((& 0) < (d / (& n)) = (& 0) < d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 44 Theorem LESS_TRANS autoloading from theory `arithmetic` ... @@ -17813,7 +17839,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 = @@ -17822,7 +17848,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) @@ -17858,11 +17884,11 @@ Intermediate theorems generated: 73 REAL_SUB_LZERO = |- !x. (& 0) - x = -- x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 REAL_SUB_RZERO = |- !x. x - (& 0) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_LET_ADD2 = |- !w x y z. w <= x /\ y < z ==> (w + y) < (x + z) @@ -17897,11 +17923,11 @@ Intermediate theorems generated: 23 REAL_SUB_RNEG = |- !x y. x - (-- y) = x + y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c @@ -17936,11 +17962,11 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_MEAN = |- !x y. x < y ==> (?z. x < z /\ z < y) @@ -17977,7 +18003,7 @@ REAL_LE_RMUL_IMP = |- !x y z. (& 0) <= x /\ y <= z ==> (y * x) <= (z * x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 26 REAL_EQ_IMP_LE = |- !x y. (x = y) ==> x <= y @@ -18009,7 +18035,7 @@ Intermediate theorems generated: 25 REAL_DIFFSQ = |- !x y. (x + y) * (x - y) = (x * x) - (y * y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 165 REAL_POSSQ = |- !x. (& 0) < (x * x) = ~(x = & 0) @@ -18017,7 +18043,7 @@ Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) @@ -18038,7 +18064,7 @@ Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) @@ -18054,7 +18080,7 @@ Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) @@ -18062,7 +18088,7 @@ Intermediate theorems generated: 604 ABS_POS = |- !x. (& 0) <= (abs x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) @@ -18079,7 +18105,7 @@ Intermediate theorems generated: 31 ABS_NZ = |- !x. ~(x = & 0) = (& 0) < (abs x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) @@ -18120,7 +18146,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -18145,7 +18171,7 @@ Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 ABS_BETWEEN2 = @@ -18154,7 +18180,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -18170,7 +18196,7 @@ Intermediate theorems generated: 56 POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) @@ -18178,7 +18204,7 @@ Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 83 POW_PLUS1 = @@ -18203,7 +18229,7 @@ Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) @@ -18211,7 +18237,7 @@ 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 @@ -18231,7 +18257,7 @@ Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -18239,7 +18265,7 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) @@ -18277,7 +18303,7 @@ |- !d. (!y. (?x. (\x. P(x + d))x /\ y < x) = y < s) ==> (!y. (?x. P x /\ y < x) = y < (s + d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) @@ -18297,7 +18323,7 @@ Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 REAL_SUP = @@ -18334,7 +18360,7 @@ Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 342 Theorem PRE autoloading from theory `prim_rec` ... @@ -18355,7 +18381,7 @@ sum = |- (!n f. sum n 0 f = & 0) /\ (!n m f. sum n(SUC m)f = (sum n m f) + (f(n num_add m))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f @@ -18372,7 +18398,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.0s +Run time: 0.1s Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) @@ -18391,7 +18417,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.1s +Run time: 0.0s Intermediate theorems generated: 272 SUM_EQ = @@ -18413,11 +18439,11 @@ SUM_ABS = |- !f m n. abs(Sum(m,n)(\m. abs(f m))) = Sum(m,n)(\m. abs(f m)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 105 Theorem ADD_ASSOC autoloading from theory `arithmetic` ... @@ -18449,7 +18475,7 @@ Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 89 SUM_SUB = @@ -18474,7 +18500,7 @@ |- !f g m n. (!p. m num_le p /\ p num_lt (m num_add n) ==> (f p = g p)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 221 SUM_NSUB = @@ -18495,7 +18521,7 @@ SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18503,7 +18529,7 @@ Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 81 SUM_OFFSET = @@ -18518,7 +18544,7 @@ Intermediate theorems generated: 117 SUM_0 = |- !m n. Sum(m,n)(\r. & 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 72 Theorem ADD_SUC autoloading from theory `arithmetic` ... @@ -18572,7 +18598,7 @@ SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 () : void @@ -18582,7 +18608,7 @@ File real.ml loaded () : void -Run time: 3.1s +Run time: 2.9s Intermediate theorems generated: 23746 #\ @@ -18592,7 +18618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -18786,7 +18812,7 @@ Intermediate theorems generated: 170 closed = |- !L S. closed L S = open L(re_compl S) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 limpt = @@ -18805,7 +18831,7 @@ ismet m = (!x y. (m(x,y) = & 0) = (x = y)) /\ (!x y z. (m(y,z)) <= ((m(x,y)) + (m(x,z)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem REAL_LE_ADD2 autoloading from theory `REAL` ... @@ -18883,7 +18909,7 @@ Run time: 0.0s METRIC_NZ = |- !m x y. ~(x = y) ==> (& 0) < (dist m(x,y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 78 mtop = @@ -18921,7 +18947,7 @@ Intermediate theorems generated: 38 ball = |- !m x e. B m(x,e) = (\y. (dist m(x,y)) < e) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -18989,7 +19015,7 @@ Run time: 0.0s ISMET_R1 = |- ismet(\(x,y). abs(y - x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 204 mr1 = |- mr1 = metric(\(x,y). abs(y - x)) @@ -19046,7 +19072,7 @@ Run time: 0.0s MR1_BETWEEN1 = |- !x y z. x < z /\ (dist mr1(x,y)) < (z - x) ==> y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... @@ -19086,7 +19112,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -19363,7 +19389,7 @@ dorder g ==> (x --> x0)(mtop d,g) /\ (x --> x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 313 SEQ_TENDS = @@ -19821,7 +19847,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -19895,7 +19921,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s real_interface_map = [(`--`, `real_neg`); @@ -19922,7 +19948,7 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 () : void @@ -20127,7 +20153,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.0s +Run time: 0.1s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -20143,7 +20169,7 @@ Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... LESS_SUC_REFL = |- !n. n num_lt (SUC n) -Run time: 0.1s +Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) Run time: 0.0s @@ -20310,7 +20336,7 @@ Theorem REAL_NOT_LT autoloading from theory `REAL` ... REAL_NOT_LT = |- !x y. ~x < y = y <= x -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_REFL autoloading from theory `REAL` ... REAL_LT_REFL = |- !x. ~x < x @@ -20335,7 +20361,7 @@ |- !f. bounded(mr1,$num_ge)f /\ (!m n. m num_ge n ==> (f m) >= (f n)) ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 910 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -20394,7 +20420,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 = @@ -20411,7 +20437,7 @@ Run time: 0.0s SEQ_SUBLE = |- !f. subseq f ==> (!n. n num_le (f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 116 Theorem LESS_EQ_CASES autoloading from theory `arithmetic` ... @@ -20528,7 +20554,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` ... @@ -20797,7 +20823,7 @@ Theorem SUM_TWO autoloading from theory `REAL` ... SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f -Run time: 0.0s +Run time: 0.1s Theorem ABS_ZERO autoloading from theory `REAL` ... ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) @@ -20817,7 +20843,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) <= (f m)) ==> (Sum(0,n)f) <= (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 220 Theorem Sum autoloading from theory `REAL` ... @@ -20971,7 +20997,7 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 395 SER_COMPARA = @@ -20989,7 +21015,7 @@ |- !f g. (!n. (f n) <= (g n)) /\ summable f /\ summable g ==> (suminf f) <= (suminf g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 191 SER_LE2 = @@ -21058,7 +21084,7 @@ Run time: 0.0s GP = |- !x. (abs x) < (& 1) ==> (\n. x pow n) sums (inv((& 1) - x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 343 Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... @@ -21115,7 +21141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -21189,7 +21215,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s real_interface_map = [(`--`, `real_neg`); @@ -21415,7 +21441,7 @@ Run time: 0.0s LIM_NULL = |- !f l x. (f --> l)x = ((\x. (f x) - l) --> (& 0))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 23 LIM_X = |- !x0. ((\x. x) --> x0)x0 @@ -21589,7 +21615,7 @@ Definition real_sub autoloading from theory `REAL` ... real_sub = |- !x y. x - y = x + (-- y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem REAL_NOT_LE autoloading from theory `REAL` ... @@ -21711,7 +21737,7 @@ Theorem REAL_SUB_LDISTRIB autoloading from theory `REAL` ... REAL_SUB_LDISTRIB = |- !x y z. x * (y - z) = (x * y) - (x * z) -Run time: 0.1s +Run time: 0.0s Theorem REAL_ADD_LID autoloading from theory `REAL` ... REAL_ADD_LID = |- !x. (& 0) + x = x @@ -21850,7 +21876,7 @@ Theorem REAL_DIV_REFL autoloading from theory `REAL` ... REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) -Run time: 0.0s +Run time: 0.1s DIFF_X = |- !x. ((\x. x) diffl (& 1))x Run time: 0.0s @@ -21870,7 +21896,7 @@ Theorem ADD_SUB autoloading from theory `arithmetic` ... ADD_SUB = |- !a c. (a num_add c) num_sub c = a -Run time: 0.1s +Run time: 0.0s Theorem ADD1 autoloading from theory `arithmetic` ... ADD1 = |- !m. SUC m = m num_add 1 @@ -21961,7 +21987,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` ... @@ -22022,7 +22048,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` ... @@ -22059,7 +22085,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 = @@ -22134,7 +22160,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f x) <= (f y))) ==> (l = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 88 DIFF_LCONST = @@ -22208,7 +22234,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 = @@ -22221,7 +22247,7 @@ Intermediate theorems generated: 310 DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 172 () : void @@ -22241,7 +22267,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -22687,7 +22713,7 @@ Sum(0,n)(\n. (& n) * ((c n) * (x pow (n num_sub 1)))) = (Sum(0,n)(\n. (diffs c n) * (x pow n))) - ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... @@ -22884,7 +22910,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.1s +Run time: 0.0s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22996,7 +23022,7 @@ Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y -Run time: 0.0s +Run time: 0.1s Theorem ABS_TRIANGLE autoloading from theory `REAL` ... ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) @@ -23093,7 +23119,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -23103,7 +23129,7 @@ File powser.ml loaded () : void -Run time: 0.5s +Run time: 0.6s Intermediate theorems generated: 8507 #\ @@ -23113,7 +23139,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -23281,7 +23307,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.1s +Run time: 0.0s basic_diffs = [] : thm list Run time: 0.0s @@ -23560,7 +23586,7 @@ Theorem REAL_LE_MUL autoloading from theory `REAL` ... REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) -Run time: 0.1s +Run time: 0.0s Theorem REAL_MUL_LZERO autoloading from theory `REAL` ... REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -23654,7 +23680,7 @@ Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... REAL_NEG_LMUL = |- !x y. --(x * y) = (-- x) * y -Run time: 0.0s +Run time: 0.1s Theorem REAL_NEG_0 autoloading from theory `REAL` ... REAL_NEG_0 = |- --(& 0) = & 0 @@ -23732,7 +23758,7 @@ Run time: 0.0s DIFF_COS = |- !x. (cos diffl (--(sin x)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 283 [|- !x. (exp diffl (exp x))x; @@ -23813,7 +23839,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) @@ -23874,7 +23900,7 @@ Run time: 0.0s EXP_POS_LE = |- !x. (& 0) <= (exp x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 27 Theorem REAL_10 autoloading from theory `REAL` ... @@ -23922,7 +23948,7 @@ Run time: 0.0s EXP_MONO_IMP = |- !x y. x < y ==> (exp x) < (exp y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 127 Theorem REAL_NOT_LT autoloading from theory `REAL` ... @@ -24030,7 +24056,7 @@ Run time: 0.0s LN_INV = |- !x. (& 0) < x ==> (ln(inv x) = --(ln x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 81 LN_DIV = |- !x. (& 0) < x /\ (& 0) < y ==> (ln(x / y) = (ln x) - (ln y)) @@ -24057,7 +24083,7 @@ Intermediate theorems generated: 2 sqrt = |- !x. sqrt x = root 2 x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -24124,7 +24150,7 @@ Theorem REAL_DIV_REFL autoloading from theory `REAL` ... REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) -Run time: 0.1s +Run time: 0.0s Theorem DIV_UNIQUE autoloading from theory `arithmetic` ... DIV_UNIQUE = @@ -24133,7 +24159,7 @@ Run time: 0.0s COS_0 = |- cos(& 0) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 @@ -24414,7 +24440,7 @@ Theorem REAL_LT_TOTAL autoloading from theory `REAL` ... REAL_LT_TOTAL = |- !x y. (x = y) \/ x < y \/ y < x -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE_01 autoloading from theory `REAL` ... REAL_LE_01 = |- (& 0) <= (& 1) @@ -24486,7 +24512,7 @@ Intermediate theorems generated: 66 COS_SIN = |- !x. cos x = sin((pi / (& 2)) - x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 SIN_PERIODIC_PI = |- !x. sin(x + pi) = --(sin x) @@ -24510,7 +24536,7 @@ Intermediate theorems generated: 134 SIN_NPI = |- !n. sin((& n) * pi) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 137 SIN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (sin x) @@ -24543,7 +24569,7 @@ Run time: 0.0s SIN_POS_PI = |- !x. (& 0) < x /\ x < pi ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 96 COS_TOTAL = @@ -24594,7 +24620,7 @@ Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... REAL_LT_HALF2 = |- !d. (d / (& 2)) < d = (& 0) < d -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT_HALF1 autoloading from theory `REAL` ... REAL_LT_HALF1 = |- !d. (& 0) < (d / (& 2)) = (& 0) < d @@ -24626,7 +24652,7 @@ |- !x. (& 0) <= x /\ (sin x = & 0) ==> (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 305 Theorem REAL_NEG_EQ autoloading from theory `REAL` ... @@ -24666,7 +24692,7 @@ Intermediate theorems generated: 2 TAN_0 = |- tan(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 TAN_PI = |- tan pi = & 0 @@ -24682,7 +24708,7 @@ Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 Theorem REAL_LDISTRIB autoloading from theory `REAL` ... @@ -24721,7 +24747,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` ... @@ -24794,14 +24820,14 @@ TAN_TOTAL = |- !y. ?! x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1301 asn = |- !y. asn y = (@x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 acs = |- !y. acs y = (@x. (& 0) <= x /\ x <= pi /\ (cos x = y)) @@ -24848,7 +24874,7 @@ Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 ACS_BOUNDS = @@ -24866,7 +24892,7 @@ (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) /\ (tan(atn y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y @@ -24889,7 +24915,7 @@ File transc.ml loaded () : void -Run time: 1.8s +Run time: 2.0s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24902,7 +24928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -24924,7 +24950,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -24990,7 +25016,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25022,7 +25048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25131,7 +25157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25284,7 +25310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25357,7 +25383,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25437,7 +25463,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25594,7 +25620,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25749,7 +25775,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25966,7 +25992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -25988,7 +26014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26007,7 +26033,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26052,7 +26078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26117,7 +26143,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26167,7 +26193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26237,7 +26263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26307,7 +26333,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26343,7 +26369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26396,7 +26422,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26468,7 +26494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26547,7 +26573,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26742,7 +26768,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -26779,7 +26805,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -27465,7 +27491,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -27937,7 +27963,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -28201,7 +28227,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -28446,7 +28472,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -28910,7 +28936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29378,7 +29404,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29434,7 +29460,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29524,7 +29550,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29723,7 +29749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29755,7 +29781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -29889,7 +29915,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30192,7 +30218,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30224,7 +30250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30263,7 +30289,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30295,7 +30321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30456,7 +30482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30589,7 +30615,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30778,7 +30804,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30838,7 +30864,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -30963,7 +30989,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31074,7 +31100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31099,7 +31125,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31127,7 +31153,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31240,7 +31266,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31743,7 +31769,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -31991,7 +32017,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -32217,7 +32243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -32259,7 +32285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -32291,7 +32317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -32514,7 +32540,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -32907,7 +32933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -33020,7 +33046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -33523,7 +33549,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -33771,7 +33797,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -33997,7 +34023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34032,7 +34058,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34071,7 +34097,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34108,7 +34134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34129,7 +34155,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34226,7 +34252,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34248,7 +34274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34744,7 +34770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34767,7 +34793,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34845,7 +34871,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34904,7 +34930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34948,7 +34974,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34966,7 +34992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -34993,7 +35019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35037,7 +35063,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35150,7 +35176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35197,7 +35223,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35236,7 +35262,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35310,7 +35336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35399,7 +35425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35470,7 +35496,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35540,7 +35566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35589,7 +35615,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35630,7 +35656,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35671,7 +35697,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35695,7 +35721,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35796,7 +35822,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35817,7 +35843,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -35842,7 +35868,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36468,7 +36494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36545,7 +36571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36572,7 +36598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36689,7 +36715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36784,7 +36810,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36870,7 +36896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -36985,7 +37011,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37078,7 +37104,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37254,7 +37280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37358,7 +37384,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37653,7 +37679,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37756,7 +37782,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37824,7 +37850,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -37886,7 +37912,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -38066,7 +38092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -38107,7 +38133,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -38137,7 +38163,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -38163,7 +38189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -38681,7 +38707,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -39218,7 +39244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -39406,7 +39432,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 + HOL88 Version 2.02 (GCL), built on 7/11/24 =============================================================================== #false : bool @@ -39424,10 +39450,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Wed Nov 6 11:55:40 -12 2024 +Thu Nov 7 14:27:45 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Nov 6 11:55:40 -12 2024 +Thu Nov 7 14:27:45 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39445,22 +39471,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 6/11/24 -=============================================================================== +BASIC-HOL version 2.02 (GCL) created 7/11/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 6/11/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 7/11/24 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 6/11/24 +HOL-LCF version 2.02 (GCL) created 7/11/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41782,7 +41808,7 @@ make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -44562,7 +44588,7 @@ make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -46994,7 +47020,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' @@ -47301,7 +47327,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -47602,7 +47628,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -47849,7 +47875,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -48105,7 +48131,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' @@ -48265,7 +48291,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -48406,7 +48432,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -48718,7 +48744,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -49254,7 +49280,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -49681,7 +49707,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' @@ -50150,7 +50176,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' @@ -50424,7 +50450,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -50799,7 +50825,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -51030,7 +51056,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -51208,7 +51234,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -51421,7 +51447,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -51665,7 +51691,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -51907,7 +51933,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' @@ -52217,7 +52243,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -52577,7 +52603,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. 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' @@ -52888,7 +52914,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.11.06:1159' -> endpages.ps +' TeX output 2024.11.07:1431' -> endpages.ps @@ -52960,7 +52986,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.11.06:1159' -> titlepages.ps +' TeX output 2024.11.07:1431' -> titlepages.ps @@ -53088,10 +53114,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_makeshlibs: warning: Compatibility levels before 10 are deprecated (level 9 in use) @@ -53101,16 +53129,17 @@ 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_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_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-contrib-source' in '../hol88-contrib-source_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 @@ -53120,12 +53149,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/6687/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/6687/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/6008 and its subdirectories -I: Current time: Wed Nov 6 12:00:50 -12 2024 -I: pbuilder-time-stamp: 1730937650 +I: removing directory /srv/workspace/pbuilder/6687 and its subdirectories +I: Current time: Thu Nov 7 14:33:05 +14 2024 +I: pbuilder-time-stamp: 1730939585