Diff of the two buildlogs: -- --- b1/build.log 2024-01-07 02:26:23.087146865 +0000 +++ b2/build.log 2024-01-07 04:11:01.116894567 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Jan 6 11:53:47 -12 2024 -I: pbuilder-time-stamp: 1704585227 +I: Current time: Sun Jan 7 16:27:57 +14 2024 +I: pbuilder-time-stamp: 1704594477 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bullseye-reproducible-base.tgz] I: copying local configuration @@ -17,7 +17,7 @@ I: copying [./hol88_2.02.19940316-35.1.debian.tar.xz] I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' -gpgv: keyblock resource '/tmp/dpkg-verify-sig.OdBHDQwW/trustedkeys.kbx': General error +gpgv: keyblock resource '/tmp/dpkg-verify-sig.RoxRGyNY/trustedkeys.kbx': General error gpgv: Signature made Tue Jan 5 11:49:56 2021 gpgv: using RSA key B8BF54137B09D35CF026FE9D091AB856069AAA1C gpgv: Can't check signature: No public key @@ -30,49 +30,80 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/24521/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/26855/tmp/hooks/D01_modify_environment starting +debug: Running on ff64a. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Jan 7 02:29 /bin/sh -> /bin/bash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/26855/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/26855/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,-fixfilepath parallel=3 ' - DISTRIBUTION='bullseye' - HOME='/root' - HOST_ARCH='armhf' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="1" [2]="4" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.1.4(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,-fixfilepath parallel=6 ' + DIRSTACK=() + DISTRIBUTION=bullseye + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='8ace2f88de4f488f8f550c12306c0845' - 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='24521' - PS1='# ' - PS2='> ' + INVOCATION_ID=656c960fde1b411dab84be9a84c84d2e + 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=26855 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.Q1RRxT31/pbuilderrc_Hhq6 --distribution bullseye --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.Q1RRxT31/b1 --logfile b1/build.log hol88_2.02.19940316-35.1.dsc' - SUDO_GID='116' - SUDO_UID='112' - 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.Q1RRxT31/pbuilderrc_WVbl --distribution bullseye --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.Q1RRxT31/b2 --logfile b2/build.log hol88_2.02.19940316-35.1.dsc' + SUDO_GID=114 + SUDO_UID=109 + 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 cbxi4b 6.1.0-17-armmp #1 SMP Debian 6.1.69-1 (2023-12-30) armv7l GNU/Linux + Linux i-capture-the-hostname 6.1.0-17-arm64 #1 SMP Debian 6.1.69-1 (2023-12-30) aarch64 GNU/Linux I: ls -l /bin total 3580 -rwxr-xr-x 1 root root 816764 Mar 27 2022 bash @@ -132,7 +163,7 @@ -rwxr-xr-x 1 root root 30732 Sep 22 2020 rmdir -rwxr-xr-x 1 root root 14144 Sep 27 2020 run-parts -rwxr-xr-x 1 root root 76012 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Dec 7 09:28 sh -> dash + lrwxrwxrwx 1 root root 9 Jan 7 02:29 sh -> /bin/bash -rwxr-xr-x 1 root root 22532 Sep 22 2020 sleep -rwxr-xr-x 1 root root 55360 Sep 22 2020 stty -rwsr-xr-x 1 root root 46704 Jan 20 2022 su @@ -158,7 +189,7 @@ -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew -I: user script /srv/workspace/pbuilder/24521/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/26855/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -334,7 +365,7 @@ Get: 126 http://deb.debian.org/debian bullseye/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 127 http://deb.debian.org/debian bullseye/main armhf texlive-base all 2020.20210202-3 [20.8 MB] Get: 128 http://deb.debian.org/debian bullseye/main armhf texlive-latex-base all 2020.20210202-3 [1120 kB] -Fetched 123 MB in 31s (3946 kB/s) +Fetched 123 MB in 11s (11.4 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package bsdextrautils. (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 ... 17486 files and directories currently installed.) @@ -756,8 +787,8 @@ Setting up tzdata (2021a-1+deb11u10) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Jan 7 00:00:51 UTC 2024. -Universal Time is now: Sun Jan 7 00:00:51 UTC 2024. +Local time is now: Sun Jan 7 02:32:31 UTC 2024. +Universal Time is now: Sun Jan 7 02:32:31 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up xtrans-dev (1.4.0-1) ... @@ -936,7 +967,11 @@ fakeroot is already the newest version (1.25.3-1.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.19940316/ && 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.19940316-35.1_source.changes +I: user script /srv/workspace/pbuilder/26855/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bullseye +I: user script /srv/workspace/pbuilder/26855/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316/ && 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.19940316-35.1_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316-35.1 dpkg-buildpackage: info: source distribution unstable @@ -1190,56 +1225,59 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/window/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ @@ -1247,41 +1285,38 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/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.19940316/Library/numeral/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/abs_theory/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/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 \ @@ -1329,7 +1364,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:10:13 -12 2024 +Sun Jan 7 16:39:27 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2503,7 +2538,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 # mem = - : (* -> * list -> bool) @@ -2641,7 +2676,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #.............start address -T 0x887cb0 () : void @@ -2800,7 +2835,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #.............start address -T 0x887cb0 () : void @@ -2992,7 +3027,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 # concat = - : (string -> string -> string) @@ -3102,7 +3137,7 @@ start address -T 0x882c20 ;; Finished loading "lisp/f-ol-net" start address -T 0x84fb68 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 6/1/24 + version 2.02 (GCL) created 7/1/24 #...start address -T 0x889de8 () : void @@ -3415,7 +3450,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 ###########################() : void @@ -3428,7 +3463,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 ################################################################################################() : void @@ -3573,7 +3608,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 ############################() : void @@ -3616,7 +3651,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 ############################Theory ind loaded () : void @@ -3653,7 +3688,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3694,7 +3729,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4096,7 +4131,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4164,7 +4199,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4369,7 +4404,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4493,7 +4528,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4579,7 +4614,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4672,7 +4707,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4741,7 +4776,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -4846,7 +4881,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5081,7 +5116,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5107,7 +5142,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5235,7 +5270,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5283,7 +5318,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5350,7 +5385,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5409,7 +5444,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5465,7 +5500,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5478,7 +5513,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 7/1/24 #() : void @@ -5530,7 +5565,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ##########################() : void @@ -5561,7 +5596,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ##############################() : void @@ -5648,7 +5683,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #######################################################################() : void @@ -5801,7 +5836,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ###########################() : void @@ -5836,7 +5871,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #############################() : void @@ -5897,7 +5932,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ###########################Theory arithmetic loaded () : void @@ -6392,7 +6427,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ##################################() : void @@ -6539,7 +6574,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #################################Theory list loaded () : void @@ -6878,7 +6913,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ###############################Theory list loaded () : void @@ -8375,7 +8410,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #############################() : void @@ -8759,7 +8794,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ############################() : void @@ -9057,7 +9092,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ############################() : void @@ -9197,7 +9232,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ############################################() : void @@ -9294,7 +9329,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 ##################################() : void @@ -9324,7 +9359,7 @@ | /build/reproducible-path/hol88-2.02.19940316/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -9341,7 +9376,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #Theory num loaded () : void @@ -9360,7 +9395,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -9517,7 +9552,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 # @@ -9555,7 +9590,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 # @@ -9589,7 +9624,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -9674,7 +9709,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -9715,7 +9750,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -9899,7 +9934,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 # define_load_lib_function = - : (string list -> void -> void) @@ -9973,7 +10008,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -9986,7 +10021,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #() : void @@ -10050,11 +10085,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:48:59 -12 2024 +Sun Jan 7 16:59:48 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:49:02 -12 2024 +Sun Jan 7 16:59:49 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10077,7 +10112,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -10161,7 +10196,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -10267,7 +10302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11017,7 +11052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11040,7 +11075,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11083,7 +11118,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11119,7 +11154,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11171,7 +11206,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11203,7 +11238,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11241,7 +11276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11269,7 +11304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11346,7 +11381,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11368,7 +11403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11422,7 +11457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11471,7 +11506,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11622,7 +11657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11666,7 +11701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11741,7 +11776,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11791,7 +11826,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11854,7 +11889,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11907,7 +11942,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -11953,7 +11988,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12041,7 +12076,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12079,7 +12114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12140,7 +12175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12204,7 +12239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12230,7 +12265,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12255,7 +12290,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12294,7 +12329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -12370,7 +12405,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13107,7 +13142,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13130,7 +13165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13173,7 +13208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13208,7 +13243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13249,7 +13284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13312,7 +13347,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13335,7 +13370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13360,7 +13395,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13387,7 +13422,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13423,7 +13458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13955,7 +13990,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -13978,7 +14013,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14012,7 +14047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14067,7 +14102,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14158,7 +14193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14327,7 +14362,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14380,7 +14415,7 @@ Intermediate theorems generated: 2 Union = |- !P. wo_Union P = (\x. ?p. P p /\ p x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 fl = |- !l x. wo_fl l x = (?y. l(x,y) \/ l(y,x)) @@ -14393,7 +14428,7 @@ (!x. wo_fl l x ==> l(x,x)) /\ (!x y z. l(x,y) /\ l(y,z) ==> l(x,z)) /\ (!x y. l(x,y) /\ l(y,x) ==> (x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 chain = |- !l P. wo_chain l P = (!x y. P x /\ P y ==> l(x,y) \/ l(y,x)) @@ -14436,11 +14471,11 @@ Intermediate theorems generated: 22 SUBSET_ANTISYM = |- !P Q. P subset Q /\ Q subset P ==> (P = Q) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 SUBSET_TRANS = |- !P Q R. P subset Q /\ Q subset R ==> P subset R -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 POSET_REFL = |- !l. poset l ==> (!x. fl l x ==> l(x,x)) @@ -14491,7 +14526,7 @@ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. P z ==> l(y,z)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1294 PAIRED_EXT = |- !l m. (!x y. l(x,y) = m(x,y)) = (l = m) @@ -14535,14 +14570,14 @@ |- !l. woset l ==> (!x y. fl l x /\ fl l y ==> (x = y) \/ less l(x,y) \/ less l(y,x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 172 WO_INDUCT = |- !P l. woset l /\ (!x. fl l x /\ (!y. less l(y,x) ==> P y) ==> P x) ==> (!x. fl l x ==> P x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 469 WO_INDUCT_TAC = - : tactic @@ -14570,7 +14605,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.2s +Run time: 0.1s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14580,7 +14615,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (?f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 444 WO_RECURSE = @@ -14611,10 +14646,10 @@ Theorem LESS_EQUAL_ANTISYM autoloading from theory `arithmetic` ... LESS_EQUAL_ANTISYM = |- !n m. n <= m /\ m <= n ==> (n = m) -Run time: 0.1s +Run time: 0.0s WOSET_NUM = |- woset(\(m,n). m <= n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 Theorem LESS_NOT_EQ autoloading from theory `prim_rec` ... @@ -14630,11 +14665,11 @@ |- !h ms. (!f g x. (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 170 UNION_INSEG = |- !P l. (!m. P m ==> m inseg l) ==> (Union P) inseg l @@ -14642,15 +14677,15 @@ Intermediate theorems generated: 232 INSEG_SUBSET = |- !l m. m inseg l ==> (!x y. m(x,y) ==> l(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -14667,19 +14702,19 @@ INSEG_PROPER_SUBSET = |- !l m. m inseg l /\ ~(l = m) ==> (?x y. l(x,y) /\ ~m(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 213 INSEG_PROPER_SUBSET_FL = |- !l m. m inseg l /\ ~(l = m) ==> (?a. fl l a /\ ~fl m a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 107 INSEG_LINSEG = |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 1172 EXTEND_FL = @@ -14718,16 +14753,16 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.1s +Run time: 0.3s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = |- !l x. ordinal l ==> fl l x ==> fl(Union ordinal)x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 ORDINAL_UP = @@ -14747,21 +14782,21 @@ Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 403 HP = |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 2506 ZL = |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -14784,13 +14819,13 @@ Intermediate theorems generated: 1083 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File mk_wellorder loaded () : void -Run time: 3.0s +Run time: 3.6s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder' @@ -14799,7 +14834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14901,7 +14936,7 @@ IDENTITY_UNIQUE = . |- !f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 36 . |- !f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m) @@ -14923,14 +14958,14 @@ File ../../Library/abs_theory/monoid_def.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 614 Making ../../Library/abs_theory/group_def.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -14975,7 +15010,7 @@ Intermediate theorems generated: 601 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 GROUP_EXTENDS_MONOID = ... |- IS_MONOID(monoid(fn g)(id g)) @@ -15015,14 +15050,14 @@ File ../../Library/abs_theory/group_def.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 1089 Making ../../Library/abs_theory/example.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -15072,7 +15107,7 @@ Run time: 0.0s GROUP_THOBS = |- IS_GROUP(group(\x y. ~(x = y))F I) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f @@ -15080,7 +15115,7 @@ Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 732 |- !a. I(I a) = a @@ -15101,7 +15136,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.2s +Run time: 0.4s Intermediate theorems generated: 2546 () : void @@ -15111,15 +15146,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.7s +Run time: 1.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Jan 6 13:01:45 -12 2024 +===> abs_theory rebuilt on Sun Jan 7 17:08:35 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -15292,7 +15327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -15387,7 +15422,7 @@ (m + 0 = m) /\ ((SUC m) + n = SUC(m + n)) /\ (m + (SUC n) = SUC(m + n)) -Run time: 0.0s +Run time: 0.1s Theorem MULT_CLAUSES autoloading from theory `arithmetic` ... MULT_CLAUSES = @@ -15398,7 +15433,7 @@ (m * 1 = m) /\ ((SUC m) * n = (m * n) + n) /\ (m * (SUC n) = m + (m * n)) -Run time: 0.1s +Run time: 0.0s Theorem PRE autoloading from theory `prim_rec` ... PRE = |- (PRE 0 = 0) /\ (!m. PRE(SUC m) = m) @@ -15456,7 +15491,7 @@ Intermediate theorems generated: 22 TRAT_EQ_SYM = |- !p q. p trat_eq q = q trat_eq p -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 37 Theorem MULT_ASSOC autoloading from theory `arithmetic` ... @@ -15476,7 +15511,7 @@ Intermediate theorems generated: 152 TRAT_EQ_AP = |- !p q. (p = q) ==> p trat_eq q -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 8 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -15502,7 +15537,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 = @@ -15530,12 +15565,12 @@ Theorem ADD_ASSOC autoloading from theory `arithmetic` ... ADD_ASSOC = |- !m n p. m + (n + p) = (m + n) + p -Run time: 0.0s +Run time: 0.1s TRAT_ADD_ASSOC = |- !h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -15572,7 +15607,7 @@ Run time: 0.0s TRAT_NOZERO = |- !h i. ~(h trat_add i) trat_eq h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... @@ -15585,18 +15620,18 @@ Theorem LESS_LESS_CASES autoloading from theory `arithmetic` ... LESS_LESS_CASES = |- !m n. (m = n) \/ m < n \/ n < m -Run time: 0.0s +Run time: 0.1s TRAT_ADD_TOTAL = |- !h i. h trat_eq i \/ (?d. h trat_eq (i trat_add d)) \/ (?d. i trat_eq (h trat_add d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 233 Theorem LESS_ADD_NONZERO autoloading from theory `arithmetic` ... @@ -15628,13 +15663,13 @@ Run time: 0.0s TRAT_ARCH = |- !h. ?n d. (trat_sucint n) trat_eq (h trat_add d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 TRAT_SUCINT = |- (trat_sucint 0) trat_eq trat_1 /\ (!n. (trat_sucint(SUC n)) trat_eq ((trat_sucint n) trat_add trat_1)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 37 TRAT_EQ_EQUIV = |- !p q. p trat_eq q = ($trat_eq p = $trat_eq q) @@ -15659,7 +15694,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -15687,7 +15722,7 @@ Intermediate theorems generated: 7 HRAT_MUL_LID = |- !h. hrat_1 hrat_mul h = h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3 HRAT_MUL_LINV = |- !h. (hrat_inv h) hrat_mul h = hrat_1 @@ -15695,7 +15730,7 @@ Intermediate theorems generated: 3 HRAT_NOZERO = |- !h i. ~(h hrat_add i = h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 5 HRAT_ADD_TOTAL = @@ -15719,7 +15754,7 @@ File hrat.ml loaded () : void -Run time: 1.6s +Run time: 1.9s Intermediate theorems generated: 11032 #\ @@ -15729,7 +15764,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -15887,7 +15922,7 @@ Intermediate theorems generated: 19 HRAT_LT_GT = |- !x y. x hrat_lt y ==> ~y hrat_lt x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 78 HRAT_LT_NE = |- !x y. x hrat_lt y ==> ~(x = y) @@ -15920,7 +15955,7 @@ HRAT_LT_RADD = |- !x y z. (x hrat_add z) hrat_lt (y hrat_add z) = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 21 HRAT_LT_MUL2 = @@ -16039,7 +16074,7 @@ Intermediate theorems generated: 37 CUT_DOWN = |- !X x y. cut X x /\ y hrat_lt x ==> cut X y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 49 CUT_UP = |- !X x. cut X x ==> (?y. cut X y /\ x hrat_lt y) @@ -16070,7 +16105,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.0s +Run time: 0.1s Theorem HRAT_ARCH autoloading from theory `HRAT` ... HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16082,7 +16117,7 @@ CUT_NEARTOP_MUL = |- !X u. hrat_1 hrat_lt u ==> (?x. cut X x /\ ~cut X(u hrat_mul x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 234 hreal_1 = |- hreal_1 = hreal(cut_of_hrat hrat_1) @@ -16109,7 +16144,7 @@ hreal (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 hreal_sup = |- !P. hreal_sup P = hreal(\w. ?X. P X /\ cut X w) @@ -16164,15 +16199,15 @@ Intermediate theorems generated: 935 HREAL_MUL_LID = |- !X. hreal_1 hreal_mul X = X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 155 hreal_sub = @@ -16181,22 +16216,22 @@ Intermediate theorems generated: 2 HREAL_LT_LEMMA = |- !X Y. X hreal_lt Y ==> (?x. ~cut X x /\ cut Y x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 210 HREAL_SUB_ISACUT = |- !X Y. X hreal_lt Y ==> isacut(\w. ?x. ~cut X x /\ cut Y(x hrat_add w)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 400 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 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 492 HREAL_LT = |- !X Y. X hreal_lt Y = (?D. Y = X hreal_add D) @@ -16205,14 +16240,14 @@ HREAL_ADD_TOTAL = |- !X Y. (X = Y) \/ (?D. Y = X hreal_add D) \/ (?D. X = Y hreal_add D) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 HREAL_SUP_ISACUT = |- !P. (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==> isacut(\w. ?X. P X /\ cut X w) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 349 HREAL_SUP = @@ -16229,7 +16264,7 @@ File hreal.ml loaded () : void -Run time: 1.7s +Run time: 2.0s Intermediate theorems generated: 10456 #\ @@ -16239,7 +16274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -16379,7 +16414,7 @@ Run time: 0.0s HREAL_EQ_LADD = |- !x y z. (x hreal_add y = x hreal_add z) = (y = z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 94 Theorem HREAL_LT autoloading from theory `HREAL` ... @@ -16497,7 +16532,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 @@ -16514,7 +16549,7 @@ TREAL_ADD_ASSOC = |- !x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 63 Theorem HREAL_MUL_ASSOC autoloading from theory `HREAL` ... @@ -16524,7 +16559,7 @@ TREAL_MUL_ASSOC = |- !x y z. x treal_mul (y treal_mul z) = (x treal_mul y) treal_mul z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 388 TREAL_LDISTRIB = @@ -16570,7 +16605,7 @@ Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 48 TREAL_LT_REFL = |- !x. ~x treal_lt x @@ -16579,12 +16614,12 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1063 TREAL_LT_ADD = |- !x y z. y treal_lt z ==> (x treal_add y) treal_lt (x treal_add z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1045 TREAL_LT_MUL = @@ -16606,7 +16641,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.1s +Run time: 0.0s Intermediate theorems generated: 986 TREAL_ISO = @@ -16640,7 +16675,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 = @@ -16698,7 +16733,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.8s +Run time: 1.1s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -16707,7 +16742,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 = @@ -16768,7 +16803,7 @@ |- !x y z. y real_lt z ==> (x real_add y) real_lt (x real_add z); |- !x y. r0 real_lt x /\ r0 real_lt y ==> r0 real_lt (x real_mul y)] : thm list -Run time: 0.2s +Run time: 0.3s () : void Run time: 0.0s @@ -16777,7 +16812,7 @@ File realax.ml loaded () : void -Run time: 2.8s +Run time: 3.3s Intermediate theorems generated: 26795 #\ @@ -16787,7 +16822,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -16991,7 +17026,7 @@ Intermediate theorems generated: 14 REAL_MUL_RID = |- !x. x * (& 1) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 14 REAL_MUL_RINV = |- !x. ~(x = & 0) ==> (x * (inv x) = & 1) @@ -17027,7 +17062,7 @@ Intermediate theorems generated: 18 REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 101 REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -17039,7 +17074,7 @@ Intermediate theorems generated: 14 REAL_NEG_LMUL = |- !x y. --(x * y) = (-- x) * y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 62 REAL_NEG_RMUL = |- !x y. --(x * y) = x * (-- y) @@ -17107,7 +17142,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 @@ -17139,7 +17174,7 @@ Intermediate theorems generated: 24 REAL_NEG_GT0 = |- !x. (& 0) < (-- x) = x < (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 25 REAL_NEG_LE0 = |- !x. (-- x) <= (& 0) = (& 0) <= x @@ -17159,7 +17194,7 @@ Intermediate theorems generated: 73 REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) @@ -17171,7 +17206,7 @@ Intermediate theorems generated: 6 REAL_LT_01 = |- (& 0) < (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 REAL_LE_LADD = |- !x y z. (x + y) <= (x + z) = y <= z @@ -17179,7 +17214,7 @@ Intermediate theorems generated: 20 REAL_LE_RADD = |- !x y z. (x + z) <= (y + z) = x <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) @@ -17207,11 +17242,11 @@ 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 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 50 REAL_SUB_ADD2 = |- !x y. y + (x - y) = x @@ -17223,7 +17258,7 @@ Intermediate theorems generated: 20 REAL_SUB_0 = |- !x y. (x - y = & 0) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LE_DOUBLE = |- !x. (& 0) <= (x + x) = (& 0) <= x @@ -17239,7 +17274,7 @@ Intermediate theorems generated: 42 REAL_NEG_EQ0 = |- !x. (-- x = & 0) = (x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 45 REAL_NEG_0 = |- --(& 0) = & 0 @@ -17271,7 +17306,7 @@ Intermediate theorems generated: 21 REAL_SUB_LDISTRIB = |- !x y z. x * (y - z) = (x * y) - (x * z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 39 REAL_SUB_RDISTRIB = |- !x y z. (x - y) * z = (x * z) - (y * z) @@ -17283,7 +17318,7 @@ Intermediate theorems generated: 30 REAL_NEG_MINUS1 = |- !x. -- x = (--(& 1)) * x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 REAL_INV_NZ = |- !x. ~(x = & 0) ==> ~(inv x = & 0) @@ -17311,7 +17346,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) @@ -17323,7 +17358,7 @@ Intermediate theorems generated: 29 REAL_LT_LMUL_IMP = |- !x y z. y < z /\ (& 0) < x ==> (x * y) < (x * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 REAL_LINV_UNIQ = |- !x y. (x * y = & 1) ==> (x = inv y) @@ -17339,11 +17374,11 @@ Intermediate theorems generated: 71 REAL_INV_1OVER = |- !x. inv x = (& 1) / x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 REAL_LE_ADDR = |- !x y. x <= (x + y) = (& 0) <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_LE_ADDL = |- !x y. y <= (x + y) = (& 0) <= x @@ -17363,12 +17398,12 @@ Intermediate theorems generated: 19 REAL_POS = |- !n. (& 0) <= (& n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 70 Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m @@ -17424,7 +17459,7 @@ Run time: 0.0s REAL_MUL = |- !m n. (& m) * (& n) = &(m num_mul n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 148 REAL_INV1 = |- inv(& 1) = & 1 @@ -17444,11 +17479,11 @@ Intermediate theorems generated: 20 REAL_LT_NZ = |- !n. ~(& n = & 0) = (& 0) < (& n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 90 REAL_NZ_IMP_LT = |- !n. ~(n = 0) ==> (& 0) < (& n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 REAL_LT_RDIV_0 = |- !y z. (& 0) < z ==> ((& 0) < (y / z) = (& 0) < y) @@ -17497,11 +17532,11 @@ Intermediate theorems generated: 22 REAL_DOUBLE = |- !x. x + x = (& 2) * x -Run time: 0.1s +Run time: 0.0s 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) @@ -17513,7 +17548,7 @@ Intermediate theorems generated: 51 REAL_DOWN = |- !x. (& 0) < x ==> (?y. (& 0) < y /\ y < x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 REAL_DOWN2 = @@ -17522,7 +17557,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -17530,7 +17565,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 @@ -17546,11 +17581,11 @@ Intermediate theorems generated: 38 REAL_LT_NEG = |- !x y. (-- x) < (-- y) = y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 REAL_LE_NEG = |- !x y. (-- x) <= (-- y) = y <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 37 REAL_ADD2_SUB2 = |- !a b c d. (a + b) - (c + d) = (a - c) + (b - d) @@ -17605,7 +17640,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) @@ -17613,7 +17648,7 @@ Intermediate theorems generated: 24 REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 REAL_INV_MUL = @@ -17622,7 +17657,7 @@ Intermediate theorems generated: 142 REAL_LE_LMUL = |- !x y z. (& 0) < x ==> ((x * y) <= (x * z) = y <= z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) @@ -17632,7 +17667,7 @@ REAL_SUB_INV2 = |- !x y. ~(x = & 0) /\ ~(y = & 0) ==> ((inv x) - (inv y) = (y - x) / (x * y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y @@ -17640,11 +17675,11 @@ Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_MEAN = |- !x y. x < y ==> (?z. x < z /\ z < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) @@ -17672,12 +17707,12 @@ REAL_LE_LMUL_IMP = |- !x y z. (& 0) <= x /\ y <= z ==> (x * y) <= (x * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 65 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 @@ -17685,7 +17720,7 @@ Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) @@ -17693,7 +17728,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) @@ -17705,7 +17740,7 @@ Run time: 0.0s REAL_FACT_NZ = |- !n. ~(&(FACT n) = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_DIFFSQ = |- !x y. (x + y) * (x - y) = (x * x) - (y * y) @@ -17713,11 +17748,11 @@ Intermediate theorems generated: 165 REAL_POSSQ = |- !x. (& 0) < (x * x) = ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) @@ -17742,11 +17777,11 @@ Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 @@ -17766,16 +17801,16 @@ Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 385 ABS_LT_MUL2 = |- !w x y z. (abs w) < y /\ (abs x) < z ==> (abs(w * x)) < (y * z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 ABS_SUB = |- !x y. abs(x - y) = abs(y - x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 31 ABS_NZ = |- !x. ~(x = & 0) = (& 0) < (abs x) @@ -17783,15 +17818,15 @@ Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 105 ABS_ABS = |- !x. abs(abs x) = abs x -Run time: 0.1s +Run time: 0.0s 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 @@ -17804,15 +17839,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) @@ -17828,24 +17863,24 @@ Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 41 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)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 ABS_BETWEEN2 = @@ -17854,31 +17889,31 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 83 POW_PLUS1 = @@ -17895,7 +17930,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 @@ -17907,7 +17942,7 @@ Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) @@ -17919,7 +17954,7 @@ Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 135 REAL_LE_POW2 = |- !x. (& 0) <= (x pow 2) @@ -17927,11 +17962,11 @@ 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 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -17939,11 +17974,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` ... @@ -18010,21 +18045,21 @@ REAL_SUP_UBOUND = |- !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: 87 SETOK_LE_LT = |- !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 = |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 15 REAL_SUP_UBOUND_LE = @@ -18049,17 +18084,17 @@ |- !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 = |- (!n f. sum n 0 f = & 0) /\ (!n m f. sum n(SUC m)f = (sum n m f) + (f(n num_add m))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Sum = @@ -18076,7 +18111,7 @@ Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -18091,7 +18126,7 @@ |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r) <= (g r)) ==> (Sum(m,n)f) <= (Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 272 SUM_EQ = @@ -18108,7 +18143,7 @@ SUM_POS_GEN = |- !f m. (!n. m num_le n ==> (& 0) <= (f n)) ==> (!n. (& 0) <= (Sum(m,n)f)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 SUM_ABS = @@ -18126,7 +18161,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 GREATER_EQ autoloading from theory `arithmetic` ... GREATER_EQ = |- !n m. n num_ge m = m num_le n @@ -18136,12 +18171,12 @@ |- !f N. (!n. n num_ge N ==> (f n = & 0)) ==> (!m n. m num_ge N ==> (Sum(m,n)f = & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 145 SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) @@ -18149,12 +18184,12 @@ Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 89 SUM_SUB = |- !f g m n. Sum(m,n)(\n. (f n) - (g n)) = (Sum(m,n)f) - (Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 74 Theorem LESS_MONO_ADD autoloading from theory `arithmetic` ... @@ -18174,7 +18209,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 = @@ -18195,7 +18230,7 @@ SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18209,12 +18244,12 @@ 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.1s +Run time: 0.0s 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 @@ -18266,7 +18301,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.3s +Run time: 0.2s Intermediate theorems generated: 2469 SUM_CANCEL = @@ -18282,7 +18317,7 @@ File real.ml loaded () : void -Run time: 8.1s +Run time: 8.9s Intermediate theorems generated: 23746 #\ @@ -18292,7 +18327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -18382,7 +18417,7 @@ Run time: 0.0s re_Union = |- !S. re_Union S = (\x. ?s. S s /\ s x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 re_union = |- !P Q. P re_union Q = (\x. P x \/ Q x) @@ -18465,12 +18500,12 @@ Intermediate theorems generated: 2 OPEN_OWN_NEIGH = |- !S top x. open top S /\ S x ==> neigh top(S,x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 OPEN_UNOPEN = |- !S top. open top S = (re_Union(\P. open top P /\ P re_subset S) = S) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 212 OPEN_SUBOPEN = @@ -18493,7 +18528,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) @@ -18526,14 +18561,14 @@ Theorem REAL_ADD_LID autoloading from theory `REAL` ... REAL_ADD_LID = |- !x. (& 0) + x = x -Run time: 0.1s +Run time: 0.0s Theorem REAL_10 autoloading from theory `REAL` ... REAL_10 = |- ~(& 1 = & 0) 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 = @@ -18610,7 +18645,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18665,7 +18700,7 @@ Definition real_sub autoloading from theory `REAL` ... real_sub = |- !x y. x - y = x + (-- y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 Theorem ABS_TRIANGLE autoloading from theory `REAL` ... @@ -18689,7 +18724,7 @@ Run time: 0.0s ISMET_R1 = |- ismet(\(x,y). abs(y - x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 204 mr1 = |- mr1 = metric(\(x,y). abs(y - x)) @@ -18697,7 +18732,7 @@ Intermediate theorems generated: 2 MR1_DEF = |- !x y. dist mr1(x,y) = abs(y - x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -18726,7 +18761,7 @@ Intermediate theorems generated: 34 MR1_SUB_LE = |- !x d. (& 0) <= d ==> (dist mr1(x,x - d) = d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -18734,7 +18769,7 @@ Run time: 0.0s MR1_ADD_LT = |- !x d. (& 0) < d ==> (dist mr1(x,x + d) = d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 11 MR1_SUB_LT = |- !x d. (& 0) < d ==> (dist mr1(x,x - d) = d) @@ -18776,7 +18811,7 @@ File topology.ml loaded () : void -Run time: 1.3s +Run time: 1.4s Intermediate theorems generated: 4132 #\ @@ -18786,7 +18821,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -18952,7 +18987,7 @@ (?n. g n n /\ (!m. g m n ==> P m)) /\ (?n. g n n /\ (!m. g m n ==> Q m)) ==> (?n. g n n /\ (!m. g m n ==> P m /\ Q m))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 312 DORDER_THEN = - : ((thm -> *) -> thm -> *) @@ -18991,7 +19026,7 @@ Run time: 0.0s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 257 Definition re_subset autoloading from theory `TOPOLOGY` ... @@ -19009,7 +19044,7 @@ Definition neigh autoloading from theory `TOPOLOGY` ... neigh = |- !top N x. neigh top(N,x) = (?P. open top P /\ P re_subset N /\ P x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 Theorem METRIC_SYM autoloading from theory `TOPOLOGY` ... @@ -19030,7 +19065,7 @@ (x --> x0)(mtop d,g) = (!e. (& 0) < e ==> (?n. g n n /\ (!m. g m n ==> (dist d(x m,x0)) < e))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 373 Theorem METRIC_TRIANGLE autoloading from theory `TOPOLOGY` ... @@ -19070,7 +19105,7 @@ |- !d x x0. (x --> x0)(mtop d,$num_ge) = (!e. (& 0) < e ==> (?N. !n. n num_ge N ==> (dist d(x n,x0)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 64 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -19087,7 +19122,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.1s +Run time: 0.0s LIM_TENDS = |- !m1 m2 f x0 y0. @@ -19122,7 +19157,7 @@ (!x. (& 0) < (dist m1(x,x0)) /\ (dist m1(x,x0)) < d ==> (dist m2(f x,y0)) < e)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 246 Theorem ABS_NEG autoloading from theory `REAL` ... @@ -19175,7 +19210,7 @@ Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT autoloading from theory `REAL` ... REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -19183,7 +19218,7 @@ NET_CONV_BOUNDED = |- !g x x0. (x --> x0)(mtop mr1,g) ==> bounded(mr1,g)x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 119 Theorem REAL_LT_REFL autoloading from theory `REAL` ... @@ -19211,7 +19246,7 @@ Theorem ABS_INV autoloading from theory `REAL` ... ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) -Run time: 0.0s +Run time: 0.1s Theorem REAL_INJ autoloading from theory `REAL` ... REAL_INJ = |- !m n. (& m = & n) = (m = n) @@ -19258,7 +19293,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> bounded(mr1,g)(\n. inv(x n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 493 NET_NULL_ADD = @@ -19275,7 +19310,7 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 < x2 /\ y1 < y2 ==> (x1 * y1) < (x2 * y2) -Run time: 0.1s +Run time: 0.0s Theorem ABS_MUL autoloading from theory `REAL` ... ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) @@ -19369,7 +19404,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 NET_SUB = @@ -19454,7 +19489,7 @@ (!x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) --> (inv x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 1253 NET_DIV = @@ -19505,13 +19540,13 @@ Intermediate theorems generated: 400 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File nets.ml loaded () : void -Run time: 1.8s +Run time: 1.6s Intermediate theorems generated: 7389 #\ @@ -19521,7 +19556,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -19622,7 +19657,7 @@ Run time: 0.0s () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 () : void @@ -19734,7 +19769,7 @@ Run time: 0.0s SEQ_NEG = |- !x x0. x --> x0 = (\n. --(x n)) --> (-- x0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 26 Theorem NET_INV autoloading from theory `NETS` ... @@ -19814,7 +19849,7 @@ Intermediate theorems generated: 2 SEQ_LIM = |- !f. convergent f = f --> (lim f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 subseq = |- !f. subseq f = (!m n. m num_lt n ==> (f m) num_lt (f n)) @@ -19827,7 +19862,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.1s +Run time: 0.0s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -19843,7 +19878,7 @@ Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... LESS_SUC_REFL = |- !n. n num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) Run time: 0.0s @@ -19934,7 +19969,7 @@ Run time: 0.0s SEQ_BOUNDED = |- !s. bounded(mr1,$num_ge)s = (?k. !n. (abs(s n)) < k) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 273 Theorem REAL_LE_NEG autoloading from theory `REAL` ... @@ -20035,7 +20070,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` ... @@ -20111,7 +20146,7 @@ Run time: 0.0s SEQ_SUBLE = |- !f. subseq f ==> (!n. n num_le (f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 116 Theorem LESS_EQ_CASES autoloading from theory `arithmetic` ... @@ -20144,7 +20179,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` ... @@ -20162,7 +20197,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` ... @@ -20228,7 +20263,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` ... @@ -20406,7 +20441,7 @@ Theorem REAL_NEG_ADD autoloading from theory `REAL` ... REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_DOUBLE autoloading from theory `REAL` ... REAL_DOUBLE = |- !x. x + x = (& 2) * x @@ -20422,7 +20457,7 @@ Theorem REAL_SUB_LDISTRIB autoloading from theory `REAL` ... REAL_SUB_LDISTRIB = |- !x y z. x * (y - z) = (x * y) - (x * z) -Run time: 0.1s +Run time: 0.0s Theorem REAL_EQ_LMUL_IMP autoloading from theory `REAL` ... REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) @@ -20457,7 +20492,7 @@ ?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.3s +Run time: 0.4s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20465,7 +20500,7 @@ Intermediate theorems generated: 2 summable = |- !f. summable f = (?s. f sums s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 suminf = |- !f. suminf f = (@s. f sums s) @@ -20481,7 +20516,7 @@ Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 69 Theorem SUM_ZERO autoloading from theory `REAL` ... @@ -20504,7 +20539,7 @@ Run time: 0.0s SER_0 = |- !f n. (!m. n num_le m ==> (f m = & 0)) ==> f sums (Sum(0,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 175 Theorem SUM_POS_GEN autoloading from theory `REAL` ... @@ -20517,7 +20552,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) <= (f m)) ==> (Sum(0,n)f) <= (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 220 Theorem Sum autoloading from theory `REAL` ... @@ -20554,7 +20589,7 @@ Theorem SUM_GROUP autoloading from theory `REAL` ... SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.1s +Run time: 0.0s SER_GROUP = |- !f k. @@ -20617,7 +20652,7 @@ Theorem SUM_CMUL autoloading from theory `REAL` ... SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.1s +Run time: 0.0s SER_CMUL = |- !x x0 c. x sums x0 ==> (\n. c * (x n)) sums (c * x0) Run time: 0.0s @@ -20643,7 +20678,7 @@ Theorem SUM_DIFF autoloading from theory `REAL` ... SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) -Run time: 0.0s +Run time: 0.1s SER_CAUCHY = |- !f. @@ -20653,7 +20688,7 @@ Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 Theorem SUM_LE autoloading from theory `REAL` ... @@ -20678,7 +20713,7 @@ |- !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` ... @@ -20689,14 +20724,14 @@ |- !f g. (!n. (f n) <= (g n)) /\ summable f /\ summable g ==> (suminf f) <= (suminf g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 191 SER_LE2 = |- !f g. (!n. (abs(f n)) <= (g n)) /\ summable g ==> summable f /\ (suminf f) <= (suminf g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 Theorem SUM_ABS autoloading from theory `REAL` ... @@ -20715,7 +20750,7 @@ SER_ABS = |- !f. summable(\n. abs(f n)) ==> (abs(suminf f)) <= (suminf(\n. abs(f n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 92 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -20747,7 +20782,7 @@ Theorem REAL_NEG_MUL2 autoloading from theory `REAL` ... REAL_NEG_MUL2 = |- !x y. (-- x) * (-- y) = x * y -Run time: 0.1s +Run time: 0.0s Theorem REAL_INV_1OVER autoloading from theory `REAL` ... REAL_INV_1OVER = |- !x. inv x = (& 1) / x @@ -20799,13 +20834,13 @@ Intermediate theorems generated: 683 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File seq.ml loaded () : void -Run time: 3.6s +Run time: 4.3s Intermediate theorems generated: 18704 #\ @@ -20815,7 +20850,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -20913,11 +20948,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -21010,7 +21045,7 @@ Run time: 0.0s LIM_CONST = |- !k x. ((\x. k) --> k)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 193 Theorem DORDER_TENDSTO autoloading from theory `NETS` ... @@ -21039,7 +21074,7 @@ (!x y x0 y0. (x tends x0)(mtop mr1,g) /\ (y tends y0)(mtop mr1,g) ==> ((\n. (x n) * (y n)) tends (x0 * y0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s LIM_MUL = |- !f g l m. @@ -21115,7 +21150,7 @@ Run time: 0.0s LIM_NULL = |- !f l x. (f --> l)x = ((\x. (f x) - l) --> (& 0))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 23 LIM_X = |- !x0. ((\x. x) --> x0)x0 @@ -21131,7 +21166,7 @@ Run time: 0.0s LIM_UNIQ = |- !f l m x. (f --> l)x /\ (f --> m)x ==> (l = m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 36 LIM_EQUAL = @@ -21158,7 +21193,7 @@ Theorem REAL_LET_TRANS autoloading from theory `REAL` ... REAL_LET_TRANS = |- !x y z. x <= y /\ y < z ==> x < z -Run time: 0.0s +Run time: 0.1s Theorem REAL_HALF_DOUBLE autoloading from theory `REAL` ... REAL_HALF_DOUBLE = |- !x. (x / (& 2)) + (x / (& 2)) = x @@ -21213,7 +21248,7 @@ Run time: 0.0s DIFF_CONT = |- !f l x. (f diffl l)x ==> f contl x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 290 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -21233,7 +21268,7 @@ Intermediate theorems generated: 20 CONT_ADD = |- !x. f contl x /\ g contl x ==> (\x. (f x) + (g x)) contl x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 CONT_MUL = |- !x. f contl x /\ g contl x ==> (\x. (f x) * (g x)) contl x @@ -21394,7 +21429,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.1s +Run time: 0.0s Intermediate theorems generated: 150 Theorem REAL_MUL_SYM autoloading from theory `REAL` ... @@ -21478,7 +21513,7 @@ Theorem ABS_LE autoloading from theory `REAL` ... ABS_LE = |- !x. x <= (abs x) -Run time: 0.1s +Run time: 0.0s Theorem MR1_BOUNDED autoloading from theory `NETS` ... MR1_BOUNDED = @@ -21491,7 +21526,7 @@ (?k d. (& 0) < d /\ (!x. (& 0) < (abs(x - x0)) /\ (abs(x - x0)) < d ==> (abs(f x)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 362 Theorem REAL_MUL_LID autoloading from theory `REAL` ... @@ -21545,7 +21580,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.3s +Run time: 0.2s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21661,7 +21696,7 @@ ((\x. (f x) / (g x)) diffl (((l * (g x)) - (m * (f x))) / ((g x) pow 2))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 293 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -21695,7 +21730,7 @@ 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.1s +Run time: 0.0s Intermediate theorems generated: 301 CONT_BOUNDED = @@ -21722,7 +21757,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 412 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -21768,7 +21803,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -21792,7 +21827,7 @@ Theorem ABS_SIGN2 autoloading from theory `REAL` ... ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) -Run time: 0.0s +Run time: 0.1s Theorem REAL_NEG_INV autoloading from theory `REAL` ... REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -21806,7 +21841,7 @@ |- !f x l. (f diffl l)x /\ l < (& 0) ==> (?d. (& 0) < d /\ (!h. (& 0) < h /\ h < d ==> (f x) < (f(x - h)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 469 Theorem REAL_ADD_SUB2 autoloading from theory `REAL` ... @@ -21842,14 +21877,14 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f y = f x))) ==> (l = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 96 INTERVAL_LEMMA = |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -21867,7 +21902,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> f differentiable x) ==> (?z. a < z /\ z < b /\ (f diffl (& 0))z) -Run time: 0.3s +Run time: 0.2s Intermediate theorems generated: 3178 gfn = "\x. (f x) - ((((f b) - (f a)) / (b - a)) * x)" : term @@ -21875,7 +21910,7 @@ Theorem REAL_NEG_ADD autoloading from theory `REAL` ... REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_EQ_RMUL autoloading from theory `REAL` ... REAL_EQ_RMUL = |- !x y z. (x * z = y * z) = (z = & 0) \/ (x = y) @@ -21899,7 +21934,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 = @@ -21908,7 +21943,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -21921,7 +21956,7 @@ Intermediate theorems generated: 310 DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 172 () : void @@ -21931,7 +21966,7 @@ File lim.ml loaded () : void -Run time: 3.8s +Run time: 3.3s Intermediate theorems generated: 21608 #\ @@ -21941,7 +21976,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -22016,7 +22051,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -22111,7 +22146,7 @@ |- !n x y. Sum(0,SUC n)(\p. (x pow p) * (y pow ((SUC n) num_sub p))) = y * (Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 223 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -22168,7 +22203,7 @@ |- !n x y. (x pow (SUC n)) - (y pow (SUC n)) = (x - y) * (Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 485 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -22240,7 +22275,7 @@ Theorem SER_CMUL autoloading from theory `SEQ` ... SER_CMUL = |- !x x0 c. x sums x0 ==> (\n. c * (x n)) sums (c * x0) -Run time: 0.0s +Run time: 0.1s Definition real_div autoloading from theory `REAL` ... real_div = |- !x y. x / y = x * (inv y) @@ -22313,7 +22348,7 @@ Theorem SEQ_BOUNDED autoloading from theory `SEQ` ... SEQ_BOUNDED = |- !s. bounded(mr1,$num_ge)s = (?k. !n. (abs(s n)) < k) -Run time: 0.1s +Run time: 0.0s Theorem SEQ_CBOUNDED autoloading from theory `SEQ` ... SEQ_CBOUNDED = |- !f. cauchy f ==> bounded(mr1,$num_ge)f @@ -22336,7 +22371,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (abs(f n)) * (z pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22351,7 +22386,7 @@ Intermediate theorems generated: 67 diffs = |- !c. diffs c = (\n. (&(SUC n)) * (c(SUC n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 Theorem REAL_NEG_RMUL autoloading from theory `REAL` ... @@ -22359,7 +22394,7 @@ Run time: 0.0s DIFFS_NEG = |- !c. diffs(\n. --(c n)) = (\n. --(diffs c n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 37 Theorem SUC_SUB1 autoloading from theory `arithmetic` ... @@ -22412,7 +22447,7 @@ Theorem SEQ_SUC autoloading from theory `SEQ` ... SEQ_SUC = |- !f l. f tends_num_real l = (\n. f(SUC n)) tends_num_real l -Run time: 0.1s +Run time: 0.0s DIFFS_EQUIV = |- !c x. @@ -22463,7 +22498,7 @@ Theorem REAL_ADD2_SUB2 autoloading from theory `REAL` ... REAL_ADD2_SUB2 = |- !a b c d. (a + b) - (c + d) = (a - c) + (b - d) -Run time: 0.0s +Run time: 0.1s Theorem REAL_RDISTRIB autoloading from theory `REAL` ... REAL_RDISTRIB = |- !x y z. (x + y) * z = (x * z) + (y * z) @@ -22475,7 +22510,7 @@ Theorem REAL autoloading from theory `REAL` ... REAL = |- !n. &(SUC n) = (& n) + (& 1) -Run time: 0.1s +Run time: 0.0s Theorem REAL_EQ_LMUL autoloading from theory `REAL` ... REAL_EQ_LMUL = |- !x y z. (x * y = x * z) = (x = & 0) \/ (y = z) @@ -22584,7 +22619,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22729,7 +22764,7 @@ Theorem ABS_REFL autoloading from theory `REAL` ... ABS_REFL = |- !x. (abs x = x) = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Theorem REAL_MEAN autoloading from theory `REAL` ... REAL_MEAN = |- !x y. x < y ==> (?z. x < z /\ z < y) @@ -22797,13 +22832,13 @@ Intermediate theorems generated: 2494 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File powser.ml loaded () : void -Run time: 2.1s +Run time: 2.0s Intermediate theorems generated: 8507 #\ @@ -22813,7 +22848,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -22899,7 +22934,7 @@ Theory POWSER loaded () : void -Run time: 0.2s +Run time: 0.4s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -22918,7 +22953,7 @@ Run time: 0.0s MULT_DIV_2 = |- !n. (2 * n) DIV 2 = n -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 66 Theorem LEFT_ADD_DISTRIB autoloading from theory `arithmetic` ... @@ -22946,7 +22981,7 @@ Run time: 0.0s EVEN_DIV2 = |- !n. ~EVEN n ==> ((SUC n) DIV 2 = SUC((n - 1) DIV 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 152 real_interface_map = @@ -23090,7 +23125,7 @@ (EVEN n' => ((--(& 1)) pow (n' DIV 2)) / (&(FACT n')) | & 0)) n) * (x pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -23239,7 +23274,7 @@ EXP_CONVERGES = |- !x. (\n. ((\n. inv(&(FACT n)))n) * (x pow n)) sums (exp x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 628 Theorem REAL_INV_POS autoloading from theory `REAL` ... @@ -23256,7 +23291,7 @@ Theorem POW_M1 autoloading from theory `REAL` ... POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE_MUL autoloading from theory `REAL` ... REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) @@ -23295,7 +23330,7 @@ n) * (x pow n)) sums (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 272 COS_CONVERGES = @@ -23321,7 +23356,7 @@ Intermediate theorems generated: 1 EXP_FDIFF = |- diffs(\n. inv(&(FACT n))) = (\n. inv(&(FACT n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 193 Theorem REAL_MUL_RZERO autoloading from theory `REAL` ... @@ -23349,7 +23384,7 @@ Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... @@ -23392,7 +23427,7 @@ ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) n) * (x pow n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 42 Theorem REAL_LT_ADDR autoloading from theory `REAL` ... @@ -23432,7 +23467,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; @@ -23475,7 +23510,7 @@ Run time: 0.0s EXP_0 = |- exp(& 0) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 274 Theorem REAL_LE_REFL autoloading from theory `REAL` ... @@ -23513,7 +23548,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) @@ -23538,11 +23573,11 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 EXP_NEG_MUL2 = |- !x. (exp(-- x)) * (exp x) = & 1 @@ -23710,7 +23745,7 @@ LN_MUL = |- !x y. (& 0) < x /\ (& 0) < y ==> (ln(x * y) = (ln x) + (ln y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 113 LN_INJ = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x = ln y) = (x = y)) @@ -23757,7 +23792,7 @@ Intermediate theorems generated: 2 sqrt = |- !x. sqrt x = root 2 x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -23783,7 +23818,7 @@ Run time: 0.0s ROOT_0 = |- !n. root(SUC n)(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem REAL_DIV_LZERO autoloading from theory `REAL` ... @@ -23803,7 +23838,7 @@ Intermediate theorems generated: 20 SQRT_1 = |- sqrt(& 1) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 Theorem REAL_LE_POW2 autoloading from theory `REAL` ... @@ -23819,7 +23854,7 @@ Run time: 0.0s SIN_0 = |- sin(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -23873,7 +23908,7 @@ Run time: 0.0s SIN_BOUND = |- !x. (abs(sin x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem ABS_BOUNDS autoloading from theory `REAL` ... @@ -23881,7 +23916,7 @@ Run time: 0.0s SIN_BOUNDS = |- !x. (--(& 1)) <= (sin x) /\ (sin x) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 Theorem REAL_LET_ADD autoloading from theory `REAL` ... @@ -23932,7 +23967,7 @@ |- !x. (((sin(-- x)) + (sin x)) pow 2) + (((cos(-- x)) - (cos x)) pow 2) = & 0 -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 1099 Theorem REAL_SUMSQ autoloading from theory `REAL` ... @@ -23954,11 +23989,11 @@ Run time: 0.0s SIN_NEG = |- !x. sin(-- x) = --(sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 COS_NEG = |- !x. cos(-- x) = cos x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 47 Theorem REAL_DOUBLE autoloading from theory `REAL` ... @@ -23996,7 +24031,7 @@ (((--(& 1)) pow n) / (&(FACT((2 num_mul n) num_add 1)))) * (x pow ((2 num_mul n) num_add 1))) sums (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 183 Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... @@ -24082,7 +24117,7 @@ Run time: 0.0s COS_2 = |- (cos(& 2)) < (& 0) -Run time: 0.4s +Run time: 0.5s Intermediate theorems generated: 3794 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -24146,7 +24181,7 @@ Intermediate theorems generated: 42 PI2_BOUNDS = |- (& 0) < (pi / (& 2)) /\ (pi / (& 2)) < (& 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 124 Theorem REAL_LT_ADD autoloading from theory `REAL` ... @@ -24194,7 +24229,7 @@ Intermediate theorems generated: 59 COS_PERIODIC_PI = |- !x. cos(x + pi) = --(cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 59 SIN_PERIODIC = |- !x. sin(x + ((& 2) * pi)) = sin x @@ -24206,11 +24241,11 @@ Intermediate theorems generated: 47 COS_NPI = |- !n. cos((& n) * pi) = (--(& 1)) pow n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 134 SIN_NPI = |- !n. sin((& n) * pi) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 137 SIN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (sin x) @@ -24309,13 +24344,13 @@ |- !y. (& 0) < y ==> (!x. (& 0) <= x ==> (?n. ((& n) * y) <= x /\ x < ((&(SUC n)) * y))) -Run time: 0.0s +Run time: 0.1s COS_ZERO_LEMMA = |- !x. (& 0) <= x /\ (cos x = & 0) ==> (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 675 Theorem REAL_LE_ADDR autoloading from theory `REAL` ... @@ -24342,7 +24377,7 @@ (cos x = & 0) = (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. ~EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 630 Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... @@ -24358,7 +24393,7 @@ (sin 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: 319 tan = |- !x. tan x = (sin x) / (cos x) @@ -24366,7 +24401,7 @@ Intermediate theorems generated: 2 TAN_0 = |- tan(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 TAN_PI = |- tan pi = & 0 @@ -24402,14 +24437,14 @@ |- !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.1s +Run time: 0.0s Intermediate theorems generated: 869 TAN_DOUBLE = |- !x. ~(cos x = & 0) /\ ~(cos((& 2) * x) = & 0) ==> (tan((& 2) * x) = ((& 2) * (tan x)) / ((& 1) - ((tan x) pow 2))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 TAN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (tan x) @@ -24421,7 +24456,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24456,7 +24491,7 @@ Theorem CONTL_LIM autoloading from theory `LIM` ... CONTL_LIM = |- !f x. f contl x = (f tends_real_real (f x))x -Run time: 0.1s +Run time: 0.0s Theorem LIM_DIV autoloading from theory `LIM` ... LIM_DIV = @@ -24467,7 +24502,7 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1046 TAN_TOTAL_POS = @@ -24501,11 +24536,11 @@ |- !y. asn y = (@x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.1s +Run time: 0.0s 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 = @@ -24537,7 +24572,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 = @@ -24548,13 +24583,13 @@ Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 ACS_BOUNDS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 COS_ACS = |- !x. (& 0) <= x /\ x <= pi ==> (acs(cos x) = x) @@ -24570,7 +24605,7 @@ Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) @@ -24579,17 +24614,17 @@ 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 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File transc.ml loaded () : void -Run time: 6.2s +Run time: 6.5s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/theories' @@ -24602,7 +24637,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -24624,7 +24659,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -24690,7 +24725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -24722,7 +24757,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -24831,7 +24866,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -24984,7 +25019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25057,7 +25092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25137,7 +25172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25294,7 +25329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25449,7 +25484,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25666,7 +25701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25688,7 +25723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25707,7 +25742,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25752,7 +25787,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25817,7 +25852,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25867,7 +25902,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -25937,7 +25972,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26007,7 +26042,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26043,7 +26078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26096,7 +26131,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26168,7 +26203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26247,7 +26282,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26442,7 +26477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -26479,7 +26514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -27165,7 +27200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -27637,7 +27672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -27901,7 +27936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -28146,7 +28181,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -28610,7 +28645,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29078,7 +29113,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29134,7 +29169,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29224,7 +29259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29423,7 +29458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29455,7 +29490,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29589,7 +29624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29892,7 +29927,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29924,7 +29959,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29963,7 +29998,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -29995,7 +30030,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30156,7 +30191,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30289,7 +30324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30478,7 +30513,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30538,7 +30573,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30663,7 +30698,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30774,7 +30809,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30799,7 +30834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30827,7 +30862,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -30940,7 +30975,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -31443,7 +31478,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -31691,7 +31726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -31917,7 +31952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -31959,7 +31994,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -31991,7 +32026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -32214,7 +32249,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -32607,7 +32642,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -32720,7 +32755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33223,7 +33258,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33471,7 +33506,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33697,7 +33732,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33732,7 +33767,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33771,7 +33806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33808,7 +33843,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33829,7 +33864,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33926,7 +33961,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -33948,7 +33983,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34444,7 +34479,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34467,7 +34502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34545,7 +34580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34604,7 +34639,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34648,7 +34683,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34666,7 +34701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34693,7 +34728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34737,7 +34772,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34850,7 +34885,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34897,7 +34932,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -34936,7 +34971,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35010,7 +35045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35099,7 +35134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35170,7 +35205,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35240,7 +35275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35289,7 +35324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35330,7 +35365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35371,7 +35406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35395,7 +35430,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35496,7 +35531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35517,7 +35552,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -35542,7 +35577,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36168,7 +36203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36245,7 +36280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36272,7 +36307,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36389,7 +36424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36484,7 +36519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36570,7 +36605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36685,7 +36720,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36778,7 +36813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -36954,7 +36989,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37058,7 +37093,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37353,7 +37388,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37456,7 +37491,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37524,7 +37559,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37586,7 +37621,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37766,7 +37801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37807,7 +37842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37837,7 +37872,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -37863,7 +37898,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -38381,7 +38416,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -38918,7 +38953,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -39106,7 +39141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 7/1/24 =============================================================================== #false : bool @@ -39124,10 +39159,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library' date -Sat Jan 6 13:51:48 -12 2024 +Sun Jan 7 17:45:15 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 13:51:48 -12 2024 +Sun Jan 7 17:45:15 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39145,22 +39180,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 7/1/24 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 6/1/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 7/1/24 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -HOL-LCF version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 7/1/24 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -40897,7 +40932,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -42663,7 +42698,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44407,7 +44442,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44662,7 +44697,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44899,7 +44934,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45077,7 +45112,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45266,7 +45301,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45385,7 +45420,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45501,7 +45536,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45741,7 +45776,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46082,7 +46117,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46289,7 +46324,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46632,7 +46667,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46824,7 +46859,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47092,7 +47127,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47253,7 +47288,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47398,7 +47433,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47550,7 +47585,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47706,7 +47741,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47884,7 +47919,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48080,7 +48115,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48305,7 +48340,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48566,7 +48601,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:1412' -> endpages.ps +' TeX output 2024.01.07:1803' -> endpages.ps @@ -48629,7 +48664,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:1413' -> titlepages.ps +' TeX output 2024.01.07:1803' -> titlepages.ps @@ -48702,8 +48737,8 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316-35.1_armhf.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316-35.1_armhf.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316-35.1_armhf.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316/%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.19940316/%s\n",$1,a);}' >>debian/hol88-source.install @@ -48750,10 +48785,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 @@ -48762,15 +48799,16 @@ dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316-35.1_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35.1_all.deb'. -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35.1_all.deb'. -dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316-35.1_all.deb'. +dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35.1_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35.1_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316-35.1_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' dpkg-genbuildinfo --build=binary @@ -48780,12 +48818,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/26855/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/26855/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/24521 and its subdirectories -I: Current time: Sat Jan 6 14:26:07 -12 2024 -I: pbuilder-time-stamp: 1704594367 +I: removing directory /srv/workspace/pbuilder/26855 and its subdirectories +I: Current time: Sun Jan 7 18:10:48 +14 2024 +I: pbuilder-time-stamp: 1704600648