Diff of the two buildlogs: -- --- b1/build.log 2024-04-13 00:49:39.526613301 +0000 +++ b2/build.log 2024-04-13 02:05:58.255585843 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Fri Apr 12 12:16:13 -12 2024 -I: pbuilder-time-stamp: 1712967373 +I: Current time: Sat Apr 13 14:50:28 +14 2024 +I: pbuilder-time-stamp: 1712969428 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/1106/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/4610/tmp/hooks/D01_modify_environment starting +debug: Running on cbxi4pro0. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Apr 13 00:51 /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/4610/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/4610/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]="21" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='c8ece5a3f82046f38a74f7239959cd93' - 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='1106' - PS1='# ' - PS2='> ' + INVOCATION_ID=057ed94a73964b4b9aab4413fc184e9e + 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=4610 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.uavRSNAc/pbuilderrc_9N8D --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.uavRSNAc/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.uavRSNAc/pbuilderrc_vRA9 --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.uavRSNAc/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=113 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://10.0.0.15:3142/ I: uname -a - Linux virt64a 6.1.0-18-arm64 #1 SMP Debian 6.1.76-1 (2024-02-01) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-18-armmp #1 SMP Debian 6.1.76-1 (2024-02-01) armv7l GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Apr 11 11:25 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/1106/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Apr 12 11:26 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/4610/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -303,7 +335,7 @@ Get: 188 http://deb.debian.org/debian trixie/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 189 http://deb.debian.org/debian trixie/main armhf texlive-base all 2023.20240207-1 [22.0 MB] Get: 190 http://deb.debian.org/debian trixie/main armhf texlive-latex-base all 2023.20240207-1 [1255 kB] -Fetched 176 MB in 6s (29.8 MB/s) +Fetched 176 MB in 12s (14.3 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 ... 19635 files and directories currently installed.) @@ -940,8 +972,8 @@ Setting up tzdata (2024a-1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Apr 13 00:18:46 UTC 2024. -Universal Time is now: Sat Apr 13 00:18:46 UTC 2024. +Local time is now: Sat Apr 13 00:53:30 UTC 2024. +Universal Time is now: Sat Apr 13 00:53:30 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libdconf1:armhf (0.40.0-4+b1) ... @@ -1133,7 +1165,11 @@ fakeroot is already the newest version (1.33-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/4610/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/4610/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 @@ -1394,12 +1430,6 @@ 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' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1407,78 +1437,84 @@ 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' +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/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/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' +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/string/Manual' +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/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/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/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/pred_sets/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/pred_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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' 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/sets/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/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +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/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/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/prettyp/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' +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/word/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ - 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/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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]: 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]: 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/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/reals/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ + 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/reals/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' 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 \ @@ -1526,7 +1562,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 12 12:27:15 -12 2024 +Sat Apr 13 15:09:09 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2764,7 +2800,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 # mem = - : (* -> * list -> bool) @@ -2902,7 +2938,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #.............start address -T 0x7b05e8 () : void @@ -3061,7 +3097,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #.............start address -T 0x7b05e8 () : void @@ -3253,7 +3289,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 # concat = - : (string -> string -> string) @@ -3363,7 +3399,7 @@ start address -T 0x6c8a28 ;; Finished loading "lisp/f-ol-net" start address -T 0x7ffd80 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 12/4/24 + version 2.02 (GCL) created 13/4/24 #...start address -T 0x6d6650 () : void @@ -3692,7 +3728,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 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 ###########################() : void @@ -3705,7 +3741,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 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 ################################################################################################() : void @@ -3850,7 +3886,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 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 ############################() : void @@ -3893,7 +3929,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 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 ############################Theory ind loaded () : void @@ -3930,7 +3966,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3971,7 +4007,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4373,7 +4409,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4441,7 +4477,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4646,7 +4682,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4770,7 +4806,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4856,7 +4892,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -4949,7 +4985,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5018,7 +5054,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5123,7 +5159,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5358,7 +5394,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5384,7 +5420,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5512,7 +5548,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5560,7 +5596,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5627,7 +5663,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5686,7 +5722,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5742,7 +5778,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 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre5 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5755,7 +5791,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 12/4/24 +HOL-LCF version 2.02 (GCL) created 13/4/24 #() : void @@ -5807,7 +5843,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ##########################() : void @@ -5838,7 +5874,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ##############################() : void @@ -5925,7 +5961,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #######################################################################() : void @@ -6078,7 +6114,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ###########################() : void @@ -6113,7 +6149,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #############################() : void @@ -6174,7 +6210,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ###########################Theory arithmetic loaded () : void @@ -6669,7 +6705,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ##################################() : void @@ -6816,7 +6852,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #################################Theory list loaded () : void @@ -7155,7 +7191,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ###############################Theory list loaded () : void @@ -8652,7 +8688,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #############################() : void @@ -9036,7 +9072,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ############################() : void @@ -9334,7 +9370,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ############################() : void @@ -9474,7 +9510,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ############################################() : void @@ -9571,7 +9607,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 ##################################() : void @@ -9601,7 +9637,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -9618,7 +9654,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #Theory num loaded () : void @@ -9637,7 +9673,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -9794,7 +9830,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 # @@ -9832,7 +9868,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 # @@ -9866,7 +9902,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -9951,7 +9987,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -9992,7 +10028,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -10176,7 +10212,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 # define_load_lib_function = - : (string list -> void -> void) @@ -10252,7 +10288,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 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre5 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10265,7 +10301,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #() : void @@ -10329,11 +10365,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 12 12:32:30 -12 2024 +Sat Apr 13 15:23:30 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 12 12:32:31 -12 2024 +Sat Apr 13 15:23:31 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10356,7 +10392,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -10440,7 +10476,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -10546,7 +10582,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11296,7 +11332,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11319,7 +11355,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11362,7 +11398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11398,7 +11434,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11450,7 +11486,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11482,7 +11518,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11520,7 +11556,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11548,7 +11584,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11625,7 +11661,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11647,7 +11683,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11701,7 +11737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11750,7 +11786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11901,7 +11937,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -11945,7 +11981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12020,7 +12056,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12070,7 +12106,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12133,7 +12169,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12186,7 +12222,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12232,7 +12268,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12320,7 +12356,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12358,7 +12394,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12419,7 +12455,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12483,7 +12519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12509,7 +12545,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12534,7 +12570,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12573,7 +12609,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -12649,7 +12685,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13386,7 +13422,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13409,7 +13445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13452,7 +13488,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13487,7 +13523,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13528,7 +13564,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13591,7 +13627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13614,7 +13650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13639,7 +13675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13666,7 +13702,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -13702,7 +13738,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14234,7 +14270,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14257,7 +14293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14291,7 +14327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14346,7 +14382,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14437,7 +14473,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14606,7 +14642,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -14697,7 +14733,7 @@ Intermediate theorems generated: 2 linseg = |- !l a. wo_linseg l a = (\(x,y). l(x,y) /\ wo_less l(y,a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 ordinal = @@ -14774,7 +14810,7 @@ Intermediate theorems generated: 1294 PAIRED_EXT = |- !l m. (!x y. l(x,y) = m(x,y)) = (l = m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 63 WOSET_REFL = |- !l. woset l ==> (!x. fl l x ==> l(x,x)) @@ -14849,7 +14885,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (!n. ?f. !x. l(ms x,n) ==> (f x = h f x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14859,7 +14895,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (?f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 444 WO_RECURSE = @@ -14874,7 +14910,7 @@ Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... LESS_EQ_REFL = |- !m. m <= m -Run time: 0.1s +Run time: 0.0s FL_NUM = |- !n. fl(\(m,n). m <= n)n Run time: 0.0s @@ -14913,7 +14949,7 @@ Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 170 UNION_INSEG = |- !P l. (!m. P m ==> m inseg l) ==> (Union P) inseg l @@ -14941,7 +14977,7 @@ Intermediate theorems generated: 39 LINSEG_FL = |- !l a x. woset l ==> (fl(linseg l a)x = less l(x,a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 142 INSEG_PROPER_SUBSET = @@ -14958,17 +14994,17 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1172 EXTEND_FL = |- !l x. woset l ==> (fl(\(x,y). l(x,y) /\ l(y,a))x = l(x,a)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 143 EXTEND_INSEG = |- !l a. woset l /\ fl l a ==> (\(x,y). l(x,y) /\ l(y,a)) inseg l -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 57 EXTEND_LINSEG = @@ -14981,14 +15017,14 @@ 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 = |- !l a. fl(\(x,y). l(x,y) \/ (y = a) /\ (fl l x \/ (x = a)))x = fl l x \/ (x = a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -14997,22 +15033,22 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = |- !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 = |- !l. ordinal l ==> (!x. fl l x) \/ (?m x. ordinal m /\ fl m x /\ ~fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 154 WO_LEMMA = |- ?l. ordinal l /\ (!x. fl l x) @@ -15022,7 +15058,7 @@ WO_FL_RESTRICT = |- !l. woset l ==> (!P. fl(\(x,y). P x /\ P y /\ l(x,y))x = P x /\ fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -15040,7 +15076,7 @@ |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -15069,7 +15105,7 @@ File mk_wellorder loaded () : void -Run time: 0.9s +Run time: 2.5s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15078,7 +15114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -15100,7 +15136,7 @@ .loading abs_theory .Extending help search path......................................() : void -Run time: 0.0s +Run time: 0.1s SYM_RULE = - : (thm -> thm) Run time: 0.0s @@ -15202,14 +15238,14 @@ 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 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -15238,7 +15274,7 @@ /bin/rm: cannot remove 'group_def.th': No such file or directory 1 : int -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -15258,7 +15294,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 = @@ -15284,7 +15320,7 @@ ALTERNATE_INVERSE_INVERSE_LEMMA = |- !g. IS_GROUP g ==> (!a. inv g(inv g a) = a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 69 () : void @@ -15294,14 +15330,14 @@ File ../../Library/abs_theory/group_def.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 1089 Making ../../Library/abs_theory/example.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -15323,7 +15359,7 @@ .loading abs_theory .Extending help search path......................................() : void -Run time: 0.0s +Run time: 0.1s /bin/rm: cannot remove 'example.th': No such file or directory 1 : int @@ -15355,7 +15391,7 @@ Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) @@ -15363,7 +15399,7 @@ Intermediate theorems generated: 732 |- !a. I(I a) = a -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1106 concrete_rep = "group(\x y. x = y)T I" : term @@ -15380,7 +15416,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 2546 () : void @@ -15390,15 +15426,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.2s +Run time: 0.6s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Fri Apr 12 12:35:10 -12 2024 +===> abs_theory rebuilt on Sat Apr 13 15:29:44 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -15558,7 +15594,7 @@ File abs_theory compiled () : void -Run time: 0.1s +Run time: 0.2s make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals' @@ -15571,7 +15607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -15658,7 +15694,7 @@ File equiv loaded () : void -Run time: 0.0s +Run time: 0.1s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -15721,7 +15757,7 @@ trat_sucint = |- (trat_sucint 0 = trat_1) /\ (!n. trat_sucint(SUC n) = (trat_sucint n) trat_add trat_1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 trat_eq = @@ -15781,7 +15817,7 @@ TRAT_ADD_WELLDEFINED = |- !p q r. p trat_eq q ==> (p trat_add r) trat_eq (q trat_add r) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 297 TRAT_ADD_WELLDEFINED2 = @@ -15818,7 +15854,7 @@ Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 15 TRAT_MUL_ASSOC = @@ -15835,7 +15871,7 @@ |- !h i j. (h trat_mul (i trat_add j)) trat_eq ((h trat_mul i) trat_add (h trat_mul j)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h @@ -15871,7 +15907,7 @@ h trat_eq i \/ (?d. h trat_eq (i trat_add d)) \/ (?d. i trat_eq (h trat_add d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) @@ -15938,7 +15974,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.2s +Run time: 0.4s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -15956,7 +15992,7 @@ HRAT_MUL_ASSOC = |- !h i j. h hrat_mul (i hrat_mul j) = (h hrat_mul i) hrat_mul j -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 7 HRAT_LDISTRIB = @@ -15998,7 +16034,7 @@ File hrat.ml loaded () : void -Run time: 0.4s +Run time: 1.2s Intermediate theorems generated: 11032 #\ @@ -16008,7 +16044,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -16082,7 +16118,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -16183,7 +16219,7 @@ Run time: 0.0s HRAT_EQ_LMUL = |- !x y z. (x hrat_mul y = x hrat_mul z) = (y = z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 50 HRAT_LT_ADD2 = @@ -16237,7 +16273,7 @@ HRAT_LT_R1 = |- !x y. (x hrat_mul (hrat_inv y)) hrat_lt hrat_1 = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 10 HRAT_GT_L1 = @@ -16281,7 +16317,7 @@ Intermediate theorems generated: 2 ISACUT_HRAT = |- !h. isacut(cut_of_hrat h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 221 hreal_tydef = |- ?rep. TYPE_DEFINITION isacut rep @@ -16330,12 +16366,12 @@ Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 137 Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... LESS_SUC_REFL = |- !n. n < (SUC n) -Run time: 0.1s +Run time: 0.0s Theorem NOT_LESS_0 autoloading from theory `prim_rec` ... NOT_LESS_0 = |- !n. ~n < 0 @@ -16404,7 +16440,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 = @@ -16427,7 +16463,7 @@ HREAL_ADD_ASSOC = |- !X Y Z. X hreal_add (Y hreal_add Z) = (X hreal_add Y) hreal_add Z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 490 HREAL_MUL_ASSOC = @@ -16439,7 +16475,7 @@ |- !X Y Z. X hreal_mul (Y hreal_add Z) = (X hreal_mul Y) hreal_add (X hreal_mul Z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 HREAL_MUL_LID = |- !X. hreal_1 hreal_mul X = X @@ -16471,7 +16507,7 @@ HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16498,7 +16534,7 @@ |- !P. (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==> (!Y. (?X. P X /\ Y hreal_lt X) = Y hreal_lt (hreal_sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 553 () : void @@ -16508,7 +16544,7 @@ File hreal.ml loaded () : void -Run time: 0.5s +Run time: 1.5s Intermediate theorems generated: 10456 #\ @@ -16518,7 +16554,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -16592,7 +16628,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -16658,7 +16694,7 @@ Run time: 0.0s HREAL_EQ_LADD = |- !x y z. (x hreal_add y = x hreal_add z) = (y = z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 94 Theorem HREAL_LT autoloading from theory `HREAL` ... @@ -16749,7 +16785,7 @@ (y hreal_lt x => ((hreal_inv(x hreal_sub y)) hreal_add hreal_1,hreal_1) | (hreal_1,(hreal_inv(y hreal_sub x)) hreal_add hreal_1))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 treal_eq = @@ -16776,7 +16812,7 @@ Intermediate theorems generated: 73 TREAL_EQ_AP = |- !p q. (p = q) ==> p treal_eq q -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 8 TREAL_10 = |- ~treal_1 treal_eq treal_0 @@ -16810,11 +16846,11 @@ |- !x y z. x treal_mul (y treal_add z) = (x treal_mul y) treal_add (x treal_mul z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 345 TREAL_ADD_LID = |- !x. (treal_0 treal_add x) treal_eq x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 158 Theorem HREAL_MUL_LID autoloading from theory `HREAL` ... @@ -16845,7 +16881,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.2s Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x @@ -16885,7 +16921,7 @@ |- (!h. hreal_of_treal(treal_of_hreal h) = h) /\ (!r. treal_0 treal_lt r = (treal_of_hreal(hreal_of_treal r)) treal_eq r) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 986 TREAL_ISO = @@ -16895,7 +16931,7 @@ TREAL_BIJ_WELLDEF = |- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1446 TREAL_NEG_WELLDEF = @@ -16919,7 +16955,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 = @@ -16948,7 +16984,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -16977,7 +17013,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.3s +Run time: 0.6s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -16986,7 +17022,7 @@ Intermediate theorems generated: 98 REAL_POS = |- !X. r0 real_lt (real_of_hreal X) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 SUP_ALLPOS_LEMMA1 = @@ -17027,7 +17063,7 @@ (?x. P x) /\ (?z. !x. P x ==> x real_lt z) ==> (?s. !y. (?x. P x /\ y real_lt x) = y real_lt s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 199 [|- ~(r1 = r0); @@ -17056,7 +17092,7 @@ File realax.ml loaded () : void -Run time: 0.8s +Run time: 2.2s Intermediate theorems generated: 26795 #\ @@ -17066,7 +17102,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -17140,7 +17176,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -17235,7 +17271,7 @@ Intermediate theorems generated: 2 REAL_LT_TOTAL = |- !x y. (x = y) \/ x < y \/ y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 REAL_LT_REFL = |- !x. ~x < x @@ -17286,7 +17322,7 @@ Intermediate theorems generated: 50 REAL_EQ_RADD = |- !x y z. (x + z = y + z) = (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 REAL_ADD_LID_UNIQ = |- !x y. (x + y = y) = (x = & 0) @@ -17294,7 +17330,7 @@ Intermediate theorems generated: 21 REAL_ADD_RID_UNIQ = |- !x y. (x + y = x) = (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_LNEG_UNIQ = |- !x y. (x + y = & 0) = (x = -- y) @@ -17334,7 +17370,7 @@ Intermediate theorems generated: 56 REAL_ENTIRE = |- !x y. (x * y = & 0) = (x = & 0) \/ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 116 REAL_LT_LADD = |- !x y z. (x + y) < (x + z) = y < z @@ -17374,7 +17410,7 @@ Intermediate theorems generated: 27 REAL_LE_REFL = |- !x. x <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 21 REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) @@ -17386,7 +17422,7 @@ Intermediate theorems generated: 125 REAL_LT_IMP_LE = |- !x y. x < y ==> x <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_LTE_TRANS = |- !x y z. x < y /\ y <= z ==> x < z @@ -17466,7 +17502,7 @@ Intermediate theorems generated: 55 REAL_LE_ADD2 = |- !w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 55 REAL_LE_ADD = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x + y) @@ -17486,7 +17522,7 @@ Intermediate theorems generated: 49 REAL_LT_ADD1 = |- !x y. x <= y ==> x < (y + (& 1)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 75 REAL_SUB_ADD = |- !x y. (x - y) + y = x @@ -17530,7 +17566,7 @@ Intermediate theorems generated: 32 REAL_SUB_LT = |- !x y. (& 0) < (x - y) = y < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 REAL_SUB_LE = |- !x y. (& 0) <= (x - y) = y <= x @@ -17542,7 +17578,7 @@ Intermediate theorems generated: 61 REAL_EQ_LMUL = |- !x y z. (x * y = x * z) = (x = & 0) \/ (y = z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 122 REAL_EQ_RMUL = |- !x y z. (x * z = y * z) = (z = & 0) \/ (x = y) @@ -17590,7 +17626,7 @@ Intermediate theorems generated: 18 REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 57 REAL_LT_RMUL = |- !x y z. (& 0) < z ==> ((x * z) < (y * z) = x < y) @@ -17606,11 +17642,11 @@ Intermediate theorems generated: 29 REAL_LINV_UNIQ = |- !x y. (x * y = & 1) ==> (x = inv y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17634,7 +17670,7 @@ Intermediate theorems generated: 20 REAL_LT_ADDL = |- !x y. y < (x + y) = (& 0) < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 REAL = |- !n. &(SUC n) = (& n) + (& 1) @@ -17651,7 +17687,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 @@ -17666,7 +17702,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` ... @@ -17688,7 +17724,7 @@ Intermediate theorems generated: 1 REAL_ADD = |- !m n. (& m) + (& n) = &(m num_add n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 131 Theorem MULT_CLAUSES autoloading from theory `arithmetic` ... @@ -17715,7 +17751,7 @@ Intermediate theorems generated: 22 REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 REAL_DIV_LZERO = |- !x. (& 0) / x = & 0 @@ -17735,7 +17771,7 @@ Intermediate theorems generated: 40 REAL_LT_RDIV = |- !x y z. (& 0) < z ==> ((x / z) < (y / z) = x < y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 44 REAL_LT_FRACTION_0 = @@ -17752,7 +17788,7 @@ Run time: 0.0s REAL_LT_MULTIPLE = |- !n d. 1 num_lt n ==> (d < ((& n) * d) = (& 0) < d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) @@ -17780,7 +17816,7 @@ Intermediate theorems generated: 37 REAL_DIV_LMUL = |- !x y. ~(y = & 0) ==> (y * (x / y) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 70 REAL_DIV_RMUL = |- !x y. ~(y = & 0) ==> ((x / y) * y = x) @@ -17809,7 +17845,7 @@ Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -17817,7 +17853,7 @@ Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 38 REAL_LE_SUB_RADD = |- !x y z. (x - y) <= z = x <= (z + y) @@ -17837,7 +17873,7 @@ 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 @@ -17853,11 +17889,11 @@ Intermediate theorems generated: 33 REAL_LET_ADD = |- !x y. (& 0) <= x /\ (& 0) < y ==> (& 0) < (x + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LTE_ADD = |- !x y. (& 0) < x /\ (& 0) <= y ==> (& 0) < (x + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 REAL_LT_MUL2 = @@ -17868,7 +17904,7 @@ Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -17884,7 +17920,7 @@ Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 93 REAL_EQ_SUB_LADD = |- !x y z. (x = y - z) = (x + z = y) @@ -17897,11 +17933,11 @@ REAL_INV_MUL = |- !x y. ~(x = & 0) /\ ~(y = & 0) ==> (inv(x * y) = (inv x) * (inv y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 142 REAL_LE_LMUL = |- !x y z. (& 0) < x ==> ((x * y) <= (x * z) = y <= z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) @@ -17911,7 +17947,7 @@ REAL_SUB_INV2 = |- !x y. ~(x = & 0) /\ ~(y = & 0) ==> ((inv x) - (inv y) = (y - x) / (x * y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y @@ -17927,7 +17963,7 @@ Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 REAL_LE_MUL2 = @@ -17956,7 +17992,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 @@ -17972,7 +18008,7 @@ Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) @@ -18013,7 +18049,7 @@ Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) @@ -18037,7 +18073,7 @@ Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 604 ABS_POS = |- !x. (& 0) <= (abs x) @@ -18045,7 +18081,7 @@ Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 385 ABS_LT_MUL2 = @@ -18058,7 +18094,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)) @@ -18070,7 +18106,7 @@ Intermediate theorems generated: 27 ABS_LE = |- !x. x <= (abs x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 75 ABS_REFL = |- !x. (abs x = x) = (& 0) <= x @@ -18083,15 +18119,15 @@ ABS_BETWEEN = |- !x y d. (& 0) < d /\ (x - d) < y /\ y < (x + d) = (abs(y - x)) < d -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) @@ -18103,7 +18139,7 @@ Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) @@ -18116,7 +18152,7 @@ ABS_CIRCLE = |- !x y h. (abs h) < ((abs y) - (abs x)) ==> (abs(x + h)) < (abs y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 61 REAL_SUB_ABS = |- !x y. ((abs x) - (abs y)) <= (abs(x - y)) @@ -18137,7 +18173,7 @@ Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -18157,7 +18193,7 @@ Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 83 POW_PLUS1 = @@ -18174,7 +18210,7 @@ Run time: 0.0s POW_ADD = |- !c m n. c pow (m num_add n) = (c pow m) * (c pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 152 POW_1 = |- !x. x pow 1 = x @@ -18182,7 +18218,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)) @@ -18190,11 +18226,11 @@ Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -18206,7 +18242,7 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 @@ -18218,11 +18254,11 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 73 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -18238,7 +18274,7 @@ Run time: 0.0s POW_2_LT = |- !n. (& n) < ((& 2) pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 POW_MINUS1 = |- !n. (--(& 1)) pow (2 num_mul n) = & 1 @@ -18249,7 +18285,7 @@ |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -18276,7 +18312,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 = @@ -18296,7 +18332,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) = (?x. P x) /\ (?z. !x. P x ==> x < z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 REAL_SUP_LE = @@ -18309,7 +18345,7 @@ REAL_SUP_UBOUND_LE = |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) @@ -18328,7 +18364,7 @@ |- !y. (& 0) < y ==> (!x. (& 0) <= x ==> (?n. ((& n) * y) <= x /\ x < ((&(SUC n)) * y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 222 sum = @@ -18338,7 +18374,7 @@ Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Sum = @@ -18360,7 +18396,7 @@ Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... LESS_EQ_ADD = |- !m n. m num_le (m num_add n) -Run time: 0.0s +Run time: 0.1s Theorem ADD_SYM autoloading from theory `arithmetic` ... ADD_SYM = |- !m n. m num_add n = n num_add m @@ -18377,7 +18413,7 @@ |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r = g r)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 82 SUM_POS = |- !f. (!n. (& 0) <= (f n)) ==> (!m n. (& 0) <= (Sum(m,n)f)) @@ -18387,7 +18423,7 @@ SUM_POS_GEN = |- !f m. (!n. m num_le n ==> (& 0) <= (f n)) ==> (!n. (& 0) <= (Sum(m,n)f)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 SUM_ABS = @@ -18409,7 +18445,7 @@ Theorem GREATER_EQ autoloading from theory `arithmetic` ... GREATER_EQ = |- !n m. n num_ge m = m num_le n -Run time: 0.0s +Run time: 0.1s SUM_ZERO = |- !f N. @@ -18453,7 +18489,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.0s +Run time: 0.1s Intermediate theorems generated: 221 SUM_NSUB = @@ -18488,16 +18524,16 @@ SUM_OFFSET = |- !f n k. Sum(0,n)(\m. f(m num_add k)) = (Sum(0,n num_add k)f) - (Sum(0,k)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 141 SUM_REINDEX = |- !f m k n. Sum(m num_add k,n)f = Sum(m,n)(\r. f(r num_add k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 117 SUM_0 = |- !m n. Sum(m,n)(\r. & 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 72 Theorem ADD_SUC autoloading from theory `arithmetic` ... @@ -18545,7 +18581,7 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2469 SUM_CANCEL = @@ -18555,13 +18591,13 @@ Intermediate theorems generated: 206 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File real.ml loaded () : void -Run time: 2.7s +Run time: 7.8s Intermediate theorems generated: 23746 #\ @@ -18571,7 +18607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -18744,7 +18780,7 @@ Intermediate theorems generated: 2 OPEN_OWN_NEIGH = |- !S top x. open top S /\ S x ==> neigh top(S,x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 OPEN_UNOPEN = @@ -18772,7 +18808,7 @@ |- !top x S. limpt top x S = (!N. neigh top(N,x) ==> (?y. ~(x = y) /\ S y /\ N y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 CLOSED_LIMPT = |- !top S. closed top S = (!x. limpt top x S ==> S x) @@ -18812,7 +18848,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 560 metric_tybij = @@ -18854,7 +18890,7 @@ METRIC_TRIANGLE = |- !m x y z. (dist m(x,z)) <= ((dist m(x,y)) + (dist m(y,z))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 52 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -18889,7 +18925,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18931,7 +18967,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -19025,7 +19061,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` ... @@ -19034,7 +19070,7 @@ Theorem REAL_ADD_RID_UNIQ autoloading from theory `REAL` ... REAL_ADD_RID_UNIQ = |- !x y. (x + y = x) = (y = & 0) -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... REAL_LT_HALF2 = |- !d. (d / (& 2)) < d = (& 0) < d @@ -19055,7 +19091,7 @@ File topology.ml loaded () : void -Run time: 0.4s +Run time: 1.0s Intermediate theorems generated: 4132 #\ @@ -19065,7 +19101,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -19139,7 +19175,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s real_interface_map = [(`--`, `real_neg`); @@ -19170,7 +19206,7 @@ Intermediate theorems generated: 30 () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -19267,7 +19303,7 @@ Theorem REAL_LE_REFL autoloading from theory `REAL` ... REAL_LE_REFL = |- !x. x <= x -Run time: 0.0s +Run time: 0.1s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) Run time: 0.0s @@ -19379,7 +19415,7 @@ (!x. (& 0) < (dist m1(x,x0)) /\ (dist m1(x,x0)) <= d ==> (dist m2(f x,y0)) < e)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 459 Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... @@ -19449,7 +19485,7 @@ NET_NULL = |- !g x x0. (x --> x0)(mtop mr1,g) = ((\n. (x n) - x0) --> (& 0))(mtop mr1,g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 151 Theorem LESS_0 autoloading from theory `prim_rec` ... @@ -19462,7 +19498,7 @@ NET_CONV_BOUNDED = |- !g x x0. (x --> x0)(mtop mr1,g) ==> bounded(mr1,g)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 119 Theorem REAL_LT_REFL autoloading from theory `REAL` ... @@ -19537,7 +19573,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> bounded(mr1,g)(\n. inv(x n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 493 NET_NULL_ADD = @@ -19578,7 +19614,7 @@ (!x y. bounded(mr1,g)x /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) * (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 484 Theorem REAL_LT_LMUL autoloading from theory `REAL` ... @@ -19780,7 +19816,7 @@ (y --> y0)(mtop mr1,g) /\ (?N. g N N /\ (!n. g n N ==> (x n) <= (y n))) ==> x0 <= y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 400 () : void @@ -19790,7 +19826,7 @@ File nets.ml loaded () : void -Run time: 0.5s +Run time: 1.4s Intermediate theorems generated: 7389 #\ @@ -19800,7 +19836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -19874,7 +19910,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s real_interface_map = [(`--`, `real_neg`); @@ -19905,7 +19941,7 @@ Intermediate theorems generated: 34 () : void -Run time: 0.1s +Run time: 0.0s [(); ()] : void list Run time: 0.0s @@ -20146,7 +20182,7 @@ Theorem LESS_EQUAL_ADD autoloading from theory `arithmetic` ... LESS_EQUAL_ADD = |- !m n. m num_le n ==> (?p. n = m num_add p) -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... LESS_EQ_SUC_REFL = |- !m. m num_le (SUC m) @@ -20159,7 +20195,7 @@ MONO_SUC = |- !f. mono f = (!n. (f(SUC n)) >= (f n)) \/ (!n. (f(SUC n)) <= (f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 528 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -20276,7 +20312,7 @@ Theorem REAL_ADD_RINV autoloading from theory `REAL` ... REAL_ADD_RINV = |- !x. x + (-- x) = & 0 -Run time: 0.0s +Run time: 0.1s Definition real_sub autoloading from theory `REAL` ... real_sub = |- !x y. x - y = x + (-- y) @@ -20314,7 +20350,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` ... @@ -20423,7 +20459,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20441,7 +20477,7 @@ |- !f g l m. f --> l /\ g --> m /\ (?N. !n. n num_ge N ==> (f n) <= (g n)) ==> l <= m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 Theorem LESS_0 autoloading from theory `prim_rec` ... @@ -20507,7 +20543,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` ... @@ -20568,7 +20604,7 @@ Run time: 0.0s SEQ_POWER_ABS = |- !c. (abs c) < (& 1) ==> (\n. (abs c) pow n) --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 573 Theorem POW_ABS autoloading from theory `REAL` ... @@ -20605,7 +20641,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.0s +Run time: 0.2s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20693,7 +20729,7 @@ Theorem REAL_INJ autoloading from theory `REAL` ... REAL_INJ = |- !m n. (& m = & n) = (m = n) -Run time: 0.1s +Run time: 0.0s Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... REAL_DIV_LMUL = |- !x y. ~(y = & 0) ==> (y * (x / y) = x) @@ -20736,11 +20772,11 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.0s +Run time: 0.2s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 summable = |- !f. summable f = (?s. f sums s) @@ -20839,7 +20875,7 @@ |- !f k. summable f /\ 0 num_lt k ==> (\n. Sum(n num_mul k,k)f) sums (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 258 Theorem MULT_SYM autoloading from theory `arithmetic` ... @@ -20891,7 +20927,7 @@ SER_ADD = |- !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. (x n) + (y n)) sums (x0 + y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 Theorem SUM_CMUL autoloading from theory `REAL` ... @@ -20928,7 +20964,7 @@ |- !f. summable f = (!e. (& 0) < e ==> (?N. !m n. m num_ge N ==> (abs(Sum(m,n)f)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) @@ -20950,14 +20986,14 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 SER_COMPARA = |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable(\k. abs(f k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 41 Theorem ZERO_LESS_EQ autoloading from theory `arithmetic` ... @@ -20994,7 +21030,7 @@ SER_ABS = |- !f. summable(\n. abs(f n)) ==> (abs(suminf f)) <= (suminf(\n. abs(f n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 92 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -21037,7 +21073,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` ... @@ -21074,7 +21110,7 @@ c < (& 1) /\ (!n. n num_ge N ==> (abs(f(SUC n))) <= (c * (abs(f n)))) ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 683 () : void @@ -21084,7 +21120,7 @@ File seq.ml loaded () : void -Run time: 1.0s +Run time: 2.8s Intermediate theorems generated: 18704 #\ @@ -21094,7 +21130,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -21196,7 +21232,7 @@ Intermediate theorems generated: 43 () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -21383,7 +21419,7 @@ |- !f g l m. (f --> l)x /\ (g --> m)x /\ ~(m = & 0) ==> ((\x. (f x) / (g x)) --> (l / m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 42 Theorem NET_NULL autoloading from theory `NETS` ... @@ -21416,7 +21452,7 @@ LIM_EQUAL = |- !f g l x0. (!x. ~(x = x0) ==> (f x = g x)) ==> ((f --> l)x0 = (g --> l)x0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 171 Theorem REAL_LT_TRANS autoloading from theory `REAL` ... @@ -21598,7 +21634,7 @@ Theorem REAL_LT_01 autoloading from theory `REAL` ... REAL_LT_01 = |- (& 0) < (& 1) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE_TRANS autoloading from theory `REAL` ... REAL_LE_TRANS = |- !x y z. x <= y /\ y <= z ==> x <= z @@ -21624,7 +21660,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.0s +Run time: 0.2s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21658,7 +21694,7 @@ Run time: 0.0s DIFF_CONST = |- !k x. ((\x. k) diffl (& 0))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 59 Theorem REAL_RDISTRIB autoloading from theory `REAL` ... @@ -21686,7 +21722,7 @@ Theorem REAL_SUB_RDISTRIB autoloading from theory `REAL` ... REAL_SUB_RDISTRIB = |- !x y z. (x - y) * z = (x * z) - (y * z) -Run time: 0.0s +Run time: 0.1s Theorem REAL_SUB_LDISTRIB autoloading from theory `REAL` ... REAL_SUB_LDISTRIB = |- !x y z. x * (y - z) = (x * y) - (x * z) @@ -21728,7 +21764,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) - (g x)) diffl (l - m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 50 Theorem NET_NULL_MUL autoloading from theory `NETS` ... @@ -21786,7 +21822,7 @@ ((f(g(x + h))) - (f(g x))) / h = (((f(g(x + h))) - (f(g x))) / ((g(x + h)) - (g x))) * (((g(x + h)) - (g x)) / h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 170 Theorem REAL_LT_RADD autoloading from theory `REAL` ... @@ -21794,7 +21830,7 @@ Run time: 0.0s CHAIN_LEMMA2 = |- !x y d. (abs(x - y)) < d ==> (abs x) < ((abs y) + d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 65 Theorem ABS_POS autoloading from theory `REAL` ... @@ -21824,7 +21860,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.0s +Run time: 0.2s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21832,7 +21868,7 @@ Run time: 0.0s DIFF_X = |- !x. ((\x. x) diffl (& 1))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 Theorem REAL_MUL_RID autoloading from theory `REAL` ... @@ -21845,7 +21881,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.1s +Run time: 0.0s Theorem ADD_SUB autoloading from theory `arithmetic` ... ADD_SUB = |- !a c. (a num_add c) num_sub c = a @@ -21887,7 +21923,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_ENTIRE autoloading from theory `REAL` ... REAL_ENTIRE = |- !x y. (x * y = & 0) = (x = & 0) \/ (y = & 0) @@ -21940,7 +21976,7 @@ ((\x. (f x) / (g x)) diffl (((l * (g x)) - (m * (f x))) / ((g x) pow 2))) x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 293 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -21974,14 +22010,14 @@ m num_le r /\ r num_lt (m num_add n) ==> ((\x'. f r x') diffl (f' r x))x) ==> ((\x'. Sum(m,n)(\n'. f n' x')) diffl (Sum(m,n)(\r. f' r x)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 301 CONT_BOUNDED = |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22038,7 +22074,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22047,7 +22083,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -22113,7 +22149,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f x) <= (f y))) ==> (l = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 88 DIFF_LCONST = @@ -22164,7 +22200,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -22178,7 +22214,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22187,7 +22223,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.1s +Run time: 0.0s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -22196,7 +22232,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (!x. a <= x /\ x <= b ==> (f x = f a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 310 DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) @@ -22210,7 +22246,7 @@ File lim.ml loaded () : void -Run time: 1.1s +Run time: 3.0s Intermediate theorems generated: 21608 #\ @@ -22220,7 +22256,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -22325,11 +22361,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22353,7 +22389,7 @@ Theorem LESS_THM autoloading from theory `prim_rec` ... LESS_THM = |- !m n. m num_lt (SUC n) = (m = n) \/ m num_lt n -Run time: 0.0s +Run time: 0.1s Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m @@ -22503,7 +22539,7 @@ Theorem REAL_LT_1 autoloading from theory `REAL` ... REAL_LT_1 = |- !x y. (& 0) <= x /\ x < y ==> (x / y) < (& 1) -Run time: 0.0s +Run time: 0.1s Theorem REAL_NOT_LT autoloading from theory `REAL` ... REAL_NOT_LT = |- !x y. ~x < y = y <= x @@ -22626,7 +22662,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (f n) * (z pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 67 diffs = |- !c. diffs c = (\n. (&(SUC n)) * (c(SUC n))) @@ -22698,7 +22734,7 @@ summable(\n. (diffs c n) * (x pow n)) ==> (\n. (& n) * ((c n) * (x pow (n num_sub 1)))) sums (suminf(\n. (diffs c n) * (x pow n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 180 Theorem SUB_ADD autoloading from theory `arithmetic` ... @@ -22791,7 +22827,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -22876,7 +22912,7 @@ Theorem REAL_LT_LMUL autoloading from theory `REAL` ... REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_TRANS autoloading from theory `REAL` ... REAL_LT_TRANS = |- !x y z. x < y /\ y < z ==> x < z @@ -22956,7 +22992,7 @@ Theorem SUM_SUMMABLE autoloading from theory `SEQ` ... SUM_SUMMABLE = |- !f l. f sums l ==> summable f -Run time: 0.0s +Run time: 0.1s Theorem SUM_UNIQ autoloading from theory `SEQ` ... SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) @@ -23072,7 +23108,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 2494 () : void @@ -23082,7 +23118,7 @@ File powser.ml loaded () : void -Run time: 0.5s +Run time: 1.5s Intermediate theorems generated: 8507 #\ @@ -23092,7 +23128,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -23167,7 +23203,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s false : bool Run time: 0.0s @@ -23178,7 +23214,7 @@ Theory POWSER loaded () : void -Run time: 0.1s +Run time: 0.2s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -23510,7 +23546,7 @@ Theorem REAL_LT autoloading from theory `REAL` ... REAL_LT = |- !m n. (& m) < (& n) = m num_lt n -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... REAL_LT_IMP_NE = |- !x y. x < y ==> ~(x = y) @@ -23531,7 +23567,7 @@ Theorem REAL_MUL_LID autoloading from theory `REAL` ... REAL_MUL_LID = |- !x. (& 1) * x = x -Run time: 0.1s +Run time: 0.0s Theorem POW_M1 autoloading from theory `REAL` ... POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 @@ -23583,7 +23619,7 @@ ((\n. (EVEN n => ((--(& 1)) pow (n DIV 2)) / (&(FACT n)) | & 0))n) * (x pow n)) sums (cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 272 Theorem REAL_MUL_RINV autoloading from theory `REAL` ... @@ -23648,7 +23684,7 @@ & 0 | ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 407 Theorem SER_NEG autoloading from theory `SEQ` ... @@ -23711,7 +23747,7 @@ Run time: 0.0s DIFF_COS = |- !x. (cos diffl (--(sin x)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 283 [|- !x. (exp diffl (exp x))x; @@ -23792,7 +23828,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) @@ -23821,7 +23857,7 @@ Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 EXP_NEG_MUL2 = |- !x. (exp(-- x)) * (exp x) = & 1 @@ -23934,7 +23970,7 @@ Theorem REAL_SUB_LE autoloading from theory `REAL` ... REAL_SUB_LE = |- !x y. (& 0) <= (x - y) = y <= x -Run time: 0.1s +Run time: 0.0s Theorem REAL_LE_SUB_LADD autoloading from theory `REAL` ... REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y @@ -23976,7 +24012,7 @@ Intermediate theorems generated: 2 LN_EXP = |- !x. ln(exp x) = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 52 EXP_LN = |- !x. (exp(ln x) = x) = (& 0) < x @@ -24023,7 +24059,7 @@ LN_MONO_LE = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x) <= (ln y) = x <= y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 LN_POW = |- !n x. (& 0) < x ==> (ln(x pow n) = (& n) * (ln x)) @@ -24055,14 +24091,14 @@ Theorem REAL_ENTIRE autoloading from theory `REAL` ... REAL_ENTIRE = |- !x y. (x * y = & 0) = (x = & 0) \/ (y = & 0) -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT_REFL autoloading from theory `REAL` ... REAL_LT_REFL = |- !x. ~x < x Run time: 0.0s ROOT_0 = |- !n. root(SUC n)(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 209 Theorem REAL_DIV_LZERO autoloading from theory `REAL` ... @@ -24098,7 +24134,7 @@ Run time: 0.0s SIN_0 = |- sin(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -24116,7 +24152,7 @@ Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 690 Theorem REAL_ADD_RINV autoloading from theory `REAL` ... @@ -24141,7 +24177,7 @@ Theorem REAL_POW2_ABS autoloading from theory `REAL` ... REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT1_POW2 autoloading from theory `REAL` ... REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) @@ -24168,7 +24204,7 @@ Run time: 0.0s COS_BOUND = |- !x. (abs(cos x)) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 160 COS_BOUNDS = |- !x. (--(& 1)) <= (cos x) /\ (cos x) <= (& 1) @@ -24204,14 +24240,14 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1747 SIN_COS_NEG = |- !x. (((sin(-- x)) + (sin x)) pow 2) + (((cos(-- x)) - (cos x)) pow 2) = & 0 -Run time: 0.0s +Run time: 0.2s Intermediate theorems generated: 1099 Theorem REAL_SUMSQ autoloading from theory `REAL` ... @@ -24245,7 +24281,7 @@ Run time: 0.0s SIN_DOUBLE = |- !x. sin((& 2) * x) = (& 2) * ((sin x) * (cos x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 COS_DOUBLE = |- !x. cos((& 2) * x) = ((cos x) pow 2) - ((sin x) pow 2) @@ -24321,7 +24357,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24361,7 +24397,7 @@ Run time: 0.0s COS_2 = |- (cos(& 2)) < (& 0) -Run time: 0.1s +Run time: 0.3s Intermediate theorems generated: 3794 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -24409,11 +24445,11 @@ Run time: 0.0s COS_ISZERO = |- ?! x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 PI2 = |- pi / (& 2) = (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24433,7 +24469,7 @@ Run time: 0.0s PI_POS = |- (& 0) < pi -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 31 Theorem REAL_LT_GT autoloading from theory `REAL` ... @@ -24485,7 +24521,7 @@ Intermediate theorems generated: 47 COS_NPI = |- !n. cos((& n) * pi) = (--(& 1)) pow n -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 134 SIN_NPI = |- !n. sin((& n) * pi) = & 0 @@ -24497,7 +24533,7 @@ Intermediate theorems generated: 53 COS_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 450 Theorem REAL_LT_NEG autoloading from theory `REAL` ... @@ -24621,7 +24657,7 @@ (cos x = & 0) = (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. ~EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 630 Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... @@ -24649,7 +24685,7 @@ Intermediate theorems generated: 19 TAN_PI = |- tan pi = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 TAN_NPI = |- !n. tan((& n) * pi) = & 0 @@ -24661,7 +24697,7 @@ Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 Theorem REAL_LDISTRIB autoloading from theory `REAL` ... @@ -24681,7 +24717,7 @@ |- !x y. ~(cos x = & 0) /\ ~(cos y = & 0) /\ ~(cos(x + y) = & 0) ==> (tan(x + y) = ((tan x) + (tan y)) / ((& 1) - ((tan x) * (tan y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 869 TAN_DOUBLE = @@ -24692,7 +24728,7 @@ Intermediate theorems generated: 68 TAN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (tan x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 78 Theorem REAL_INV_1OVER autoloading from theory `REAL` ... @@ -24784,7 +24820,7 @@ Intermediate theorems generated: 2 acs = |- !y. acs y = (@x. (& 0) <= x /\ x <= pi /\ (cos x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 atn = @@ -24816,7 +24852,7 @@ SIN_ASN = |- !x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) ==> (asn(sin x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 86 ACS = @@ -24833,11 +24869,11 @@ ACS_BOUNDS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 COS_ACS = |- !x. (& 0) <= x /\ x <= pi ==> (acs(cos x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 86 ATN = @@ -24858,7 +24894,7 @@ TAN_ATN = |- !x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) ==> (atn(tan x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 () : void @@ -24868,7 +24904,7 @@ File transc.ml loaded () : void -Run time: 1.8s +Run time: 4.8s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24881,7 +24917,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -24903,7 +24939,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -24969,7 +25005,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25001,7 +25037,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25110,7 +25146,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25263,7 +25299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25336,7 +25372,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25416,7 +25452,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25573,7 +25609,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25728,7 +25764,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25945,7 +25981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25967,7 +26003,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -25986,7 +26022,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26031,7 +26067,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26096,7 +26132,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26146,7 +26182,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26216,7 +26252,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26286,7 +26322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26322,7 +26358,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26375,7 +26411,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26447,7 +26483,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26526,7 +26562,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26721,7 +26757,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -26758,7 +26794,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -27444,7 +27480,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -27916,7 +27952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -28180,7 +28216,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -28425,7 +28461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -28889,7 +28925,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29357,7 +29393,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29413,7 +29449,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29503,7 +29539,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29702,7 +29738,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29734,7 +29770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -29868,7 +29904,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30171,7 +30207,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30203,7 +30239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30242,7 +30278,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30274,7 +30310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30435,7 +30471,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30568,7 +30604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30757,7 +30793,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30817,7 +30853,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -30942,7 +30978,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31053,7 +31089,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31078,7 +31114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31106,7 +31142,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31219,7 +31255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31722,7 +31758,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -31970,7 +32006,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32196,7 +32232,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32238,7 +32274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32270,7 +32306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32493,7 +32529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32886,7 +32922,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -32999,7 +33035,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -33502,7 +33538,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -33750,7 +33786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -33976,7 +34012,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34011,7 +34047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34050,7 +34086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34087,7 +34123,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34108,7 +34144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34205,7 +34241,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34227,7 +34263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34723,7 +34759,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34746,7 +34782,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34824,7 +34860,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34883,7 +34919,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34927,7 +34963,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34945,7 +34981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -34972,7 +35008,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35016,7 +35052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35129,7 +35165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35176,7 +35212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35215,7 +35251,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35289,7 +35325,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35378,7 +35414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35449,7 +35485,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35519,7 +35555,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35568,7 +35604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35609,7 +35645,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35650,7 +35686,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35674,7 +35710,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35775,7 +35811,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35796,7 +35832,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -35821,7 +35857,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36447,7 +36483,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36524,7 +36560,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36551,7 +36587,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36668,7 +36704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36763,7 +36799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36849,7 +36885,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -36964,7 +37000,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37057,7 +37093,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37233,7 +37269,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37337,7 +37373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37632,7 +37668,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37735,7 +37771,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37803,7 +37839,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -37865,7 +37901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -38045,7 +38081,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -38086,7 +38122,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -38116,7 +38152,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -38142,7 +38178,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -38660,7 +38696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -39197,7 +39233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -39385,7 +39421,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 12/4/24 + HOL88 Version 2.02 (GCL), built on 13/4/24 =============================================================================== #false : bool @@ -39403,10 +39439,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Fri Apr 12 12:44:05 -12 2024 +Sat Apr 13 15:51:50 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 12 12:44:05 -12 2024 +Sat Apr 13 15:51:50 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39424,22 +39460,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 12/4/24 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 13/4/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 12/4/24 +BASIC-HOL version 2.02 (GCL) created 13/4/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 12/4/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 13/4/24 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41177,7 +41213,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' @@ -42942,7 +42978,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' @@ -44685,7 +44721,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' @@ -44939,7 +44975,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' @@ -45175,7 +45211,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' @@ -45352,7 +45388,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' @@ -45540,7 +45576,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' @@ -45658,7 +45694,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' @@ -45773,7 +45809,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' @@ -46012,7 +46048,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' @@ -46352,7 +46388,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' @@ -46558,7 +46594,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' @@ -46900,7 +46936,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' @@ -47091,7 +47127,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' @@ -47358,7 +47394,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' @@ -47518,7 +47554,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' @@ -47662,7 +47698,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' @@ -47813,7 +47849,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' @@ -47968,7 +48004,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' @@ -48145,7 +48181,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' @@ -48340,7 +48376,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' @@ -48564,7 +48600,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' @@ -48824,7 +48860,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.04.12:1248' -> endpages.ps +' TeX output 2024.04.13:1602' -> endpages.ps @@ -48888,7 +48924,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.04.12:1248' -> titlepages.ps +' TeX output 2024.04.13:1602' -> titlepages.ps @@ -48963,8 +48999,8 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_armhf.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_armhf.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_armhf.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install find ml -type f -name "*ml" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install @@ -49011,10 +49047,12 @@ dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_fixperms dh_makeshlibs dh_installdeb @@ -49023,16 +49061,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-doc' in '../hol88-doc_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-source' in '../hol88-source_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-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-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 @@ -49042,12 +49081,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/4610/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/4610/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/1106 and its subdirectories -I: Current time: Fri Apr 12 12:49:26 -12 2024 -I: pbuilder-time-stamp: 1712969366 +I: removing directory /srv/workspace/pbuilder/4610 and its subdirectories +I: Current time: Sat Apr 13 16:05:49 +14 2024 +I: pbuilder-time-stamp: 1712973949