Diff of the two buildlogs: -- --- b1/build.log 2024-01-06 19:30:58.960635329 +0000 +++ b2/build.log 2024-01-06 19:41:29.712786776 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Jan 6 04:17:51 -12 2024 -I: pbuilder-time-stamp: 1704557871 +I: Current time: Sat Feb 8 15:54:04 +14 2025 +I: pbuilder-time-stamp: 1738979644 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -28,49 +28,81 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/844868/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/206875/tmp/hooks/D01_modify_environment starting +debug: Running on ionos15-amd64. +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 Feb 8 01:54 /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/206875/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/206875/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='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=15 ' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="15" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.15(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=16 ' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='69afde6892bd4b249c71ff5dbf733428' - 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='844868' - PS1='# ' - PS2='> ' + INVOCATION_ID=949bd3e50a0246c189b36405a895bf97 + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + 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=206875 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.4zgKZvSt/pbuilderrc_E1Nv --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.4zgKZvSt/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='110' - SUDO_UID='105' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://78.137.99.97:3128' + 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.4zgKZvSt/pbuilderrc_ichn --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.4zgKZvSt/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=111 + SUDO_UID=106 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://85.184.249.68:3128 I: uname -a - Linux ionos1-amd64 6.1.0-17-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.69-1 (2023-12-30) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.5.0-0.deb12.4-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.5.10-1~bpo12+1 (2023-11-23) x86_64 GNU/Linux I: ls -l /bin total 5632 -rwxr-xr-x 1 root root 1265648 Apr 23 2023 bash @@ -128,15 +160,15 @@ -rwxr-xr-x 1 root root 52112 Sep 20 2022 readlink -rwxr-xr-x 1 root root 72752 Sep 20 2022 rm -rwxr-xr-x 1 root root 56240 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 27560 Jul 28 23:46 run-parts + -rwxr-xr-x 1 root root 27560 Jul 28 2023 run-parts -rwxr-xr-x 1 root root 126424 Jan 5 2023 sed - lrwxrwxrwx 1 root root 4 Jan 5 2023 sh -> dash + lrwxrwxrwx 1 root root 9 Feb 8 01:54 sh -> /bin/bash -rwxr-xr-x 1 root root 43888 Sep 20 2022 sleep -rwxr-xr-x 1 root root 85008 Sep 20 2022 stty -rwsr-xr-x 1 root root 72000 Mar 23 2023 su -rwxr-xr-x 1 root root 39824 Sep 20 2022 sync -rwxr-xr-x 1 root root 531984 Apr 6 2023 tar - -rwxr-xr-x 1 root root 14520 Jul 28 23:46 tempfile + -rwxr-xr-x 1 root root 14520 Jul 28 2023 tempfile -rwxr-xr-x 1 root root 109616 Sep 20 2022 touch -rwxr-xr-x 1 root root 35664 Sep 20 2022 true -rwxr-xr-x 1 root root 14568 Mar 23 2023 ulockmgr_server @@ -156,7 +188,7 @@ -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew -I: user script /srv/workspace/pbuilder/844868/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/206875/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -379,7 +411,7 @@ Get: 181 http://deb.debian.org/debian bookworm/main amd64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 182 http://deb.debian.org/debian bookworm/main amd64 texlive-base all 2022.20230122-3 [21.9 MB] Get: 183 http://deb.debian.org/debian bookworm/main amd64 texlive-latex-base all 2022.20230122-3 [1182 kB] -Fetched 184 MB in 1min 40s (1843 kB/s) +Fetched 184 MB in 2s (96.1 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libargon2-1:amd64. (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 ... 18148 files and directories currently installed.) @@ -993,8 +1025,8 @@ Setting up tzdata (2023c-5+deb12u1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Jan 6 16:23:15 UTC 2024. -Universal Time is now: Sat Jan 6 16:23:15 UTC 2024. +Local time is now: Sat Feb 8 01:54:36 UTC 2025. +Universal Time is now: Sat Feb 8 01:54:36 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libdconf1:amd64 (0.40.0-4) ... @@ -1181,7 +1213,11 @@ fakeroot is already the newest version (1.31-1.2). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/206875/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bookworm +I: user script /srv/workspace/pbuilder/206875/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1574,7 +1610,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 6 04:28:30 -12 2024 +Sat Feb 8 15:55:29 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2812,7 +2848,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # mem = - : (* -> * list -> bool) @@ -2950,7 +2986,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #.............start address -T 0xa81dc0 () : void @@ -3109,7 +3145,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #.............start address -T 0xa81dc0 () : void @@ -3301,7 +3337,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # concat = - : (string -> string -> string) @@ -3411,7 +3447,7 @@ start address -T 0xa7af00 ;; Finished loading "lisp/f-ol-net" start address -T 0xa349d0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 6/1/24 + version 2.02 (GCL) created 8/2/25 #...start address -T 0xa86fd0 () : void @@ -3740,7 +3776,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ###########################() : void @@ -3753,7 +3789,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ################################################################################################() : void @@ -3898,7 +3934,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ############################() : void @@ -3941,7 +3977,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ############################Theory ind loaded () : void @@ -3978,7 +4014,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4019,7 +4055,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4421,7 +4457,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4489,7 +4525,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4694,7 +4730,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4818,7 +4854,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4904,7 +4940,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4997,7 +5033,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5066,7 +5102,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5171,7 +5207,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5406,7 +5442,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5432,7 +5468,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5560,7 +5596,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5608,7 +5644,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5675,7 +5711,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5734,7 +5770,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5790,7 +5826,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 8/2/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre3 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5803,7 +5839,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5855,7 +5891,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##########################() : void @@ -5886,7 +5922,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##############################() : void @@ -5973,7 +6009,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #######################################################################() : void @@ -6126,7 +6162,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###########################() : void @@ -6161,7 +6197,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #############################() : void @@ -6222,7 +6258,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###########################Theory arithmetic loaded () : void @@ -6717,7 +6753,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##################################() : void @@ -6864,7 +6900,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 8/2/25 #################################Theory list loaded () : void @@ -7203,7 +7239,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###############################Theory list loaded () : void @@ -8700,7 +8736,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #############################() : void @@ -9084,7 +9120,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################() : void @@ -9382,7 +9418,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################() : void @@ -9522,7 +9558,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################################() : void @@ -9619,7 +9655,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##################################() : void @@ -9649,7 +9685,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9666,7 +9702,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #Theory num loaded () : void @@ -9685,7 +9721,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9842,7 +9878,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # @@ -9880,7 +9916,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # @@ -9914,7 +9950,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9999,7 +10035,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -10040,7 +10076,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -10224,7 +10260,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10300,7 +10336,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 8/2/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre3 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10313,7 +10349,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -10377,11 +10413,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 6 04:58:20 -12 2024 +Sat Feb 8 15:57:28 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 6 04:58:22 -12 2024 +Sat Feb 8 15:57:28 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10404,7 +10440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -10488,7 +10524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -10594,7 +10630,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11344,7 +11380,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11367,7 +11403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11410,7 +11446,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11446,7 +11482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11498,7 +11534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11530,7 +11566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11568,7 +11604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11596,7 +11632,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11673,7 +11709,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11695,7 +11731,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11749,7 +11785,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11798,7 +11834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11949,7 +11985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11993,7 +12029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12068,7 +12104,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12118,7 +12154,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12181,7 +12217,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12234,7 +12270,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12280,7 +12316,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12368,7 +12404,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12406,7 +12442,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12467,7 +12503,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12531,7 +12567,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12557,7 +12593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12582,7 +12618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12621,7 +12657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12697,7 +12733,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13434,7 +13470,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13457,7 +13493,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13500,7 +13536,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13535,7 +13571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13576,7 +13612,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13639,7 +13675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13662,7 +13698,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13687,7 +13723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13714,7 +13750,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13750,7 +13786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14282,7 +14318,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14305,7 +14341,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14339,7 +14375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14394,7 +14430,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14485,7 +14521,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14654,7 +14690,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14808,7 +14844,7 @@ WOSET_TRANS_LESS = |- !l. woset l ==> (!x y z. less l(x,y) /\ l(y,z) ==> less l(x,z)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 144 WOSET = @@ -14818,7 +14854,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) @@ -14869,7 +14905,7 @@ |- !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.1s +Run time: 0.0s Intermediate theorems generated: 469 WO_INDUCT_TAC = - : tactic @@ -14887,7 +14923,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14897,7 +14933,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.0s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14907,7 +14943,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 = @@ -14922,7 +14958,7 @@ Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... LESS_EQ_REFL = |- !m. m <= m -Run time: 0.1s +Run time: 0.0s FL_NUM = |- !n. fl(\(m,n). m <= n)n Run time: 0.0s @@ -14941,7 +14977,7 @@ Run time: 0.0s WOSET_NUM = |- woset(\(m,n). m <= n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 148 Theorem LESS_NOT_EQ autoloading from theory `prim_rec` ... @@ -14969,7 +15005,7 @@ Intermediate theorems generated: 232 INSEG_SUBSET = |- !l m. m inseg l ==> (!x y. m(x,y) ==> l(x,y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) @@ -14977,7 +15013,7 @@ Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -14985,7 +15021,7 @@ Intermediate theorems generated: 240 LINSEG_WOSET = |- !l a. woset l ==> woset(linseg l a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 39 LINSEG_FL = |- !l a x. woset l ==> (fl(linseg l a)x = less l(x,a)) @@ -15006,7 +15042,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 1172 EXTEND_FL = @@ -15081,14 +15117,14 @@ |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2506 ZL = |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -15117,7 +15153,7 @@ File mk_wellorder loaded () : void -Run time: 2.4s +Run time: 0.4s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15126,7 +15162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15257,7 +15293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15349,7 +15385,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15399,19 +15435,19 @@ Run time: 0.0s GROUP_THOBS = |- IS_GROUP(group(\x y. ~(x = y))F I) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 732 |- !a. I(I a) = a -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 1106 concrete_rep = "group(\x y. x = y)T I" : term @@ -15428,7 +15464,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.4s +Run time: 0.1s Intermediate theorems generated: 2546 () : void @@ -15438,15 +15474,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.9s +Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Jan 6 05:26:39 -12 2024 +===> abs_theory rebuilt on Sat Feb 8 15:58:19 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15606,7 +15642,7 @@ File abs_theory compiled () : void -Run time: 0.4s +Run time: 0.0s make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals' @@ -15619,7 +15655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15706,7 +15742,7 @@ File equiv loaded () : void -Run time: 0.2s +Run time: 0.0s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -15740,7 +15776,7 @@ Run time: 0.0s UNSUCK_TAC = - : tactic -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 336 trat_1 = |- trat_1 = 0,0 @@ -15811,7 +15847,7 @@ Run time: 0.0s TRAT_ADD_SYM_EQ = |- !h i. h trat_add i = i trat_add h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 62 TRAT_MUL_SYM_EQ = |- !h i. h trat_mul i = i trat_mul h @@ -15841,7 +15877,7 @@ TRAT_MUL_WELLDEFINED = |- !p q r. p trat_eq q ==> (p trat_mul r) trat_eq (q trat_mul r) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 207 TRAT_MUL_WELLDEFINED2 = @@ -15862,7 +15898,7 @@ 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) @@ -15883,7 +15919,7 @@ |- !h i j. (h trat_mul (i trat_add j)) trat_eq ((h trat_mul i) trat_add (h trat_mul j)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h @@ -15891,7 +15927,7 @@ Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 136 Theorem ADD_INV_0_EQ autoloading from theory `arithmetic` ... @@ -15899,7 +15935,7 @@ Run time: 0.0s TRAT_NOZERO = |- !h i. ~(h trat_add i) trat_eq h -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 250 Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... @@ -15919,11 +15955,11 @@ 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.1s +Run time: 0.0s Intermediate theorems generated: 233 Theorem LESS_ADD_NONZERO autoloading from theory `arithmetic` ... @@ -15955,7 +15991,7 @@ 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 = @@ -15986,7 +16022,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.8s +Run time: 0.0s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -16010,7 +16046,7 @@ HRAT_LDISTRIB = |- !h i j. h hrat_mul (i hrat_add j) = (h hrat_mul i) hrat_add (h hrat_mul j) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 7 HRAT_MUL_LID = |- !h. hrat_1 hrat_mul h = h @@ -16046,7 +16082,7 @@ File hrat.ml loaded () : void -Run time: 2.1s +Run time: 0.1s Intermediate theorems generated: 11032 #\ @@ -16056,7 +16092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -16130,7 +16166,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -16222,7 +16258,7 @@ Intermediate theorems generated: 33 HRAT_EQ_LADD = |- !x y z. (x hrat_add y = x hrat_add z) = (y = z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 126 Theorem HRAT_MUL_ASSOC autoloading from theory `HRAT` ... @@ -16253,7 +16289,7 @@ HRAT_LT_MUL2 = |- !u v x y. u hrat_lt x /\ v hrat_lt y ==> (u hrat_mul v) hrat_lt (x hrat_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 100 HRAT_LT_LMUL = @@ -16285,7 +16321,7 @@ HRAT_LT_R1 = |- !x y. (x hrat_mul (hrat_inv y)) hrat_lt hrat_1 = x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 10 HRAT_GT_L1 = @@ -16311,7 +16347,7 @@ Intermediate theorems generated: 154 HRAT_MEAN = |- !x y. x hrat_lt y ==> (?z. x hrat_lt z /\ z hrat_lt y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 133 isacut = @@ -16338,7 +16374,7 @@ hreal_tybij = |- (!a. hreal(cut a) = a) /\ (!r. isacut r = (cut(hreal r) = r)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 4 EQUAL_CUTS = |- !X Y. (cut X = cut Y) ==> (X = Y) @@ -16378,7 +16414,7 @@ Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 137 Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... @@ -16397,7 +16433,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.1s +Run time: 0.0s Theorem HRAT_ARCH autoloading from theory `HRAT` ... HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16436,7 +16472,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) @@ -16452,17 +16488,17 @@ isacut (\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: 502 HREAL_ADD_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 521 HREAL_MUL_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X @@ -16480,18 +16516,18 @@ HREAL_MUL_ASSOC = |- !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 490 HREAL_LDISTRIB = |- !X Y Z. X hreal_mul (Y hreal_add Z) = (X hreal_mul Y) hreal_add (X hreal_mul Z) -Run time: 0.1s +Run time: 0.0s 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 @@ -16514,16 +16550,16 @@ 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.1s +Run time: 0.0s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 492 HREAL_LT = |- !X Y. X hreal_lt Y = (?D. Y = X hreal_add D) @@ -16546,7 +16582,7 @@ |- !P. (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==> (!Y. (?X. P X /\ Y hreal_lt X) = Y hreal_lt (hreal_sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 553 () : void @@ -16556,7 +16592,7 @@ File hreal.ml loaded () : void -Run time: 2.5s +Run time: 0.2s Intermediate theorems generated: 10456 #\ @@ -16566,7 +16602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -16663,7 +16699,7 @@ File equiv loaded () : void -Run time: 0.1s +Run time: 0.0s Theorem HREAL_LDISTRIB autoloading from theory `HREAL` ... HREAL_LDISTRIB = @@ -16680,7 +16716,7 @@ |- !x y z. (x hreal_add y) hreal_mul z = (x hreal_mul z) hreal_add (y hreal_mul z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 Theorem HREAL_NOZERO autoloading from theory `HREAL` ... @@ -16807,7 +16843,7 @@ Intermediate theorems generated: 2 TREAL_EQ_REFL = |- !x. x treal_eq x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 TREAL_EQ_SYM = |- !x y. x treal_eq y = y treal_eq x @@ -16816,7 +16852,7 @@ TREAL_EQ_TRANS = |- !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1147 TREAL_EQ_EQUIV = |- !p q. p treal_eq q = ($treal_eq p = $treal_eq q) @@ -16841,7 +16877,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` ... @@ -16858,7 +16894,7 @@ |- !x y z. x treal_mul (y treal_add z) = (x treal_mul y) treal_add (x treal_mul z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 345 TREAL_ADD_LID = |- !x. (treal_0 treal_add x) treal_eq x @@ -16870,7 +16906,7 @@ Run time: 0.0s TREAL_MUL_LID = |- !x. (treal_1 treal_mul x) treal_eq x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 217 TREAL_ADD_LINV = |- !x. ((treal_neg x) treal_add x) treal_eq treal_0 @@ -16893,7 +16929,7 @@ TREAL_MUL_LINV = |- !x. ~x treal_eq treal_0 ==> ((treal_inv x) treal_mul x) treal_eq treal_1 -Run time: 0.3s +Run time: 0.0s Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x @@ -16906,7 +16942,7 @@ 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 = @@ -16918,7 +16954,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -16933,28 +16969,28 @@ |- (!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 = |- !h i. h hreal_lt i ==> (treal_of_hreal h) treal_lt (treal_of_hreal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 450 TREAL_BIJ_WELLDEF = |- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1446 TREAL_NEG_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 58 TREAL_ADD_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1044 TREAL_ADD_WELLDEF = @@ -16979,12 +17015,12 @@ TREAL_LT_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_lt y = x2 treal_lt y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 519 TREAL_LT_WELLDEFL = |- !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 612 TREAL_LT_WELLDEF = @@ -16996,7 +17032,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -17025,12 +17061,12 @@ (!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: 1.0s +Run time: 0.1s Intermediate theorems generated: 7766 REAL_ISO_EQ = |- !h i. h hreal_lt i = (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 98 REAL_POS = |- !X. r0 real_lt (real_of_hreal X) @@ -17054,7 +17090,7 @@ (?z. !x. P x ==> x real_lt z) ==> (?X. (\h. P(real_of_hreal h))X) /\ (?Y. !X. (\h. P(real_of_hreal h))X ==> X hreal_lt Y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 135 SUP_ALLPOS_LEMMA4 = @@ -17075,7 +17111,7 @@ (?x. P x) /\ (?z. !x. P x ==> x real_lt z) ==> (?s. !y. (?x. P x /\ y real_lt x) = y real_lt s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 199 [|- ~(r1 = r0); @@ -17095,7 +17131,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.1s () : void Run time: 0.0s @@ -17104,7 +17140,7 @@ File realax.ml loaded () : void -Run time: 3.9s +Run time: 0.4s Intermediate theorems generated: 26795 #\ @@ -17114,7 +17150,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -17188,7 +17224,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -17259,7 +17295,7 @@ Intermediate theorems generated: 2 REAL_MUL_ASSOC = |- !x y z. x * (y * z) = (x * y) * z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 REAL_ADD_LID = |- !x. (& 0) + x = x @@ -17306,7 +17342,7 @@ |- !P. (!x. P x ==> (& 0) < x) /\ (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 12 REAL_ADD_RID = |- !x. x + (& 0) = x @@ -17338,7 +17374,7 @@ Intermediate theorems generated: 21 REAL_ADD_LID_UNIQ = |- !x y. (x + y = y) = (x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 REAL_ADD_RID_UNIQ = |- !x y. (x + y = x) = (y = & 0) @@ -17362,7 +17398,7 @@ Intermediate theorems generated: 40 REAL_MUL_RZERO = |- !x. x * (& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 14 REAL_NEG_LMUL = |- !x y. --(x * y) = (-- x) * y @@ -17386,7 +17422,7 @@ Intermediate theorems generated: 116 REAL_LT_LADD = |- !x y z. (x + y) < (x + z) = y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 REAL_LT_RADD = |- !x y z. (x + z) < (y + z) = x < y @@ -17410,7 +17446,7 @@ Intermediate theorems generated: 19 REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 55 REAL_LET_TOTAL = |- !x y. x <= y \/ y < x @@ -17430,7 +17466,7 @@ Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 125 REAL_LT_IMP_LE = |- !x y. x < y ==> x <= y @@ -17470,7 +17506,7 @@ Intermediate theorems generated: 25 REAL_NEG_LE0 = |- !x. (-- x) <= (& 0) = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_NEG_GE0 = |- !x. (& 0) <= (-- x) = x <= (& 0) @@ -17486,7 +17522,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) @@ -17502,7 +17538,7 @@ Intermediate theorems generated: 29 REAL_LE_LADD = |- !x y z. (x + y) <= (x + z) = y <= z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_LE_RADD = |- !x y z. (x + z) <= (y + z) = x <= y @@ -17534,7 +17570,7 @@ Intermediate theorems generated: 49 REAL_LT_ADD1 = |- !x y. x <= y ==> x < (y + (& 1)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 75 REAL_SUB_ADD = |- !x y. (x - y) + y = x @@ -17554,7 +17590,7 @@ Intermediate theorems generated: 33 REAL_LE_DOUBLE = |- !x. (& 0) <= (x + x) = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 72 REAL_LE_NEGL = |- !x. (-- x) <= x = (& 0) <= x @@ -17570,7 +17606,7 @@ Intermediate theorems generated: 45 REAL_NEG_0 = |- --(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x @@ -17602,7 +17638,7 @@ Intermediate theorems generated: 39 REAL_SUB_RDISTRIB = |- !x y z. (x - y) * z = (x * z) - (y * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_NEG_EQ = |- !x y. (-- x = y) = (x = -- y) @@ -17642,7 +17678,7 @@ Intermediate theorems generated: 57 REAL_LT_RMUL = |- !x y z. (& 0) < z ==> ((x * z) < (y * z) = x < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_LT_RMUL_IMP = |- !x y z. x < y /\ (& 0) < z ==> (x * z) < (y * z) @@ -17658,7 +17694,7 @@ Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17670,7 +17706,7 @@ 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 @@ -17686,7 +17722,7 @@ Intermediate theorems generated: 17 REAL = |- !n. &(SUC n) = (& n) + (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 REAL_POS = |- !n. (& 0) <= (& n) @@ -17699,7 +17735,7 @@ Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m -Run time: 0.1s +Run time: 0.0s Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... LESS_EQ_MONO = |- !n m. (SUC n) num_le (SUC m) = n num_le m @@ -17714,7 +17750,7 @@ Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 Theorem LESS_EQUAL_ANTISYM autoloading from theory `arithmetic` ... @@ -17751,7 +17787,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 @@ -17759,11 +17795,11 @@ Intermediate theorems generated: 26 REAL_OVER1 = |- !x. x / (& 1) = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 REAL_DIV_LZERO = |- !x. (& 0) / x = & 0 @@ -17775,7 +17811,7 @@ 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) @@ -17804,7 +17840,7 @@ Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 184 Theorem NOT_SUC autoloading from theory `num` ... @@ -17824,7 +17860,7 @@ 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) @@ -17836,7 +17872,7 @@ Intermediate theorems generated: 17 REAL_HALF_DOUBLE = |- !x. (x / (& 2)) + (x / (& 2)) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 51 REAL_DOWN = |- !x. (& 0) < x ==> (?y. (& 0) < y /\ y < x) @@ -17849,7 +17885,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -17861,11 +17897,11 @@ Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 38 REAL_LE_SUB_RADD = |- !x y z. (x - y) <= z = x <= (z + y) @@ -17873,7 +17909,7 @@ Intermediate theorems generated: 38 REAL_LT_NEG = |- !x y. (-- x) < (-- y) = y < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 REAL_LE_NEG = |- !x y. (-- x) <= (-- y) = y <= x @@ -17885,7 +17921,7 @@ Intermediate theorems generated: 73 REAL_SUB_LZERO = |- !x. (& 0) - x = -- x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_SUB_RZERO = |- !x. x - (& 0) = x @@ -17897,7 +17933,7 @@ Intermediate theorems generated: 58 REAL_LTE_ADD2 = |- !w x y z. w < x /\ y <= z ==> (w + y) < (x + z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 REAL_LET_ADD = |- !x y. (& 0) <= x /\ (& 0) < y ==> (& 0) < (x + y) @@ -17916,7 +17952,7 @@ Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -17928,7 +17964,7 @@ Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c @@ -17936,7 +17972,7 @@ Intermediate theorems generated: 93 REAL_EQ_SUB_LADD = |- !x y z. (x = y - z) = (x + z = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) @@ -17949,7 +17985,7 @@ Intermediate theorems generated: 142 REAL_LE_LMUL = |- !x y z. (& 0) < x ==> ((x * y) <= (x * z) = y <= z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) @@ -17959,7 +17995,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 @@ -17982,11 +18018,11 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> (x1 * y1) <= (x2 * y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 345 REAL_LE_LDIV = |- !x y z. (& 0) < x /\ y <= (z * x) ==> (y / x) <= z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 REAL_LE_RDIV = |- !x y z. (& 0) < x /\ (y * x) <= z ==> y <= (z / x) @@ -17994,7 +18030,7 @@ Intermediate theorems generated: 101 REAL_LT_1 = |- !x y. (& 0) <= x /\ x < y ==> (x / y) < (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 120 REAL_LE_LMUL_IMP = @@ -18008,7 +18044,7 @@ Intermediate theorems generated: 26 REAL_EQ_IMP_LE = |- !x y. (x = y) ==> x <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) @@ -18016,7 +18052,7 @@ Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) @@ -18024,7 +18060,7 @@ Intermediate theorems generated: 36 REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 Theorem FACT_LESS autoloading from theory `arithmetic` ... @@ -18032,7 +18068,7 @@ Run time: 0.0s REAL_FACT_NZ = |- !n. ~(&(FACT n) = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 25 REAL_DIFFSQ = |- !x y. (x + y) * (x - y) = (x * x) - (y * y) @@ -18040,7 +18076,7 @@ Intermediate theorems generated: 165 REAL_POSSQ = |- !x. (& 0) < (x * x) = ~(x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) @@ -18048,7 +18084,7 @@ Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 36 REAL_DIV_MUL2 = @@ -18073,7 +18109,7 @@ Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 @@ -18081,11 +18117,11 @@ Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 604 ABS_POS = |- !x. (& 0) <= (abs x) @@ -18110,7 +18146,7 @@ Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 105 ABS_ABS = |- !x. abs(abs x) = abs x @@ -18118,7 +18154,7 @@ Intermediate theorems generated: 27 ABS_LE = |- !x. x <= (abs x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 75 ABS_REFL = |- !x. (abs x = x) = (& 0) <= x @@ -18126,12 +18162,12 @@ Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 ABS_BETWEEN = |- !x y d. (& 0) < d /\ (x - d) < y /\ y < (x + d) = (abs(y - x)) < d -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) @@ -18139,7 +18175,7 @@ Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) @@ -18147,7 +18183,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -18155,16 +18191,16 @@ Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 41 ABS_CIRCLE = |- !x y h. (abs h) < ((abs y) - (abs x)) ==> (abs(x + h)) < (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 61 REAL_SUB_ABS = |- !x y. ((abs x) - (abs y)) <= (abs(x - y)) @@ -18172,7 +18208,7 @@ Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 80 ABS_BETWEEN2 = @@ -18181,15 +18217,15 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k -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.1s +Run time: 0.0s Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 @@ -18197,7 +18233,7 @@ 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) @@ -18205,12 +18241,12 @@ 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 = |- !e. (& 0) < e ==> (!n. ((& 1) + ((& n) * e)) <= (((& 1) + e) pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 298 Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... @@ -18226,7 +18262,7 @@ Intermediate theorems generated: 152 POW_1 = |- !x. x pow 1 = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x @@ -18234,7 +18270,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) @@ -18242,7 +18278,7 @@ Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -18250,7 +18286,7 @@ Intermediate theorems generated: 135 REAL_LE_POW2 = |- !x. (& 0) <= (x pow 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 @@ -18258,7 +18294,7 @@ 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) @@ -18270,7 +18306,7 @@ 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` ... @@ -18290,7 +18326,7 @@ Intermediate theorems generated: 103 POW_MINUS1 = |- !n. (--(& 1)) pow (2 num_mul n) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 231 REAL_SUP_SOMEPOS = @@ -18391,7 +18427,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (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: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18444,7 +18480,7 @@ Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 105 Theorem ADD_ASSOC autoloading from theory `arithmetic` ... @@ -18463,7 +18499,7 @@ |- !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 = @@ -18526,7 +18562,7 @@ Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) @@ -18593,13 +18629,13 @@ |- !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.1s +Run time: 0.0s Intermediate theorems generated: 2469 SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 () : void @@ -18609,7 +18645,7 @@ File real.ml loaded () : void -Run time: 8.8s +Run time: 1.4s Intermediate theorems generated: 23746 #\ @@ -18619,7 +18655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -18693,7 +18729,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s [] : (string # string) list Run time: 0.0s @@ -18703,7 +18739,7 @@ Intermediate theorems generated: 11 () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -18741,7 +18777,7 @@ Intermediate theorems generated: 16 COMPL_MEM = |- !S x. S x = ~re_compl S x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 23 SUBSET_ANTISYM = |- !P Q. P re_subset Q /\ Q re_subset P = (P = Q) @@ -18860,7 +18896,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 560 metric_tybij = @@ -18873,7 +18909,7 @@ Intermediate theorems generated: 20 METRIC_ZERO = |- !m x y. (dist m(x,y) = & 0) = (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 41 METRIC_SAME = |- !m x. dist m(x,x) = & 0 @@ -19053,7 +19089,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` ... @@ -19103,7 +19139,7 @@ File topology.ml loaded () : void -Run time: 0.9s +Run time: 0.1s Intermediate theorems generated: 4132 #\ @@ -19113,7 +19149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -19318,7 +19354,7 @@ Run time: 0.0s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 257 Definition re_subset autoloading from theory `TOPOLOGY` ... @@ -19585,7 +19621,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> bounded(mr1,g)(\n. inv(x n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 493 NET_NULL_ADD = @@ -19696,7 +19732,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 = @@ -19838,7 +19874,7 @@ File nets.ml loaded () : void -Run time: 0.5s +Run time: 0.3s Intermediate theorems generated: 7389 #\ @@ -19848,7 +19884,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -19922,7 +19958,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -19953,7 +19989,7 @@ Intermediate theorems generated: 34 () : void -Run time: 0.1s +Run time: 0.0s [(); ()] : void list Run time: 0.0s @@ -20033,7 +20069,7 @@ SEQ_ADD = |- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. (x n) + (y n)) --> (x0 + y0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 Theorem NET_MUL autoloading from theory `NETS` ... @@ -20090,7 +20126,7 @@ SEQ_SUB = |- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. (x n) - (y n)) --> (x0 - y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 Theorem NET_DIV autoloading from theory `NETS` ... @@ -20154,7 +20190,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 @@ -20173,7 +20209,7 @@ Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 182 mono = @@ -20207,7 +20243,7 @@ MONO_SUC = |- !f. mono f = (!n. (f(SUC n)) >= (f n)) \/ (!n. (f(SUC n)) <= (f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 528 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -20231,7 +20267,7 @@ Run time: 0.0s MAX_LEMMA = |- !s N. ?k. !n. n num_lt N ==> (abs(s n)) < k -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 241 Theorem REAL_LTE_TRANS autoloading from theory `REAL` ... @@ -20286,7 +20322,7 @@ Definition abs autoloading from theory `REAL` ... abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem REAL_LT_01 autoloading from theory `REAL` ... @@ -20370,7 +20406,7 @@ Run time: 0.0s SEQ_NEG_CONV = |- !f. convergent f = convergent(\n. --(f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 72 Theorem ABS_NEG autoloading from theory `REAL` ... @@ -20616,7 +20652,7 @@ Run time: 0.0s SEQ_POWER_ABS = |- !c. (abs c) < (& 1) ==> (\n. (abs c) pow n) --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 573 Theorem POW_ABS autoloading from theory `REAL` ... @@ -20653,7 +20689,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20667,7 +20703,7 @@ (!n. (f n) <= (g n)) /\ (\n. (f n) - (g n)) --> (& 0) ==> (?l. ((!n. (f n) <= l) /\ f --> l) /\ (!n. l <= (g n)) /\ g --> l) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 295 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -20733,7 +20769,7 @@ Theorem REAL_NEG_ADD autoloading from theory `REAL` ... REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.1s +Run time: 0.0s Theorem REAL_DOUBLE autoloading from theory `REAL` ... REAL_DOUBLE = |- !x. x + x = (& 2) * x @@ -20784,7 +20820,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.4s +Run time: 0.1s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20800,7 +20836,7 @@ Intermediate theorems generated: 2 SUM_SUMMABLE = |- !f l. f sums l ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 16 SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) @@ -20831,7 +20867,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` ... @@ -20850,7 +20886,7 @@ Theorem Sum autoloading from theory `REAL` ... Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.1s +Run time: 0.0s SER_POS_LT = |- !f n. @@ -20887,7 +20923,7 @@ |- !f k. summable f /\ 0 num_lt k ==> (\n. Sum(n num_mul k,k)f) sums (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 258 Theorem MULT_SYM autoloading from theory `arithmetic` ... @@ -20909,7 +20945,7 @@ |- !f. summable f ==> (!k. (\n. f(n num_add k)) sums ((suminf f) - (Sum(0,k)f))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 299 Theorem REAL_EQ_IMP_LE autoloading from theory `REAL` ... @@ -20928,7 +20964,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -20947,7 +20983,7 @@ Run time: 0.0s SER_CMUL = |- !x x0 c. x sums x0 ==> (\n. c * (x n)) sums (c * x0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 82 Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... @@ -20980,7 +21016,7 @@ Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 Theorem SUM_LE autoloading from theory `REAL` ... @@ -21023,7 +21059,7 @@ |- !f g. (!n. (abs(f n)) <= (g n)) /\ summable g ==> summable f /\ (suminf f) <= (suminf g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 136 Theorem SUM_ABS autoloading from theory `REAL` ... @@ -21042,7 +21078,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` ... @@ -21065,7 +21101,7 @@ |- !x. ~(x = & 1) ==> (!n. Sum(0,n)(\n'. x pow n') = ((x pow n) - (& 1)) / (x - (& 1))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 411 Theorem REAL_NEG_INV autoloading from theory `REAL` ... @@ -21085,7 +21121,7 @@ Run time: 0.0s GP = |- !x. (abs x) < (& 1) ==> (\n. x pow n) sums (inv((& 1) - x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 343 Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... @@ -21102,7 +21138,7 @@ ABS_NEG_LEMMA = |- !c. c <= (& 0) ==> (!x y. (abs x) <= (c * (abs y)) ==> (x = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 114 Theorem REAL_LE_LMUL autoloading from theory `REAL` ... @@ -21126,13 +21162,13 @@ Intermediate theorems generated: 683 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File seq.ml loaded () : void -Run time: 3.9s +Run time: 0.6s Intermediate theorems generated: 18704 #\ @@ -21142,7 +21178,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -21216,7 +21252,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -21244,7 +21280,7 @@ Intermediate theorems generated: 43 () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -21321,7 +21357,7 @@ |- !m x y z. tendsto(m,x)y z = (& 0) < (dist m(x,y)) /\ (dist m(x,y)) <= (dist m(x,z)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem METRIC_SAME autoloading from theory `TOPOLOGY` ... @@ -21446,7 +21482,7 @@ Intermediate theorems generated: 23 LIM_X = |- !x0. ((\x. x) --> x0)x0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 52 Theorem MTOP_TENDS_UNIQ autoloading from theory `NETS` ... @@ -21469,7 +21505,7 @@ Theorem REAL_LT_TRANS autoloading from theory `REAL` ... REAL_LT_TRANS = |- !x y z. x < y /\ y < z ==> x < z -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_ADD2 autoloading from theory `REAL` ... REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) @@ -21511,7 +21547,7 @@ LIM_TRANSFORM = |- !f g x0 l. ((\x. (f x) - (g x)) --> (& 0))x0 /\ (g --> l)x0 ==> (f --> l)x0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 473 diffl = @@ -21540,7 +21576,7 @@ Run time: 0.0s DIFF_CONT = |- !f l x. (f diffl l)x ==> f contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 290 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -21556,7 +21592,7 @@ Intermediate theorems generated: 275 CONT_CONST = |- !x. (\x. k) contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 CONT_ADD = |- !x. f contl x /\ g contl x ==> (\x. (f x) + (g x)) contl x @@ -21583,7 +21619,7 @@ |- !x. f contl x /\ g contl x /\ ~(g x = & 0) ==> (\x. (f x) / (g x)) contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 31 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -21654,7 +21690,7 @@ Theorem REAL_LE_TOTAL autoloading from theory `REAL` ... REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x -Run time: 0.1s +Run time: 0.0s Theorem BOLZANO_LEMMA autoloading from theory `SEQ` ... BOLZANO_LEMMA = @@ -21672,7 +21708,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.3s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21706,7 +21742,7 @@ Run time: 0.0s DIFF_CONST = |- !k x. ((\x. k) diffl (& 0))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 59 Theorem REAL_RDISTRIB autoloading from theory `REAL` ... @@ -21756,7 +21792,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) * (g x)) diffl ((l * (g x)) + (m * (f x))))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 567 DIFF_CMUL = @@ -21834,7 +21870,7 @@ ((f(g(x + h))) - (f(g x))) / h = (((f(g(x + h))) - (f(g x))) / ((g(x + h)) - (g x))) * (((g(x + h)) - (g x)) / h) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 170 Theorem REAL_LT_RADD autoloading from theory `REAL` ... @@ -21872,7 +21908,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.0s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21880,7 +21916,7 @@ Run time: 0.0s DIFF_X = |- !x. ((\x. x) diffl (& 1))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 148 Theorem REAL_MUL_RID autoloading from theory `REAL` ... @@ -21955,7 +21991,7 @@ DIFF_XM1 = |- !x. ~(x = & 0) ==> ((\x. inv x) diffl (--((inv x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 818 Theorem POW_INV autoloading from theory `REAL` ... @@ -22029,7 +22065,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22049,7 +22085,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` ... @@ -22086,7 +22122,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22095,7 +22131,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` ... @@ -22123,7 +22159,7 @@ Theorem REAL_NEG_INV autoloading from theory `REAL` ... REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) -Run time: 0.1s +Run time: 0.0s Theorem REAL_NEG_LT0 autoloading from theory `REAL` ... REAL_NEG_LT0 = |- !x. (-- x) < (& 0) = (& 0) < x @@ -22149,7 +22185,7 @@ (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: 572 Theorem REAL_NEG_EQ0 autoloading from theory `REAL` ... @@ -22176,7 +22212,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -22194,7 +22230,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.0s Intermediate theorems generated: 3178 gfn = "\x. (f x) - ((((f b) - (f a)) / (b - a)) * x)" : term @@ -22212,7 +22248,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -22226,7 +22262,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.2s +Run time: 0.0s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22244,7 +22280,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (!x. a <= x /\ x <= b ==> (f x = f a)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 310 DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) @@ -22252,13 +22288,13 @@ Intermediate theorems generated: 172 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File lim.ml loaded () : void -Run time: 5.3s +Run time: 0.5s Intermediate theorems generated: 21608 #\ @@ -22268,7 +22304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -22343,7 +22379,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -22373,11 +22409,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 47 () : void -Run time: 0.1s +Run time: 0.0s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22480,7 +22516,7 @@ Theorem SUB_0 autoloading from theory `arithmetic` ... SUB_0 = |- !m. (0 num_sub m = 0) /\ (m num_sub 0 = m) -Run time: 0.1s +Run time: 0.0s Theorem REAL_ADD_LID autoloading from theory `REAL` ... REAL_ADD_LID = |- !x. (& 0) + x = x @@ -22530,7 +22566,7 @@ |- !n x y. Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p))) = Sum(0,SUC n)(\p. (x pow (n num_sub p)) * (y pow p)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 235 Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... @@ -22663,7 +22699,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.1s +Run time: 0.0s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22702,7 +22738,7 @@ Sum(0,n)(\n'. (diffs c n') * (x pow n')) = (Sum(0,n)(\n'. (& n') * ((c n') * (x pow (n' num_sub 1))))) + ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 229 Theorem REAL_EQ_SUB_LADD autoloading from theory `REAL` ... @@ -22746,7 +22782,7 @@ summable(\n. (diffs c n) * (x pow n)) ==> (\n. (& n) * ((c n) * (x pow (n num_sub 1)))) sums (suminf(\n. (diffs c n) * (x pow n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 180 Theorem SUB_ADD autoloading from theory `arithmetic` ... @@ -22868,7 +22904,7 @@ Theorem REAL_LE_LT autoloading from theory `REAL` ... REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) -Run time: 0.1s +Run time: 0.0s Theorem POW_POS autoloading from theory `REAL` ... POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) @@ -22911,7 +22947,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.0s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22966,7 +23002,7 @@ Theorem REAL_LT_HALF1 autoloading from theory `REAL` ... REAL_LT_HALF1 = |- !d. (& 0) < (d / (& 2)) = (& 0) < d -Run time: 0.1s +Run time: 0.0s Theorem LIM autoloading from theory `LIM` ... LIM = @@ -22986,7 +23022,7 @@ (& 0) < k /\ (!h. (& 0) < (abs h) /\ (abs h) < k ==> (abs(f h)) <= (K * (abs h))) ==> (f tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 917 Theorem SER_LE autoloading from theory `SEQ` ... @@ -23018,7 +23054,7 @@ (& 0) < (abs h) /\ (abs h) < k ==> (!n. (abs(g h n)) <= ((f n) * (abs h)))) ==> ((\h. suminf(g h)) tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 502 Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... @@ -23052,7 +23088,7 @@ Theorem ABS_N autoloading from theory `REAL` ... ABS_N = |- !n. abs(& n) = & n -Run time: 0.1s +Run time: 0.0s Theorem ABS_REFL autoloading from theory `REAL` ... ABS_REFL = |- !x. (abs x = x) = (& 0) <= x @@ -23120,7 +23156,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.3s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -23130,7 +23166,7 @@ File powser.ml loaded () : void -Run time: 2.8s +Run time: 0.3s Intermediate theorems generated: 8507 #\ @@ -23140,7 +23176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -23215,7 +23251,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s false : bool Run time: 0.0s @@ -23226,7 +23262,7 @@ Theory POWSER loaded () : void -Run time: 0.3s +Run time: 0.1s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -23304,11 +23340,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 () : void -Run time: 0.1s +Run time: 0.0s basic_diffs = [] : thm list Run time: 0.0s @@ -23334,7 +23370,7 @@ Theorem DIFF_NEG autoloading from theory `LIM` ... DIFF_NEG = |- !f l x. (f diffl l)x ==> ((\x. --(f x)) diffl (-- l))x -Run time: 0.1s +Run time: 0.0s Theorem DIFF_SUB autoloading from theory `LIM` ... DIFF_SUB = @@ -23566,7 +23602,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` ... @@ -23622,7 +23658,7 @@ n) * (x pow n)) sums (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 272 COS_CONVERGES = @@ -23640,7 +23676,7 @@ Theorem REAL_EQ_RMUL autoloading from theory `REAL` ... REAL_EQ_RMUL = |- !x y z. (x * z = y * z) = (z = & 0) \/ (x = y) -Run time: 0.1s +Run time: 0.0s Definition diffs autoloading from theory `POWSER` ... diffs = |- !c. diffs c = (\n. (&(SUC n)) * (c(SUC n))) @@ -23667,7 +23703,7 @@ & 0 | ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) = (\n. (EVEN n => ((--(& 1)) pow (n DIV 2)) / (&(FACT n)) | & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 361 Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... @@ -23751,7 +23787,7 @@ Intermediate theorems generated: 144 DIFF_SIN = |- !x. (sin diffl (cos x))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 200 Theorem DIFFS_NEG autoloading from theory `POWSER` ... @@ -23869,7 +23905,7 @@ 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 @@ -23917,7 +23953,7 @@ Run time: 0.0s EXP_POS_LT = |- !x. (& 0) < (exp x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 38 Theorem REAL_RDISTRIB autoloading from theory `REAL` ... @@ -23957,7 +23993,7 @@ Run time: 0.0s EXP_MONO_LT = |- !x y. (exp x) < (exp y) = x < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 85 EXP_MONO_LE = |- !x y. (exp x) <= (exp y) = x <= y @@ -24016,7 +24052,7 @@ Run time: 0.0s EXP_TOTAL = |- !y. (& 0) < y ==> (?x. exp x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 134 ln = |- !x. ln x = (@u. exp u = x) @@ -24041,7 +24077,7 @@ Intermediate theorems generated: 113 LN_INJ = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x = ln y) = (x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 53 LN_1 = |- ln(& 1) = & 0 @@ -24071,7 +24107,7 @@ LN_MONO_LE = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x) <= (ln y) = x <= y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 53 LN_POW = |- !n x. (& 0) < x ==> (ln(x pow n) = (& n) * (ln x)) @@ -24098,7 +24134,7 @@ ROOT_LN = |- !n x. (& 0) < x ==> (!n. root(SUC n)x = exp((ln x) / (&(SUC n)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 282 Theorem REAL_ENTIRE autoloading from theory `REAL` ... @@ -24160,11 +24196,11 @@ Run time: 0.0s COS_0 = |- cos(& 0) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 690 Theorem REAL_ADD_RINV autoloading from theory `REAL` ... @@ -24200,7 +24236,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` ... @@ -24216,7 +24252,7 @@ Run time: 0.0s COS_BOUND = |- !x. (abs(cos x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 160 COS_BOUNDS = |- !x. (--(& 1)) <= (cos x) /\ (cos x) <= (& 1) @@ -24252,7 +24288,7 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.3s +Run time: 0.0s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -24273,7 +24309,7 @@ COS_ADD = |- !x y. cos(x + y) = ((cos x) * (cos y)) - ((sin x) * (sin y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 51 Theorem REAL_LNEG_UNIQ autoloading from theory `REAL` ... @@ -24293,7 +24329,7 @@ Run time: 0.0s SIN_DOUBLE = |- !x. sin((& 2) * x) = (& 2) * ((sin x) * (cos x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 COS_DOUBLE = |- !x. cos((& 2) * x) = ((cos x) pow 2) - ((sin x) pow 2) @@ -24369,7 +24405,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.3s +Run time: 0.0s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24394,7 +24430,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.1s +Run time: 0.0s Theorem REAL_ADD_LINV autoloading from theory `REAL` ... REAL_ADD_LINV = |- !x. (-- x) + x = & 0 @@ -24409,7 +24445,7 @@ Run time: 0.0s COS_2 = |- (cos(& 2)) < (& 0) -Run time: 0.5s +Run time: 0.1s Intermediate theorems generated: 3794 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -24461,7 +24497,7 @@ Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 PI2 = |- pi / (& 2) = (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24473,7 +24509,7 @@ Intermediate theorems generated: 42 PI2_BOUNDS = |- (& 0) < (pi / (& 2)) /\ (pi / (& 2)) < (& 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 124 Theorem REAL_LT_ADD autoloading from theory `REAL` ... @@ -24493,7 +24529,7 @@ Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -24509,7 +24545,7 @@ Intermediate theorems generated: 79 SIN_COS = |- !x. sin x = cos((pi / (& 2)) - x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 66 COS_SIN = |- !x. cos x = sin((pi / (& 2)) - x) @@ -24537,7 +24573,7 @@ Intermediate theorems generated: 134 SIN_NPI = |- !n. sin((& n) * pi) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 137 SIN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (sin x) @@ -24545,7 +24581,7 @@ Intermediate theorems generated: 53 COS_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 450 Theorem REAL_LT_NEG autoloading from theory `REAL` ... @@ -24570,14 +24606,14 @@ Run time: 0.0s SIN_POS_PI = |- !x. (& 0) < x /\ x < pi ==> (& 0) < (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 96 COS_TOTAL = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (& 0) <= x /\ x <= pi /\ (cos x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 766 Theorem REAL_EQ_RADD autoloading from theory `REAL` ... @@ -24608,7 +24644,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 431 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -24642,7 +24678,7 @@ |- !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` ... @@ -24674,7 +24710,7 @@ Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... EVEN_EXISTS = |- !n. EVEN n = (?m. n = 2 num_mul m) -Run time: 0.1s +Run time: 0.0s Theorem REAL_NEG_GE0 autoloading from theory `REAL` ... REAL_NEG_GE0 = |- !x. (& 0) <= (-- x) = x <= (& 0) @@ -24693,7 +24729,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 @@ -24709,7 +24745,7 @@ Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 Theorem REAL_LDISTRIB autoloading from theory `REAL` ... @@ -24748,7 +24784,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24794,13 +24830,13 @@ 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 = |- !y. (& 0) <= y ==> (?x. (& 0) <= x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 372 Theorem POW_NZ autoloading from theory `REAL` ... @@ -24821,7 +24857,7 @@ TAN_TOTAL = |- !y. ?! x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y) -Run time: 0.2s +Run time: 0.0s Intermediate theorems generated: 1301 asn = @@ -24839,7 +24875,7 @@ |- !y. atn y = (@x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ASN = @@ -24859,19 +24895,19 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 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 = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi /\ (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) @@ -24885,7 +24921,7 @@ Intermediate theorems generated: 17 COS_ACS = |- !x. (& 0) <= x /\ x <= pi ==> (acs(cos x) = x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 86 ATN = @@ -24901,7 +24937,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 TAN_ATN = @@ -24910,13 +24946,13 @@ Intermediate theorems generated: 103 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File transc.ml loaded () : void -Run time: 8.2s +Run time: 0.8s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24929,7 +24965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24951,7 +24987,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25017,7 +25053,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25049,7 +25085,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25158,7 +25194,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25311,7 +25347,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25384,7 +25420,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25464,7 +25500,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25621,7 +25657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25776,7 +25812,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25993,7 +26029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26015,7 +26051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26034,7 +26070,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26079,7 +26115,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26144,7 +26180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26194,7 +26230,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26264,7 +26300,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26334,7 +26370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26370,7 +26406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26423,7 +26459,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26495,7 +26531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26574,7 +26610,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26769,7 +26805,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26806,7 +26842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -27492,7 +27528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -27964,7 +28000,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -28228,7 +28264,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -28473,7 +28509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -28937,7 +28973,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29405,7 +29441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29461,7 +29497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29551,7 +29587,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29750,7 +29786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29782,7 +29818,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29916,7 +29952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30219,7 +30255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30251,7 +30287,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30290,7 +30326,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30322,7 +30358,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30483,7 +30519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30616,7 +30652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30805,7 +30841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30865,7 +30901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30990,7 +31026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31101,7 +31137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31126,7 +31162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31154,7 +31190,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31267,7 +31303,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31770,7 +31806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32018,7 +32054,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32244,7 +32280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32286,7 +32322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32318,7 +32354,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32541,7 +32577,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32934,7 +32970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33047,7 +33083,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33550,7 +33586,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33798,7 +33834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34024,7 +34060,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34059,7 +34095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34098,7 +34134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34135,7 +34171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34156,7 +34192,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34253,7 +34289,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34275,7 +34311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34771,7 +34807,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34794,7 +34830,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34872,7 +34908,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34931,7 +34967,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34975,7 +35011,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34993,7 +35029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35020,7 +35056,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35064,7 +35100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35177,7 +35213,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35224,7 +35260,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35263,7 +35299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35337,7 +35373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35426,7 +35462,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35497,7 +35533,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35567,7 +35603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35616,7 +35652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35657,7 +35693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35698,7 +35734,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35722,7 +35758,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35823,7 +35859,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35844,7 +35880,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35869,7 +35905,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36495,7 +36531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36572,7 +36608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36599,7 +36635,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36716,7 +36752,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36811,7 +36847,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36897,7 +36933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37012,7 +37048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37105,7 +37141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37281,7 +37317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37385,7 +37421,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37680,7 +37716,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37783,7 +37819,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37851,7 +37887,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37913,7 +37949,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38093,7 +38129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38134,7 +38170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38164,7 +38200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38190,7 +38226,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38708,7 +38744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -39245,7 +39281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -39433,7 +39469,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -39451,10 +39487,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sat Jan 6 06:46:25 -12 2024 +Sat Feb 8 16:01:28 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 6 06:46:26 -12 2024 +Sat Feb 8 16:01:28 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39474,20 +39510,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39835,7 +39871,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (112 pages, 316556 bytes). +Output written on tutorial.dvi (112 pages, 316560 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' @@ -41219,12 +41255,12 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 999968 bytes). +Output written on description.dvi (346 pages, 999972 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -42990,7 +43026,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44734,7 +44770,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44989,7 +45025,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45226,7 +45262,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45404,7 +45440,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45593,7 +45629,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45712,7 +45748,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45828,7 +45864,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46068,7 +46104,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46409,7 +46445,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46616,7 +46652,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46959,7 +46995,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47151,7 +47187,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47419,7 +47455,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47580,7 +47616,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47725,7 +47761,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47877,7 +47913,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48033,7 +48069,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48211,7 +48247,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48407,7 +48443,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48632,7 +48668,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48894,7 +48930,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:0706' -> endpages.ps +' TeX output 2025.02.08:1603' -> endpages.ps @@ -48958,7 +48994,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:0706' -> titlepages.ps +' TeX output 2025.02.08:1603' -> titlepages.ps @@ -49031,8 +49067,8 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install find ml -type f -name "*ml" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install @@ -49106,13 +49142,13 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.changes @@ -49121,12 +49157,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/206875/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/206875/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/844868 and its subdirectories -I: Current time: Sat Jan 6 07:30:57 -12 2024 -I: pbuilder-time-stamp: 1704569457 +I: removing directory /srv/workspace/pbuilder/206875 and its subdirectories +I: Current time: Sat Feb 8 16:04:30 +14 2025 +I: pbuilder-time-stamp: 1738980270