Diff of the two buildlogs: -- --- b1/build.log 2024-01-07 15:58:03.209834525 +0000 +++ b2/build.log 2024-01-07 16:06:56.468316754 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Jan 7 03:43:19 -12 2024 -I: pbuilder-time-stamp: 1704642199 +I: Current time: Sun Feb 9 12:21:05 +14 2025 +I: pbuilder-time-stamp: 1739053265 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/1375620/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3870031/tmp/hooks/D01_modify_environment starting +debug: Running on codethink03-arm64. +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 22:21 /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/3870031/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3870031/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='arm64' - DEBIAN_FRONTEND='noninteractive' + 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]="aarch64-unknown-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=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='a6e2c39284e44cdcab6bb166ece6e738' - 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='1375620' - PS1='# ' - PS2='> ' + INVOCATION_ID=333876c0ba7a42cf92fc592517629098 + LANG=C + LANGUAGE=nl_BE:nl + LC_ALL=C + MACHTYPE=aarch64-unknown-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=3870031 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.Pj0yUx29/pbuilderrc_Ea48 --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.Pj0yUx29/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.104: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.Pj0yUx29/pbuilderrc_Tqip --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.Pj0yUx29/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://192.168.101.104:3128 I: uname -a - Linux codethink04-arm64 6.1.0-17-cloud-arm64 #1 SMP Debian 6.1.69-1 (2023-12-30) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-17-cloud-arm64 #1 SMP Debian 6.1.69-1 (2023-12-30) aarch64 GNU/Linux I: ls -l /bin total 7104 -rwxr-xr-x 1 root root 1346480 Apr 23 2023 bash @@ -128,15 +160,15 @@ -rwxr-xr-x 1 root root 68456 Sep 20 2022 readlink -rwxr-xr-x 1 root root 68592 Sep 20 2022 rm -rwxr-xr-x 1 root root 68480 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 68392 Jul 28 23:46 run-parts + -rwxr-xr-x 1 root root 68392 Jul 28 2023 run-parts -rwxr-xr-x 1 root root 134536 Jan 5 2023 sed - lrwxrwxrwx 1 root root 4 Jan 5 2023 sh -> dash + lrwxrwxrwx 1 root root 9 Feb 8 22:21 sh -> /bin/bash -rwxr-xr-x 1 root root 68432 Sep 20 2022 sleep -rwxr-xr-x 1 root root 134088 Sep 20 2022 stty -rwsr-xr-x 1 root root 133312 Mar 23 2023 su -rwxr-xr-x 1 root root 68448 Sep 20 2022 sync -rwxr-xr-x 1 root root 539896 Apr 6 2023 tar - -rwxr-xr-x 1 root root 67904 Jul 28 23:46 tempfile + -rwxr-xr-x 1 root root 67904 Jul 28 2023 tempfile -rwxr-xr-x 1 root root 134160 Sep 20 2022 touch -rwxr-xr-x 1 root root 68384 Sep 20 2022 true -rwxr-xr-x 1 root root 67664 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/1375620/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/3870031/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -378,7 +410,7 @@ Get: 180 http://deb.debian.org/debian bookworm/main arm64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 181 http://deb.debian.org/debian bookworm/main arm64 texlive-base all 2022.20230122-3 [21.9 MB] Get: 182 http://deb.debian.org/debian bookworm/main arm64 texlive-latex-base all 2022.20230122-3 [1182 kB] -Fetched 173 MB in 1s (227 MB/s) +Fetched 173 MB in 1s (181 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libargon2-1:arm64. (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 ... 18171 files and directories currently installed.) @@ -988,8 +1020,8 @@ Setting up tzdata (2023c-5+deb12u1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Jan 7 15:44:06 UTC 2024. -Universal Time is now: Sun Jan 7 15:44:06 UTC 2024. +Local time is now: Sat Feb 8 22:21:36 UTC 2025. +Universal Time is now: Sat Feb 8 22:21:36 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libdconf1:arm64 (0.40.0-4) ... @@ -1176,7 +1208,11 @@ fakeroot is already the newest version (1.31-1.2). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/3870031/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bookworm +I: user script /srv/workspace/pbuilder/3870031/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 @@ -1569,7 +1605,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 03:45:31 -12 2024 +Sun Feb 9 12:22:20 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2807,7 +2843,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 # mem = - : (* -> * list -> bool) @@ -2945,7 +2981,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #.............start address -T 0xc2e440 () : void @@ -3104,7 +3140,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #.............start address -T 0xc2e440 () : void @@ -3296,7 +3332,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 # concat = - : (string -> string -> string) @@ -3406,7 +3442,7 @@ start address -T 0xc23c60 ;; Finished loading "lisp/f-ol-net" start address -T 0xa48c30 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 7/1/24 + version 2.02 (GCL) created 9/2/25 #...start address -T 0xbb5600 () : void @@ -3735,7 +3771,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 ###########################() : void @@ -3748,7 +3784,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 ################################################################################################() : void @@ -3893,7 +3929,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 ############################() : void @@ -3936,7 +3972,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 ############################Theory ind loaded () : void @@ -3973,7 +4009,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4014,7 +4050,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4416,7 +4452,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4484,7 +4520,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4689,7 +4725,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4813,7 +4849,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4899,7 +4935,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -4992,7 +5028,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5061,7 +5097,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5166,7 +5202,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5401,7 +5437,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5427,7 +5463,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5555,7 +5591,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5603,7 +5639,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5670,7 +5706,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5729,7 +5765,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5785,7 +5821,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/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) @@ -5798,7 +5834,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #() : void @@ -5850,7 +5886,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ##########################() : void @@ -5881,7 +5917,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ##############################() : void @@ -5968,7 +6004,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #######################################################################() : void @@ -6121,7 +6157,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ###########################() : void @@ -6156,7 +6192,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #############################() : void @@ -6217,7 +6253,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ###########################Theory arithmetic loaded () : void @@ -6712,7 +6748,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ##################################() : void @@ -6859,7 +6895,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #################################Theory list loaded () : void @@ -7198,7 +7234,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ###############################Theory list loaded () : void @@ -8695,7 +8731,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #############################() : void @@ -9079,7 +9115,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ############################() : void @@ -9377,7 +9413,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ############################() : void @@ -9517,7 +9553,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ############################################() : void @@ -9614,7 +9650,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 ##################################() : void @@ -9644,7 +9680,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -9661,7 +9697,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #Theory num loaded () : void @@ -9680,7 +9716,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -9837,7 +9873,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 # @@ -9875,7 +9911,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 # @@ -9909,7 +9945,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -9994,7 +10030,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -10035,7 +10071,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -10219,7 +10255,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10295,7 +10331,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/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) @@ -10308,7 +10344,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #() : void @@ -10372,11 +10408,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 03:48:41 -12 2024 +Sun Feb 9 12:24:32 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 03:48:41 -12 2024 +Sun Feb 9 12:24:32 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10399,7 +10435,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -10483,7 +10519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -10589,7 +10625,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11339,7 +11375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11362,7 +11398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11405,7 +11441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11441,7 +11477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11493,7 +11529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11525,7 +11561,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11563,7 +11599,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11591,7 +11627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11668,7 +11704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11690,7 +11726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11744,7 +11780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11793,7 +11829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11944,7 +11980,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -11988,7 +12024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12063,7 +12099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12113,7 +12149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12176,7 +12212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12229,7 +12265,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12275,7 +12311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12363,7 +12399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12401,7 +12437,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12462,7 +12498,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12526,7 +12562,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12552,7 +12588,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12577,7 +12613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12616,7 +12652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -12692,7 +12728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13429,7 +13465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13452,7 +13488,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13495,7 +13531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13530,7 +13566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13571,7 +13607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13634,7 +13670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13657,7 +13693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13682,7 +13718,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13709,7 +13745,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -13745,7 +13781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14277,7 +14313,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14300,7 +14336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14334,7 +14370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14389,7 +14425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14480,7 +14516,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14649,7 +14685,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -14902,7 +14938,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (?f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 444 WO_RECURSE = @@ -15031,7 +15067,7 @@ |- !l a. fl(\(x,y). l(x,y) \/ (y = a) /\ (fl l x \/ (x = a)))x = fl l x \/ (x = a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -15040,7 +15076,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -15121,7 +15157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -15252,7 +15288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -15344,7 +15380,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -15436,12 +15472,12 @@ Run time: 0.0s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sun Jan 7 03:49:57 -12 2024 +===> abs_theory rebuilt on Sun Feb 9 12:25:25 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -15614,7 +15650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -15882,7 +15918,7 @@ Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 @@ -15918,7 +15954,7 @@ 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` ... @@ -16032,7 +16068,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -16041,7 +16077,7 @@ File hrat.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 11032 #\ @@ -16051,7 +16087,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -16447,12 +16483,12 @@ isacut (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 502 HREAL_ADD_ISACUT = |- !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 = @@ -16561,7 +16597,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -16901,7 +16937,7 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16913,7 +16949,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 @@ -17109,7 +17145,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -17465,7 +17501,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) @@ -17537,7 +17573,7 @@ Intermediate theorems generated: 50 REAL_SUB_ADD2 = |- !x y. y + (x - y) = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 16 REAL_SUB_REFL = |- !x. x - x = & 0 @@ -17633,7 +17669,7 @@ Intermediate theorems generated: 18 REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 REAL_LT_RMUL = |- !x y z. (& 0) < z ==> ((x * z) < (y * z) = x < y) @@ -17705,7 +17741,7 @@ Run time: 0.0s REAL_LE = |- !m n. (& m) <= (& n) = m num_le n -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -17915,7 +17951,7 @@ Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 23 REAL_SUB_RNEG = |- !x y. x - (-- y) = x + y @@ -17958,7 +17994,7 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y @@ -18068,7 +18104,7 @@ Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 @@ -18080,7 +18116,7 @@ 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) @@ -18150,7 +18186,7 @@ Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) @@ -18184,7 +18220,7 @@ 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 @@ -18237,7 +18273,7 @@ Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -18303,7 +18339,7 @@ Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 SUP_LEMMA3 = @@ -18346,7 +18382,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 15 REAL_SUP_UBOUND_LE = @@ -18467,7 +18503,7 @@ Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) @@ -18588,7 +18624,7 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2469 SUM_CANCEL = @@ -18604,7 +18640,7 @@ File real.ml loaded () : void -Run time: 0.9s +Run time: 0.8s Intermediate theorems generated: 23746 #\ @@ -18614,7 +18650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -19108,7 +19144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -19482,7 +19518,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19833,7 +19869,7 @@ File nets.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 7389 #\ @@ -19843,7 +19879,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -20310,7 +20346,7 @@ Intermediate theorems generated: 1 SEQ_CBOUNDED = |- !f. cauchy f ==> bounded(mr1,$num_ge)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 110 Theorem REAL_LE_RADD autoloading from theory `REAL` ... @@ -20378,7 +20414,7 @@ Intermediate theorems generated: 39 SEQ_BCONV = |- !f. bounded(mr1,$num_ge)f /\ mono f ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... @@ -20604,7 +20640,7 @@ Theorem POW_NZ autoloading from theory `REAL` ... POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE_LT autoloading from theory `REAL` ... REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) @@ -20687,7 +20723,7 @@ Theorem REAL_MUL_RZERO autoloading from theory `REAL` ... REAL_MUL_RZERO = |- !x. x * (& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Theorem REAL_NEG_0 autoloading from theory `REAL` ... REAL_NEG_0 = |- --(& 0) = & 0 @@ -20839,7 +20875,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) <= (f m)) ==> (Sum(0,n)f) <= (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 220 Theorem Sum autoloading from theory `REAL` ... @@ -20942,7 +20978,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` ... @@ -21127,7 +21163,7 @@ File seq.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 18704 #\ @@ -21137,7 +21173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -21535,7 +21571,7 @@ Run time: 0.0s DIFF_CONT = |- !f l x. (f diffl l)x ==> f contl x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 290 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -21547,7 +21583,7 @@ Run time: 0.0s CONTL_LIM = |- !f x. f contl x = (f --> (f x))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 275 CONT_CONST = |- !x. (\x. k) contl x @@ -22081,7 +22117,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22090,7 +22126,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -22230,7 +22266,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -22253,7 +22289,7 @@ File lim.ml loaded () : void -Run time: 0.4s +Run time: 0.3s Intermediate theorems generated: 21608 #\ @@ -22263,7 +22299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -22490,7 +22526,7 @@ |- !n x y. (x pow (SUC n)) - (y pow (SUC n)) = (x - y) * (Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 485 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -22995,7 +23031,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 Theorem SUM_SUMMABLE autoloading from theory `SEQ` ... SUM_SUMMABLE = |- !f l. f sums l ==> summable f @@ -23125,7 +23161,7 @@ File powser.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 8507 #\ @@ -23135,7 +23171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -23303,7 +23339,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23417,7 +23453,7 @@ Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... LESS_EQ_SUC_REFL = |- !m. m num_le (SUC m) -Run time: 0.1s +Run time: 0.0s Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... LESS_EQ_TRANS = |- !m n p. m num_le n /\ n num_le p ==> m num_le p @@ -23860,7 +23896,7 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 @@ -23932,7 +23968,7 @@ Intermediate theorems generated: 152 EXP_SUB = |- !x y. exp(x - y) = (exp x) / (exp y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 38 Theorem REAL_LT_RMUL autoloading from theory `REAL` ... @@ -24236,7 +24272,7 @@ Theorem REAL_SUB_REFL autoloading from theory `REAL` ... REAL_SUB_REFL = |- !x. x - x = & 0 -Run time: 0.0s +Run time: 0.1s Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... REAL_SUB_RZERO = |- !x. x - (& 0) = x @@ -24572,7 +24608,7 @@ |- !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` ... @@ -24603,7 +24639,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 431 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -24924,7 +24960,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -24946,7 +24982,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25012,7 +25048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25044,7 +25080,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25153,7 +25189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25306,7 +25342,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25379,7 +25415,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25459,7 +25495,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25616,7 +25652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25771,7 +25807,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -25988,7 +26024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26010,7 +26046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26029,7 +26065,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26074,7 +26110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26139,7 +26175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26189,7 +26225,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26259,7 +26295,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26329,7 +26365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26365,7 +26401,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26418,7 +26454,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26490,7 +26526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26569,7 +26605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26764,7 +26800,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -26801,7 +26837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -27487,7 +27523,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -27959,7 +27995,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28223,7 +28259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28263,38 +28299,1281 @@ Theory word_bitop loaded () : void +[(); ()] : void list + +() : void + +...() : void + +Theorem CONS_11 autoloading from theory `list` ... +CONS_11 = |- !h t h' t'. (CONS h t = CONS h' t') = (h = h') /\ (t = t') + +Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... +INV_SUC_EQ = |- !m n. (SUC m = SUC n) = (m = n) + +Definition LENGTH autoloading from theory `list` ... +LENGTH = |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) + +Definition MAP2 autoloading from theory `list` ... +MAP2 = +|- (!f. MAP2 f[][] = []) /\ + (!f h1 t1 h2 t2. + MAP2 f(CONS h1 t1)(CONS h2 t2) = CONS(f h1 h2)(MAP2 f t1 t2)) + +Definition SNOC autoloading from theory `list` ... +SNOC = +|- (!x. SNOC x[] = [x]) /\ + (!x x' l. SNOC x(CONS x' l) = CONS x'(SNOC x l)) + +MAP2_SNOC = +|- !f h1 h2 l1 l2. + (LENGTH l1 = LENGTH l2) ==> + (MAP2 f(SNOC h1 l1)(SNOC h2 l2) = SNOC(f h1 h2)(MAP2 f l1 l2)) + +Definition BUTLASTN autoloading from theory `list` ... +BUTLASTN = +|- (!l. BUTLASTN 0 l = l) /\ + (!n x l. BUTLASTN(SUC n)(SNOC x l) = BUTLASTN n l) + +BUTLASTN_MAP2 = +|- !l1 l2. + (LENGTH l1 = LENGTH l2) ==> + (!n. + n <= (LENGTH l1) ==> + (!f. + BUTLASTN n(MAP2 f l1 l2) = MAP2 f(BUTLASTN n l1)(BUTLASTN n l2))) + +Theorem SNOC_11 autoloading from theory `list` ... +SNOC_11 = |- !x l x' l'. (SNOC x l = SNOC x' l') = (x = x') /\ (l = l') + +Theorem LENGTH_LASTN autoloading from theory `list` ... +LENGTH_LASTN = |- !n l. n <= (LENGTH l) ==> (LENGTH(LASTN n l) = n) + +Definition LASTN autoloading from theory `list` ... +LASTN = +|- (!l. LASTN 0 l = []) /\ + (!n x l. LASTN(SUC n)(SNOC x l) = SNOC x(LASTN n l)) + +LASTN_MAP2 = +|- !l1 l2. + (LENGTH l1 = LENGTH l2) ==> + (!n. + n <= (LENGTH l1) ==> + (!f. LASTN n(MAP2 f l1 l2) = MAP2 f(LASTN n l1)(LASTN n l2))) + +Theorem word_Ax autoloading from theory `word_base` ... +word_Ax = |- !f. ?! fn. !l. fn(WORD l) = f l + +WNOT_DEF = |- !l. WNOT(WORD l) = WORD(MAP $~ l) + +Theorem LENGTH_BUTLASTN autoloading from theory `list` ... +LENGTH_BUTLASTN = +|- !n l. n <= (LENGTH l) ==> (LENGTH(BUTLASTN n l) = (LENGTH l) - n) + +Theorem LASTN_MAP autoloading from theory `list` ... +LASTN_MAP = +|- !n l. n <= (LENGTH l) ==> (!f. LASTN n(MAP f l) = MAP f(LASTN n l)) + +Theorem BUTLASTN_MAP autoloading from theory `list` ... +BUTLASTN_MAP = +|- !n l. + n <= (LENGTH l) ==> (!f. BUTLASTN n(MAP f l) = MAP f(BUTLASTN n l)) + +Theorem WORD_11 autoloading from theory `word_base` ... +WORD_11 = |- !l l'. (WORD l = WORD l') = (l = l') + +Theorem LENGTH_MAP autoloading from theory `list` ... +LENGTH_MAP = |- !l f. LENGTH(MAP f l) = LENGTH l + +Definition WSEG_DEF autoloading from theory `word_base` ... +WSEG_DEF = |- !m k l. WSEG m k(WORD l) = WORD(LASTN m(BUTLASTN k l)) + +Definition PWORDLEN_DEF autoloading from theory `word_base` ... +PWORDLEN_DEF = |- !n l. PWORDLEN n(WORD l) = (n = LENGTH l) + +BIT_WNOT_SYM_lemma = +|- !n. + !w :: PWORDLEN n. + PWORDLEN n(WNOT w) /\ + (!m k. (m + k) <= n ==> (WNOT(WSEG m k w) = WSEG m k(WNOT w))) + +Definition PBITOP_DEF autoloading from theory `word_bitop` ... +PBITOP_DEF = +|- !op. + PBITOP op = + (!n. + !w :: PWORDLEN n. + PWORDLEN n(op w) /\ + (!m k. (m + k) <= n ==> (op(WSEG m k w) = WSEG m k(op w)))) + +PBITOP_WNOT = |- PBITOP WNOT + +Definition MAP autoloading from theory `list` ... +MAP = +|- (!f. MAP f[] = []) /\ (!f h t. MAP f(CONS h t) = CONS(f h)(MAP f t)) + +WNOT_WNOT = |- !w. WNOT(WNOT w) = w + +Theorem MAP_APPEND autoloading from theory `list` ... +MAP_APPEND = +|- !f l1 l2. MAP f(APPEND l1 l2) = APPEND(MAP f l1)(MAP f l2) + +Definition WCAT_DEF autoloading from theory `word_base` ... +WCAT_DEF = |- !l1 l2. WCAT(WORD l1,WORD l2) = WORD(APPEND l1 l2) + +WCAT_WNOT = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. WCAT(WNOT w1,WNOT w2) = WNOT(WCAT(w1,w2)) + +Theorem LENGTH_MAP2 autoloading from theory `list` ... +LENGTH_MAP2 = +|- !l1 l2. + (LENGTH l1 = LENGTH l2) ==> + (!f. + (LENGTH(MAP2 f l1 l2) = LENGTH l1) /\ + (LENGTH(MAP2 f l1 l2) = LENGTH l2)) + +LENGTH_MAP22 = +|- !l1 l2 f. + (LENGTH l1 = LENGTH l2) ==> (LENGTH(MAP2 f l1 l2) = LENGTH l2) + +Theorem PBITBOP_EXISTS autoloading from theory `word_bitop` ... +PBITBOP_EXISTS = +|- !f. ?fn. !l1 l2. fn(WORD l1)(WORD l2) = WORD(MAP2 f l1 l2) + +WAND_DEF = |- !l1 l2. (WORD l1) WAND (WORD l2) = WORD(MAP2 $/\ l1 l2) + +PBITBOP_WAND_lemma = +|- !n. + !w1 w2 :: PWORDLEN n. + PWORDLEN n(w1 WAND w2) /\ + (!m k. + (m + k) <= n ==> + ((WSEG m k w1) WAND (WSEG m k w2) = WSEG m k(w1 WAND w2))) + +Definition PBITBOP_DEF autoloading from theory `word_bitop` ... +PBITBOP_DEF = +|- !op. + PBITBOP op = + (!n. + !w1 :: PWORDLEN n. + !w2 :: PWORDLEN n. + PWORDLEN n(op w1 w2) /\ + (!m k. + (m + k) <= n ==> + (op(WSEG m k w1)(WSEG m k w2) = WSEG m k(op w1 w2)))) + +PBITBOP_WAND = |- PBITBOP $WAND + +WOR_DEF = |- !l1 l2. (WORD l1) WOR (WORD l2) = WORD(MAP2 $\/ l1 l2) + +PBITBOP_WOR_lemma = +|- !n. + !w1 w2 :: PWORDLEN n. + PWORDLEN n(w1 WOR w2) /\ + (!m k. + (m + k) <= n ==> + ((WSEG m k w1) WOR (WSEG m k w2) = WSEG m k(w1 WOR w2))) + +PBITBOP_WOR = |- PBITBOP $WOR + +WXOR_DEF = +|- !l1 l2. (WORD l1) WXOR (WORD l2) = WORD(MAP2(\x y. ~(x = y))l1 l2) + +PBITBOP_WXOR_lemma = +|- !n. + !w1 w2 :: PWORDLEN n. + PWORDLEN n(w1 WXOR w2) /\ + (!m k. + (m + k) <= n ==> + ((WSEG m k w1) WXOR (WSEG m k w2) = WSEG m k(w1 WXOR w2))) + +PBITBOP_WXOR = |- PBITBOP $WXOR + +() : void + + +File mk_bword_bitop loaded +() : void + +#rm -f bword_num.th +echo 'set_flag(`abort_when_fail`,true);;'\ + 'loadt `mk_bword_num`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 9/2/25 +=============================================================================== + +#false : bool + + + +autoload_all = - : (string -> void) + +Loading library arith ... +Loading library reduce ... +Extending help search path. +Loading boolean conversions........ +Loading arithmetic conversions.................. +Loading general conversions, rule and tactic..... +Library reduce loaded. +.Updating help search path +....................................................................................................................................................................................................................................................................................... +Library arith loaded. +() : void + +Loading library res_quan ... +Updating search path +Theory res_quan loaded +...............................................................................Updating help search path +. +Library res_quan loaded. +() : void + +....() : void + + +File ver_202 loaded +() : void + +.........................................................() : void + +Theory word_bitop loaded +() : void + +() : void + +Theory word_num loaded +() : void + +[(); (); ()] : void list + +...() : void + +BV_DEF = |- !b. BV b = (b => SUC 0 | 0) + +Theorem word_Ax autoloading from theory `word_base` ... +word_Ax = |- !f. ?! fn. !l. fn(WORD l) = f l + +BNVAL_DEF = |- !l. BNVAL(WORD l) = LVAL BV 2 l + +BV_LESS_2 = |- !x. (BV x) < 2 + +Definition NVAL_DEF autoloading from theory `word_num` ... +NVAL_DEF = |- !f b l. NVAL f b(WORD l) = LVAL f b l + +BNVAL_NVAL = |- !w. BNVAL w = NVAL BV 2 w + +Theorem NVAL0 autoloading from theory `word_num` ... +NVAL0 = |- !f b. NVAL f b(WORD[]) = 0 + +BNVAL0 = |- BNVAL(WORD[]) = 0 + +Theorem SUC_LESS autoloading from theory `prim_rec` ... +SUC_LESS = |- !m n. (SUC m) < n ==> m < n + +Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... +INV_SUC_EQ = |- !m n. (SUC m = SUC n) = (m = n) + +Theorem NOT_SUC autoloading from theory `num` ... +NOT_SUC = |- !n. ~(SUC n = 0) + +Theorem ADD_EQ_0 autoloading from theory `arithmetic` ... +ADD_EQ_0 = |- !m n. (m + n = 0) = (m = 0) /\ (n = 0) + +Theorem LESS_NOT_EQ autoloading from theory `prim_rec` ... +LESS_NOT_EQ = |- !m n. m < n ==> ~(m = n) + +BNVAL_11_lem = |- !m n p. m < p /\ n < p ==> ~(p + m = n) + +Theorem EQ_MONO_ADD_EQ autoloading from theory `arithmetic` ... +EQ_MONO_ADD_EQ = |- !m n p. (m + p = n + p) = (m = n) + +Theorem CONS_11 autoloading from theory `list` ... +CONS_11 = |- !h t h' t'. (CONS h t = CONS h' t') = (h = h') /\ (t = t') + +Theorem LVAL autoloading from theory `word_num` ... +LVAL = +|- (!f b. LVAL f b[] = 0) /\ + (!l f b x. + LVAL f b(CONS x l) = ((f x) * (b EXP (LENGTH l))) + (LVAL f b l)) + +Theorem WORD_11 autoloading from theory `word_base` ... +WORD_11 = |- !l l'. (WORD l = WORD l') = (l = l') + +Definition WORDLEN_DEF autoloading from theory `word_base` ... +WORDLEN_DEF = |- !l. WORDLEN(WORD l) = LENGTH l + +Theorem LVAL_MAX autoloading from theory `word_num` ... +LVAL_MAX = +|- !l f b. (!x. (f x) < b) ==> (LVAL f b l) < (b EXP (LENGTH l)) + +BNVAL_11 = +|- !w1 w2. + (WORDLEN w1 = WORDLEN w2) ==> (BNVAL w1 = BNVAL w2) ==> (w1 = w2) + +BNVAL_ONTO = |- !w. ?n. BNVAL w = n + +BNVAL_MAX = |- !n. !w :: PWORDLEN n. (BNVAL w) < (2 EXP n) + +Theorem LVAL_SNOC autoloading from theory `word_num` ... +LVAL_SNOC = |- !l h f b. LVAL f b(SNOC h l) = ((LVAL f b l) * b) + (f h) + +Theorem SNOC_APPEND autoloading from theory `list` ... +SNOC_APPEND = |- !x l. SNOC x l = APPEND l[x] + +Definition WCAT_DEF autoloading from theory `word_base` ... +WCAT_DEF = |- !l1 l2. WCAT(WORD l1,WORD l2) = WORD(APPEND l1 l2) + +BNVAL_WCAT1 = +|- !n. + !w :: PWORDLEN n. + !x. BNVAL(WCAT(w,WORD[x])) = ((BNVAL w) * 2) + (BV x) + +Theorem NVAL_WCAT2 autoloading from theory `word_num` ... +NVAL_WCAT2 = +|- !n. + !w :: PWORDLEN n. + !f b x. + NVAL f b(WCAT(WORD[x],w)) = ((f x) * (b EXP n)) + (NVAL f b w) + +BNVAL_WCAT2 = +|- !n. + !w :: PWORDLEN n. + !x. BNVAL(WCAT(WORD[x],w)) = ((BV x) * (2 EXP n)) + (BNVAL w) + +Theorem NVAL_WCAT autoloading from theory `word_num` ... +NVAL_WCAT = +|- !n m. + !w1 :: PWORDLEN n. + !w2 :: PWORDLEN m. + !f b. + NVAL f b(WCAT(w1,w2)) = + ((NVAL f b w1) * (b EXP m)) + (NVAL f b w2) + +BNVAL_WCAT = +|- !n m. + !w1 :: PWORDLEN n. + !w2 :: PWORDLEN m. + BNVAL(WCAT(w1,w2)) = ((BNVAL w1) * (2 EXP m)) + (BNVAL w2) + +VB_DEF = |- !n. VB n = ~(n MOD 2 = 0) + +NBWORD_DEF = |- !n m. NBWORD n m = WORD(NLIST n VB 2 m) + +Definition NLIST_DEF autoloading from theory `word_num` ... +NLIST_DEF = +|- (!frep b m. NLIST 0 frep b m = []) /\ + (!n frep b m. + NLIST(SUC n)frep b m = SNOC(frep(m MOD b))(NLIST n frep b(m DIV b))) + +NBWORD0 = |- !m. NBWORD 0 m = WORD[] + +Theorem LENGTH_SNOC autoloading from theory `list` ... +LENGTH_SNOC = |- !x l. LENGTH(SNOC x l) = SUC(LENGTH l) + +Definition LENGTH autoloading from theory `list` ... +LENGTH = |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) + +NLIST_LENGTH = |- !n f b m. LENGTH(NLIST n f b m) = n + +WORDLEN_NBWORD = |- !n m. WORDLEN(NBWORD n m) = n + +Theorem PWORDLEN autoloading from theory `word_base` ... +PWORDLEN = |- !n w. PWORDLEN n w = (WORDLEN w = n) + +PWORDLEN_NBWORD = |- !n m. PWORDLEN n(NBWORD n m) + +Theorem WORD_SNOC_WCAT autoloading from theory `word_base` ... +WORD_SNOC_WCAT = |- !x l. WORD(SNOC x l) = WCAT(WORD l,WORD[x]) + +NBWORD_SUC = +|- !n m. NBWORD(SUC n)m = WCAT(NBWORD n(m DIV 2),WORD[VB(m MOD 2)]) + +Theorem SUC_ID autoloading from theory `prim_rec` ... +SUC_ID = |- !n. ~(SUC n = n) + +Theorem LESS_MOD autoloading from theory `arithmetic` ... +LESS_MOD = |- !n k. k < n ==> (k MOD n = k) + +VB_BV = |- !x. VB(BV x) = x + +Theorem ZERO_MOD autoloading from theory `arithmetic` ... +ZERO_MOD = |- !n. 0 < n ==> (0 MOD n = 0) + +Theorem ZERO_DIV autoloading from theory `arithmetic` ... +ZERO_DIV = |- !n. 0 < n ==> (0 DIV n = 0) + +BV_VB = |- !x. x < 2 ==> (BV(VB x) = x) + +Theorem MOD_EQ_0 autoloading from theory `arithmetic` ... +MOD_EQ_0 = |- !n. 0 < n ==> (!k. (k * n) MOD n = 0) + +Theorem MOD_MOD autoloading from theory `arithmetic` ... +MOD_MOD = |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) + +Theorem SNOC_11 autoloading from theory `list` ... +SNOC_11 = |- !x l x' l'. (SNOC x l = SNOC x' l') = (x = x') /\ (l = l') + +NBWORD_BNVAL = |- !n. !w :: PWORDLEN n. NBWORD n(BNVAL w) = w + +Theorem LESS_MULT_MONO autoloading from theory `arithmetic` ... +LESS_MULT_MONO = |- !m i n. ((SUC n) * m) < ((SUC n) * i) = m < i + +Theorem ZERO_LESS_EXP autoloading from theory `arithmetic` ... +ZERO_LESS_EXP = |- !m n. 0 < ((SUC n) EXP m) + +Definition EXP autoloading from theory `arithmetic` ... +EXP = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n)) + +Definition DIVISION autoloading from theory `arithmetic` ... +DIVISION = +|- !n. + 0 < n ==> (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n) + +BNVAL_NBWORD = |- !n m. m < (2 EXP n) ==> (BNVAL(NBWORD n m) = m) + +ZERO_WORD_VAL = +|- !n. !w :: PWORDLEN n. (w = NBWORD n 0) = (BNVAL w = 0) + +Theorem WCAT_ASSOC autoloading from theory `word_base` ... +WCAT_ASSOC = |- !w1 w2 w3. WCAT(w1,WCAT(w2,w3)) = WCAT(WCAT(w1,w2),w3) + +Theorem ADD_SUC autoloading from theory `arithmetic` ... +ADD_SUC = |- !m n. SUC(m + n) = m + (SUC n) + +Theorem WCAT0 autoloading from theory `word_base` ... +WCAT0 = |- !w. (WCAT(WORD[],w) = w) /\ (WCAT(w,WORD[]) = w) + +WCAT_NBWORD_0 = +|- !n1 n2. WCAT(NBWORD n1 0,NBWORD n2 0) = NBWORD(n1 + n2)0 + +WSPLIT_NBWORD_0 = +|- !m n. m <= n ==> (WSPLIT m(NBWORD n 0) = NBWORD(n - m)0,NBWORD m 0) + +Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... +LESS_EQ_REFL = |- !m. m <= m + +Theorem WSEG_PWORDLEN autoloading from theory `word_base` ... +WSEG_PWORDLEN = +|- !n. !w :: PWORDLEN n. !m k. (m + k) <= n ==> PWORDLEN m(WSEG m k w) + +Theorem WCAT_11 autoloading from theory `word_base` ... +WCAT_11 = +|- !m n. + !wm1 wm2 :: PWORDLEN m. + !wn1 wn2 :: PWORDLEN n. + (WCAT(wm1,wn1) = WCAT(wm2,wn2)) = (wm1 = wm2) /\ (wn1 = wn2) + +Theorem WSPLIT_WSEG autoloading from theory `word_base` ... +WSPLIT_WSEG = +|- !n. + !w :: PWORDLEN n. + !k. k <= n ==> (WSPLIT k w = WSEG(n - k)k w,WSEG k 0 w) + +EQ_NBWORD0_SPLIT = +|- !n. + !w :: PWORDLEN n. + !m. + m <= n ==> + ((w = NBWORD n 0) = + (WSEG(n - m)m w = NBWORD(n - m)0) /\ (WSEG m 0 w = NBWORD m 0)) + +Theorem MULT_0 autoloading from theory `arithmetic` ... +MULT_0 = |- !m. m * 0 = 0 + +LESS2_DIV2 = |- !r y. 0 < y /\ r < (2 * y) ==> (r DIV 2) < y + +less2 = |- 0 < 2 + +MOD_DIV_lemma = +|- !x y. 0 < y ==> ((x MOD (2 * y)) DIV 2 = (x DIV 2) MOD y) + +Definition PWORDLEN_DEF autoloading from theory `word_base` ... +PWORDLEN_DEF = |- !n l. PWORDLEN n(WORD l) = (n = LENGTH l) + +NBWORD_MOD = |- !n m. NBWORD n(m MOD (2 EXP n)) = NBWORD n m + +Theorem WSEG_WORD_LENGTH autoloading from theory `word_base` ... +WSEG_WORD_LENGTH = |- !n. !w :: PWORDLEN n. WSEG n 0 w = w + +Theorem SUC_SUB1 autoloading from theory `arithmetic` ... +SUC_SUB1 = |- !m. (SUC m) - 1 = m + +Theorem ZERO_LESS_EQ autoloading from theory `arithmetic` ... +ZERO_LESS_EQ = |- !n. 0 <= n + +Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... +LESS_EQ_SUC_REFL = |- !m. m <= (SUC m) + +Theorem PWORDLEN1 autoloading from theory `word_base` ... +PWORDLEN1 = |- !x. PWORDLEN 1(WORD[x]) + +Theorem WSEG_WCAT_WSEG autoloading from theory `word_base` ... +WSEG_WCAT_WSEG = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. + !m k. + (m + k) <= (n1 + n2) /\ k < n2 /\ n2 <= (m + k) ==> + (WSEG m k(WCAT(w1,w2)) = + WCAT(WSEG((m + k) - n2)0 w1,WSEG(n2 - k)k w2)) + +Theorem WSEG0 autoloading from theory `word_base` ... +WSEG0 = |- !k w. WSEG 0 k w = WORD[] + +WSEG_NBWORD_SUC = |- !n m. WSEG n 0(NBWORD(SUC n)m) = NBWORD n m + +Theorem NVAL_MAX autoloading from theory `word_num` ... +NVAL_MAX = +|- !f b. + (!x. (f x) < b) ==> (!n. !w :: PWORDLEN n. (NVAL f b w) < (b EXP n)) + +Theorem WORDLEN_SUC_WCAT_BIT_WSEG autoloading from theory `word_base` ... +WORDLEN_SUC_WCAT_BIT_WSEG = +|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WORD[BIT n w],WSEG n 0 w) + +NBWORD_SUC_WSEG = +|- !n. !w :: PWORDLEN(SUC n). NBWORD n(BNVAL w) = WSEG n 0 w + +Theorem TIMES2 autoloading from theory `arithmetic` ... +TIMES2 = |- !n. 2 * n = n + n + +Definition SHL_DEF autoloading from theory `word_bitop` ... +SHL_DEF = +|- !f w b. + SHL f w b = + BIT(PRE(WORDLEN w))w, + WCAT(WSEG(PRE(WORDLEN w))0 w,(f => WSEG 1 0 w | WORD[b])) + +DOUBLE_EQ_SHL = +|- !n. + 0 < n ==> + (!w :: PWORDLEN n. + !b. NBWORD n((BNVAL w) + ((BNVAL w) + (BV b))) = SND(SHL F w b)) + +Theorem LESS_ADD_SUC autoloading from theory `arithmetic` ... +LESS_ADD_SUC = |- !m n. m < (m + (SUC n)) + +Theorem BIT_WCAT_FST autoloading from theory `word_base` ... +BIT_WCAT_FST = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. + !k. + n2 <= k /\ k < (n1 + n2) ==> (BIT k(WCAT(w1,w2)) = BIT(k - n2)w1) + +Definition SNOC autoloading from theory `list` ... +SNOC = +|- (!x. SNOC x[] = [x]) /\ + (!x x' l. SNOC x(CONS x' l) = CONS x'(SNOC x l)) + +Theorem BIT0 autoloading from theory `word_base` ... +BIT0 = |- !b. BIT 0(WORD[b]) = b + +MSB_NBWORD = +|- !n m. BIT n(NBWORD(SUC n)m) = VB((m DIV (2 EXP n)) MOD 2) + +ZERO_LESS_TWO_EXP = |- !m. 0 < (2 EXP m) + +NBWORD_SPLIT = +|- !n1 n2 m. + NBWORD(n1 + n2)m = WCAT(NBWORD n1(m DIV (2 EXP n2)),NBWORD n2 m) + +Theorem WSEG_WCAT2 autoloading from theory `word_base` ... +WSEG_WCAT2 = +|- !n1 n2. + !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n2 0(WCAT(w1,w2)) = w2 + +Theorem SUB_EQUAL_0 autoloading from theory `arithmetic` ... +SUB_EQUAL_0 = |- !c. c - c = 0 + +Theorem WSEG_WCAT_WSEG1 autoloading from theory `word_base` ... +WSEG_WCAT_WSEG1 = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. + !m k. + m <= n1 /\ n2 <= k ==> (WSEG m k(WCAT(w1,w2)) = WSEG m(k - n2)w1) + +WSEG_NBWORD = +|- !m k n. + (m + k) <= n ==> + (!l. WSEG m k(NBWORD n l) = NBWORD m(l DIV (2 EXP k))) + +NBWORD_SUC_FST = +|- !n m. + NBWORD(SUC n)m = WCAT(WORD[VB((m DIV (2 EXP n)) MOD 2)],NBWORD n m) + +Theorem BIT_WSEG autoloading from theory `word_base` ... +BIT_WSEG = +|- !n. + !w :: PWORDLEN n. + !m k j. + (m + k) <= n ==> j < m ==> (BIT j(WSEG m k w) = BIT(j + k)w) + +BIT_NBWORD0 = |- !k n. k < n ==> (BIT k(NBWORD n 0) = F) + +add_lem = +|- !m1 m2 n1 n2 p. + ((m1 * p) + n1) + ((m2 * p) + n2) = + ((m1 * p) + (m2 * p)) + (n1 + n2) + +ADD_BNVAL_LEFT = +|- !n. + !w1 w2 :: PWORDLEN(SUC n). + (BNVAL w1) + (BNVAL w2) = + (((BV(BIT n w1)) + (BV(BIT n w2))) * (2 EXP n)) + + ((BNVAL(WSEG n 0 w1)) + (BNVAL(WSEG n 0 w2))) + +Theorem WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT autoloading from theory `word_base` ... +WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT = +|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WSEG n 1 w,WORD[BIT 0 w]) + +ADD_BNVAL_RIGHT = +|- !n. + !w1 w2 :: PWORDLEN(SUC n). + (BNVAL w1) + (BNVAL w2) = + (((BNVAL(WSEG n 1 w1)) + (BNVAL(WSEG n 1 w2))) * 2) + + ((BV(BIT 0 w1)) + (BV(BIT 0 w2))) + +Theorem WCAT_WSEG_WSEG autoloading from theory `word_base` ... +WCAT_WSEG_WSEG = +|- !n. + !w :: PWORDLEN n. + !m1 m2 k. + (m1 + (m2 + k)) <= n ==> + (WCAT(WSEG m2(m1 + k)w,WSEG m1 k w) = WSEG(m1 + m2)k w) + +ADD_BNVAL_SPLIT = +|- !n1 n2. + !w1 w2 :: PWORDLEN(n1 + n2). + (BNVAL w1) + (BNVAL w2) = + (((BNVAL(WSEG n1 n2 w1)) + (BNVAL(WSEG n1 n2 w2))) * (2 EXP n2)) + + ((BNVAL(WSEG n2 0 w1)) + (BNVAL(WSEG n2 0 w2))) + +() : void + + +File mk_bword_num loaded +() : void + +#rm -f bword_arith.th +echo 'set_flag(`abort_when_fail`,true);;'\ + 'loadt `mk_bword_arith`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 9/2/25 +=============================================================================== + +#false : bool + + + +autoload_all = - : (string -> void) + +Loading library arith ... +Loading library reduce ... +Extending help search path. +Loading boolean conversions........ +Loading arithmetic conversions.................. +Loading general conversions, rule and tactic..... +Library reduce loaded. +.Updating help search path +....................................................................................................................................................................................................................................................................................... +Library arith loaded. +() : void + +Loading library res_quan ... +Updating search path +Theory res_quan loaded +...............................................................................Updating help search path +. +Library res_quan loaded. +() : void + +....() : void + + +File ver_202 loaded +() : void + +.........................................................() : void + +Theory bword_num loaded +() : void + +[(); (); ()] : void list + +() : void + +MULT_LEFT_1 = |- !m. 1 * m = m + +ADD_DIV_SUC_DIV = |- !n. 0 < n ==> (!r. (n + r) DIV n = SUC(r DIV n)) + +Theorem LESS_EQ autoloading from theory `arithmetic` ... +LESS_EQ = |- !m n. m < n = (SUC m) <= n + +Theorem ZERO_LESS_EQ autoloading from theory `arithmetic` ... +ZERO_LESS_EQ = |- !n. 0 <= n + +LESS_IMP_LESS_EQ_PRE = |- !m n. 0 < n ==> (m < n = m <= (PRE n)) + +LESS_MONO_DIV = +|- !n. 0 < n ==> (!p q. p < q ==> (p DIV n) <= (q DIV n)) + +Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... +LESS_EQ_REFL = |- !m. m <= m + +Definition LESS_OR_EQ autoloading from theory `arithmetic` ... +LESS_OR_EQ = |- !m n. m <= n = m < n \/ (m = n) + +LESS_EQ_MONO_DIV = +|- !n. 0 < n ==> (!p q. p <= q ==> (p DIV n) <= (q DIV n)) + +Theorem PRE_SUC_EQ autoloading from theory `arithmetic` ... +PRE_SUC_EQ = |- !m n. 0 < n ==> ((m = PRE n) = (SUC m = n)) + +SUC_PRE = |- !n. 0 < n ==> (SUC(PRE n) = n) + +Theorem TIMES2 autoloading from theory `arithmetic` ... +TIMES2 = |- !n. 2 * n = n + n + +Definition EXP autoloading from theory `arithmetic` ... +EXP = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n)) + +ONE_LESS_TWO_EXP_SUC = |- !n. 1 < (2 EXP (SUC n)) + +ADD_MONO_EQ = |- !m n p. (p + m = p + n) = (m = n) + +ACARRY_DEF = +|- (!w1 w2 cin. ACARRY 0 w1 w2 cin = cin) /\ + (!n w1 w2 cin. + ACARRY(SUC n)w1 w2 cin = + VB + (((BV(BIT n w1)) + ((BV(BIT n w2)) + (BV(ACARRY n w1 w2 cin)))) DIV + 2)) + +ICARRY_DEF = +|- (!w1 w2 cin. ICARRY 0 w1 w2 cin = cin) /\ + (!n w1 w2 cin. + ICARRY(SUC n)w1 w2 cin = + BIT n w1 /\ BIT n w2 \/ + (BIT n w1 \/ BIT n w2) /\ ICARRY n w1 w2 cin) + +Theorem ZERO_MOD autoloading from theory `arithmetic` ... +ZERO_MOD = |- !n. 0 < n ==> (0 MOD n = 0) + +Theorem ZERO_DIV autoloading from theory `arithmetic` ... +ZERO_DIV = |- !n. 0 < n ==> (0 DIV n = 0) + +div_mod_lemmas = +[|- !x. (SUC(SUC x)) DIV 2 = SUC(x DIV 2); + |- (SUC 0) DIV 2 = 0; + |- 0 DIV 2 = 0; + |- (SUC 0) MOD 2 = SUC 0; + |- 0 MOD 2 = 0] +: thm list + +Theorem SUC_NOT autoloading from theory `arithmetic` ... +SUC_NOT = |- !n. ~(0 = SUC n) + +Theorem NOT_SUC autoloading from theory `num` ... +NOT_SUC = |- !n. ~(SUC n = 0) + +Definition VB_DEF autoloading from theory `bword_num` ... +VB_DEF = |- !n. VB n = ~(n MOD 2 = 0) + +Definition BV_DEF autoloading from theory `bword_num` ... +BV_DEF = |- !b. BV b = (b => SUC 0 | 0) + +Theorem LESS_IMP_LESS_OR_EQ autoloading from theory `arithmetic` ... +LESS_IMP_LESS_OR_EQ = |- !m n. m < n ==> m <= n + +ACARRY_EQ_ICARRY = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin k. k <= n ==> (ACARRY k w1 w2 cin = ICARRY k w1 w2 cin) + +Less2 = |- 0 < 2 + +Less2_SUC0 = |- (SUC 0) < 2 + +Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... +LESS_EQ_SUC_REFL = |- !m. m <= (SUC m) + +BV_LESS_EQ_1 = |- !x. (BV x) <= 1 + +Theorem LESS_EQ_LESS_EQ_MONO autoloading from theory `arithmetic` ... +LESS_EQ_LESS_EQ_MONO = +|- !m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q) + +ADD_BV_LESS_EQ_2 = |- !x1 x2. ((BV x1) + (BV x2)) <= 2 + +LESS_EQ1_LESS2 = |- n < 2 = n <= 1 + +Theorem BNVAL_MAX autoloading from theory `bword_num` ... +BNVAL_MAX = |- !n. !w :: PWORDLEN n. (BNVAL w) < (2 EXP n) + +Theorem ZERO_LESS_EXP autoloading from theory `arithmetic` ... +ZERO_LESS_EXP = |- !m n. 0 < ((SUC n) EXP m) + +Theorem PRE_SUB1 autoloading from theory `arithmetic` ... +PRE_SUB1 = |- !m. PRE m = m - 1 + +BNVAL_LESS_EQ = |- !n. !w :: PWORDLEN n. (BNVAL w) <= ((2 EXP n) - 1) + +Theorem LESS_MONO_MULT autoloading from theory `arithmetic` ... +LESS_MONO_MULT = |- !m n p. m <= n ==> (m * p) <= (n * p) + +Theorem LEFT_SUB_DISTRIB autoloading from theory `arithmetic` ... +LEFT_SUB_DISTRIB = |- !m n p. p * (m - n) = (p * m) - (p * n) + +ADD_BNVAL_LESS_EQ = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin. + ((BNVAL w1) + ((BNVAL w2) + (BV cin))) <= ((2 EXP (SUC n)) - 1) -Error: UNDEFINED-FUNCTION :NAME NIL -Fast links are on: do (si::use-fast-links nil) for debugging -Signalled by FUN%2506%11. -UNDEFINED-FUNCTION :NAME NIL - -Broken at FUN%2506%11. Type :H for Help. - 1 Return to top level. ->> -Error: UNBOUND-VARIABLE :NAME QUIT -Fast links are on: do (si::use-fast-links nil) for debugging -Signalled by FUN%2506%11. - -UNBOUND-VARIABLE :NAME QUIT - -Broken at FUN%2506%11. - 1 (abort) Return to debug level 1. - 2 Return to top level. ->>> -NIL ->>> -Error: ERROR "Caught fatal error [memory may be damaged]" -Fast links are on: do (si::use-fast-links nil) for debugging -Signalled by FUN%2506%11. - -ERROR "Caught fatal error [memory may be damaged]" - -Broken at FUN%2506%11. - 1 (abort) Return to debug level 2. - 2 Return to debug level 1. - 3 Return to top level. ->>>>make[4]: *** [Makefile:87: bword_bitop.th] Error 255 +ZERO_LESS_TWO_EXP = |- !m. 0 < (2 EXP m) + +EXP_SUB1_LESS = |- ((2 EXP n) - 1) < (2 EXP n) + +ADD_BNVAL_LESS_EQ1 = +|- !n cin. + !w1 w2 :: PWORDLEN n. + (((BNVAL w1) + ((BNVAL w2) + (BV cin))) DIV (2 EXP n)) <= (SUC 0) + +ADD_BV_BNVAL_DIV_LESS_EQ1 = +|- !n x1 x2 cin. + !w1 w2 :: PWORDLEN n. + ((((BV x1) + (BV x2)) + + (((BNVAL w1) + ((BNVAL w2) + (BV cin))) DIV (2 EXP n))) DIV + 2) <= + 1 + +Theorem SUC_LESS autoloading from theory `prim_rec` ... +SUC_LESS = |- !m n. (SUC m) < n ==> m < n + +ADD_BV_BNVAL_LESS_EQ = +|- !n x1 x2 cin. + !w1 w2 :: PWORDLEN n. + (((BV x1) + (BV x2)) + ((BNVAL w1) + ((BNVAL w2) + (BV cin)))) <= + (SUC(2 EXP (SUC n))) + +ADD_BV_BNVAL_LESS_EQ1 = +|- !n x1 x2 cin. + !w1 w2 :: PWORDLEN n. + ((((BV x1) + (BV x2)) + ((BNVAL w1) + ((BNVAL w2) + (BV cin)))) DIV + (2 EXP (n + 1))) <= + 1 + +Theorem WSEG_PWORDLEN autoloading from theory `word_base` ... +WSEG_PWORDLEN = +|- !n. !w :: PWORDLEN n. !m k. (m + k) <= n ==> PWORDLEN m(WSEG m k w) + +seg_pw = +|- !w. PWORDLEN n w ==> (SUC k) <= n ==> PWORDLEN(SUC k)(WSEG(SUC k)0 w) + +Theorem BIT_WSEG autoloading from theory `word_base` ... +BIT_WSEG = +|- !n. + !w :: PWORDLEN n. + !m k j. + (m + k) <= n ==> j < m ==> (BIT j(WSEG m k w) = BIT(j + k)w) + +bit_thm = +|- !w. + PWORDLEN n w ==> (SUC k) <= n ==> (BIT k(WSEG(SUC k)0 w) = BIT k w) + +Theorem WSEG_WSEG autoloading from theory `word_base` ... +WSEG_WSEG = +|- !n. + !w :: PWORDLEN n. + !m1 k1 m2 k2. + (m1 + k1) <= n /\ (m2 + k2) <= m1 ==> + (WSEG m2 k2(WSEG m1 k1 w) = WSEG m2(k1 + k2)w) + +seg_thm = +|- !w. + PWORDLEN n w ==> + (SUC k) <= n ==> + (WSEG k 0(WSEG(SUC k)0 w) = WSEG k 0 w) + +seg_pw_thm' = |- !w. PWORDLEN n w ==> k <= n ==> PWORDLEN k(WSEG k 0 w) + +spec_thm = - : (thm -> thm list) + +Theorem ADD_BNVAL_LEFT autoloading from theory `bword_num` ... +ADD_BNVAL_LEFT = +|- !n. + !w1 w2 :: PWORDLEN(SUC n). + (BNVAL w1) + (BNVAL w2) = + (((BV(BIT n w1)) + (BV(BIT n w2))) * (2 EXP n)) + + ((BNVAL(WSEG n 0 w1)) + (BNVAL(WSEG n 0 w2))) + +add_left = +... |- (BNVAL(WSEG(SUC k)0 w1)) + (BNVAL(WSEG(SUC k)0 w2)) = + (((BV(BIT k w1)) + (BV(BIT k w2))) * (2 EXP k)) + + ((BNVAL(WSEG k 0 w1)) + (BNVAL(WSEG k 0 w2))) + +less1_lem = +... |- ((((BV(BIT k w1)) + (BV(BIT k w2))) + + (((BNVAL(WSEG k 0 w1)) + ((BNVAL(WSEG k 0 w2)) + (BV cin))) DIV + (2 EXP k))) DIV + 2) <= + 1 + +Theorem BV_VB autoloading from theory `bword_num` ... +BV_VB = |- !x. x < 2 ==> (BV(VB x) = x) + +Theorem BNVAL0 autoloading from theory `bword_num` ... +BNVAL0 = |- BNVAL(WORD[]) = 0 + +Theorem WSEG0 autoloading from theory `word_base` ... +WSEG0 = |- !k w. WSEG 0 k w = WORD[] + +ACARRY_EQ_ADD_DIV = +|- !n. + !w1 w2 :: PWORDLEN n. + !k. + k < n ==> + (BV(ACARRY k w1 w2 cin) = + ((BNVAL(WSEG k 0 w1)) + ((BNVAL(WSEG k 0 w2)) + (BV cin))) DIV + (2 EXP k)) + +Theorem NBWORD_MOD autoloading from theory `bword_num` ... +NBWORD_MOD = |- !n m. NBWORD n(m MOD (2 EXP n)) = NBWORD n m + +Theorem LESS_ADD_NONZERO autoloading from theory `arithmetic` ... +LESS_ADD_NONZERO = |- !m n. ~(n = 0) ==> m < (m + n) + +Theorem NBWORD_SPLIT autoloading from theory `bword_num` ... +NBWORD_SPLIT = +|- !n1 n2 m. + NBWORD(n1 + n2)m = WCAT(NBWORD n1(m DIV (2 EXP n2)),NBWORD n2 m) + +Theorem WSEG_WORD_LENGTH autoloading from theory `word_base` ... +WSEG_WORD_LENGTH = |- !n. !w :: PWORDLEN n. WSEG n 0 w = w + +Theorem WCAT0 autoloading from theory `word_base` ... +WCAT0 = |- !w. (WCAT(WORD[],w) = w) /\ (WCAT(w,WORD[]) = w) + +Theorem NBWORD0 autoloading from theory `bword_num` ... +NBWORD0 = |- !m. NBWORD 0 m = WORD[] + +Theorem PWORDLEN_NBWORD autoloading from theory `bword_num` ... +PWORDLEN_NBWORD = |- !n m. PWORDLEN n(NBWORD n m) + +Theorem WCAT_11 autoloading from theory `word_base` ... +WCAT_11 = +|- !m n. + !wm1 wm2 :: PWORDLEN m. + !wn1 wn2 :: PWORDLEN n. + (WCAT(wm1,wn1) = WCAT(wm2,wn2)) = (wm1 = wm2) /\ (wn1 = wn2) + +Theorem ADD_BNVAL_SPLIT autoloading from theory `bword_num` ... +ADD_BNVAL_SPLIT = +|- !n1 n2. + !w1 w2 :: PWORDLEN(n1 + n2). + (BNVAL w1) + (BNVAL w2) = + (((BNVAL(WSEG n1 n2 w1)) + (BNVAL(WSEG n1 n2 w2))) * (2 EXP n2)) + + ((BNVAL(WSEG n2 0 w1)) + (BNVAL(WSEG n2 0 w2))) + +ADD_WORD_SPLIT = +|- !n1 n2. + !w1 w2 :: PWORDLEN(n1 + n2). + !cin. + NBWORD(n1 + n2)((BNVAL w1) + ((BNVAL w2) + (BV cin))) = + WCAT + (NBWORD + n1 + ((BNVAL(WSEG n1 n2 w1)) + + ((BNVAL(WSEG n1 n2 w2)) + (BV(ACARRY n2 w1 w2 cin)))), + NBWORD + n2 + ((BNVAL(WSEG n2 0 w1)) + ((BNVAL(WSEG n2 0 w2)) + (BV cin)))) + +Theorem WSEG_WCAT2 autoloading from theory `word_base` ... +WSEG_WCAT2 = +|- !n1 n2. + !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n2 0(WCAT(w1,w2)) = w2 + +Theorem WSEG_WCAT_WSEG1 autoloading from theory `word_base` ... +WSEG_WCAT_WSEG1 = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. + !m k. + m <= n1 /\ n2 <= k ==> (WSEG m k(WCAT(w1,w2)) = WSEG m(k - n2)w1) + +Theorem SUB_EQUAL_0 autoloading from theory `arithmetic` ... +SUB_EQUAL_0 = |- !c. c - c = 0 + +WSEG_NBWORD_ADD = +|- !n. + !w1 w2 :: PWORDLEN n. + !m k cin. + (m + k) <= n ==> + (WSEG m k(NBWORD n((BNVAL w1) + ((BNVAL w2) + (BV cin)))) = + NBWORD + m + ((BNVAL(WSEG m k w1)) + + ((BNVAL(WSEG m k w2)) + (BV(ACARRY k w1 w2 cin))))) + +ADD_NBWORD_EQ0_SPLIT = +|- !n1 n2. + !w1 w2 :: PWORDLEN(n1 + n2). + !cin. + (NBWORD(n1 + n2)((BNVAL w1) + ((BNVAL w2) + (BV cin))) = + NBWORD(n1 + n2)0) = + (NBWORD + n1 + ((BNVAL(WSEG n1 n2 w1)) + + ((BNVAL(WSEG n1 n2 w2)) + (BV(ACARRY n2 w1 w2 cin)))) = + NBWORD n1 0) /\ + (NBWORD + n2 + ((BNVAL(WSEG n2 0 w1)) + ((BNVAL(WSEG n2 0 w2)) + (BV cin))) = + NBWORD n2 0) + +Theorem MOD_MOD autoloading from theory `arithmetic` ... +MOD_MOD = |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) + +VB_MOD_2 = |- !n. VB(n MOD 2) = VB n + +Theorem NBWORD_SUC_FST autoloading from theory `bword_num` ... +NBWORD_SUC_FST = +|- !n m. + NBWORD(SUC n)m = WCAT(WORD[VB((m DIV (2 EXP n)) MOD 2)],NBWORD n m) + +Theorem VB_BV autoloading from theory `bword_num` ... +VB_BV = |- !x. VB(BV x) = x + +Theorem BV_LESS_2 autoloading from theory `bword_num` ... +BV_LESS_2 = |- !x. (BV x) < 2 + +Theorem LESS_MOD autoloading from theory `arithmetic` ... +LESS_MOD = |- !n k. k < n ==> (k MOD n = k) + +Theorem NVAL0 autoloading from theory `word_num` ... +NVAL0 = |- !f b. NVAL f b(WORD[]) = 0 + +Theorem NBWORD_SUC autoloading from theory `bword_num` ... +NBWORD_SUC = +|- !n m. NBWORD(SUC n)m = WCAT(NBWORD n(m DIV 2),WORD[VB(m MOD 2)]) + +Theorem BNVAL_NVAL autoloading from theory `bword_num` ... +BNVAL_NVAL = |- !w. BNVAL w = NVAL BV 2 w + +Theorem PWORDLEN0 autoloading from theory `word_base` ... +PWORDLEN0 = |- !w. PWORDLEN 0 w ==> (w = WORD[]) + +Theorem BIT_WCAT_FST autoloading from theory `word_base` ... +BIT_WCAT_FST = +|- !n1 n2. + !w1 :: PWORDLEN n1. + !w2 :: PWORDLEN n2. + !k. + n2 <= k /\ k < (n1 + n2) ==> (BIT k(WCAT(w1,w2)) = BIT(k - n2)w1) + +Theorem BIT0 autoloading from theory `word_base` ... +BIT0 = |- !b. BIT 0(WORD[b]) = b + +Theorem LESS_ADD_SUC autoloading from theory `arithmetic` ... +LESS_ADD_SUC = |- !m n. m < (m + (SUC n)) + +Theorem PWORDLEN1 autoloading from theory `word_base` ... +PWORDLEN1 = |- !x. PWORDLEN 1(WORD[x]) + +ACARRY_MSB = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin. + ACARRY n w1 w2 cin = + BIT n(NBWORD(SUC n)((BNVAL w1) + ((BNVAL w2) + (BV cin)))) + +Theorem LESS_SUC autoloading from theory `prim_rec` ... +LESS_SUC = |- !m n. m < n ==> m < (SUC n) + +ACARRY_WSEG = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin k m. + k < m /\ m <= n ==> + (ACARRY k(WSEG m 0 w1)(WSEG m 0 w2)cin = ACARRY k w1 w2 cin) + +ICARRY_WSEG = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin k m. + k < m /\ m <= n ==> + (ICARRY k(WSEG m 0 w1)(WSEG m 0 w2)cin = ICARRY k w1 w2 cin) + +ACARRY_ACARRY_WSEG = +|- !n. + !w1 w2 :: PWORDLEN n. + !cin m k1 k2. + k1 < m /\ k2 < n /\ (m + k2) <= n ==> + (ACARRY k1(WSEG m k2 w1)(WSEG m k2 w2)(ACARRY k2 w1 w2 cin) = + ACARRY(k1 + k2)w1 w2 cin) + +() : void + + +File mk_bword_arith loaded +() : void + +#rm -f word.th +echo 'set_flag(`abort_when_fail`,true);;'\ + 'loadt `mk_word`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 9/2/25 +=============================================================================== + +#false : bool + + + +autoload_all = - : (string -> void) + +Loading library arith ... +Loading library reduce ... +Extending help search path. +Loading boolean conversions........ +Loading arithmetic conversions.................. +Loading general conversions, rule and tactic..... +Library reduce loaded. +.Updating help search path +....................................................................................................................................................................................................................................................................................... +Library arith loaded. +() : void + +Loading library res_quan ... +Updating search path +Theory res_quan loaded +...............................................................................Updating help search path +. +Library res_quan loaded. +() : void + +....() : void + + +File ver_202 loaded +() : void + +() : void + +Theory bword_bitop loaded +Theory bword_num loaded +Theory bword_arith loaded +[(); (); ()] : void list + +() : void + + +File mk_word loaded +() : void + +#echo 'set_flag(`abort_when_fail`,true);;'\ + 'load_library`res_quan`;;'\ + 'load_theory `word`;;'\ + 'compilet `word_convs`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 9/2/25 +=============================================================================== + +#false : bool + +Loading library res_quan ... +Updating search path +Theory res_quan loaded +...............................................................................Updating help search path +. +Library res_quan loaded. +() : void + +#Theory word loaded +() : void + + +word_CASES_TAC = - : (term -> tactic) + +word_INDUCT_TAC = - : tactic + +RESQ_WORDLEN_TAC = - : tactic + +BIT_CONV = - : conv + +WSEG_CONV = - : conv + + +LESS_CONV = - : conv + +LESS_EQ_CONV = - : conv + +word_inst_thm = - : ((term # term) -> thm -> thm) + +WNOT_PWORDLEN = |- !n. !w :: PWORDLEN n. PWORDLEN n(WNOT w) + +WAND_PWORDLEN = |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WAND w2) +WOR_PWORDLEN = |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WOR w2) +WXOR_PWORDLEN = |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WXOR w2) + +pwordlen_bitop_funs = +[(`WNOT`, |- !n. !w :: PWORDLEN n. PWORDLEN n(WNOT w)); + (`WAND`, |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WAND w2)); + (`WOR`, |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WOR w2)); + (`WXOR`, |- !n. !w1 w2 :: PWORDLEN n. PWORDLEN n(w1 WXOR w2))] +: (string # thm) list + +pwordlen_funs = +[(`WORD`, -); + (`WSEG`, -); + (`WNOT`, -); + (`WAND`, -); + (`WOR`, -); + (`WXOR`, -); + (`WCAT`, -)] +: (string # (term list -> term -> term list -> thm)) list + +check = - : (string -> term -> term) + +pick_fn = - : (string -> (string # *) list -> term -> *) + +PWORDLEN_CONV = - : (term list -> conv) + +PWORDLEN_bitop_CONV = - : conv + +WSEG_WSEG_CONV = - : (term -> conv) + +((-), (-), -) : ((term list -> conv) # conv # (term -> conv)) + + +PWORDLEN_CONV = - : (term list -> conv) +PWORDLEN_bitop_CONV = - : conv +WSEG_WSEG_CONV = - : (term -> conv) + +PWORDLEN_TAC = - : (term list -> tactic) + +Calling Lisp compiler + +File word_convs compiled +() : void + +#===> library word rebuilt make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof' echo 'set_flag(`abort_when_fail`,true);;'\ @@ -28303,7 +29582,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28502,7 +29781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28534,7 +29813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28668,7 +29947,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -28971,7 +30250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29003,7 +30282,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29042,7 +30321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29074,7 +30353,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29235,7 +30514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29368,7 +30647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29557,7 +30836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29617,7 +30896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29742,7 +31021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29853,7 +31132,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29878,7 +31157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -29906,7 +31185,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -30019,7 +31298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -30522,7 +31801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -30770,7 +32049,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -30996,7 +32275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -31038,7 +32317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -31070,7 +32349,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -31293,7 +32572,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -31686,7 +32965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -31799,7 +33078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32302,7 +33581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32550,7 +33829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32776,7 +34055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32811,7 +34090,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32850,7 +34129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32887,7 +34166,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -32908,7 +34187,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33005,7 +34284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33027,7 +34306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33523,7 +34802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33546,7 +34825,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33624,7 +34903,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33683,7 +34962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33727,7 +35006,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33745,7 +35024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33772,7 +35051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33816,7 +35095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33929,7 +35208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -33976,7 +35255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34015,7 +35294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34089,7 +35368,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34178,7 +35457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34249,7 +35528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34319,7 +35598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34368,7 +35647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34409,7 +35688,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34450,7 +35729,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34474,7 +35753,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34575,7 +35854,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34596,7 +35875,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -34621,7 +35900,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35247,7 +36526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35324,7 +36603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35351,7 +36630,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35468,7 +36747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35563,7 +36842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35649,7 +36928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35764,7 +37043,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -35857,7 +37136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36033,7 +37312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36137,7 +37416,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36432,7 +37711,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36535,7 +37814,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36603,7 +37882,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36665,7 +37944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36845,7 +38124,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36886,7 +38165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36916,7 +38195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -36942,7 +38221,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -37460,7 +38739,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -37997,7 +39276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -38185,7 +39464,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #false : bool @@ -38203,10 +39482,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sun Jan 7 03:54:08 -12 2024 +Sun Feb 9 12:28:22 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sun Jan 7 03:54:08 -12 2024 +Sun Feb 9 12:28:22 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -38226,20 +39505,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 7/1/24 + HOL88 Version 2.02 (GCL), built on 9/2/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 7/1/24 +BASIC-HOL version 2.02 (GCL) created 9/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 7/1/24 +HOL-LCF version 2.02 (GCL) created 9/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -38587,7 +39866,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' @@ -39971,12 +41250,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 . @@ -41742,7 +43021,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -43486,7 +44765,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -43741,7 +45020,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -43978,7 +45257,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44156,7 +45435,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44345,7 +45624,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44464,7 +45743,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44580,7 +45859,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44820,7 +46099,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45161,7 +46440,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45368,7 +46647,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45711,7 +46990,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45903,7 +47182,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46171,7 +47450,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46332,7 +47611,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46477,7 +47756,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46629,7 +47908,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46785,7 +48064,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46963,7 +48242,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47159,7 +48438,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47384,7 +48663,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47646,7 +48925,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.07:0357' -> endpages.ps +' TeX output 2025.02.09:1229' -> endpages.ps @@ -47710,7 +48989,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2022.1 (TeX Live 2022) Copyright 2022 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.07:0357' -> titlepages.ps +' TeX output 2025.02.09:1229' -> titlepages.ps @@ -47858,12 +49137,12 @@ 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-source' in '../hol88-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-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-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-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_arm64.buildinfo @@ -47873,12 +49152,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/3870031/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3870031/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/1375620 and its subdirectories -I: Current time: Sun Jan 7 03:58:02 -12 2024 -I: pbuilder-time-stamp: 1704643082 +I: removing directory /srv/workspace/pbuilder/3870031 and its subdirectories +I: Current time: Sun Feb 9 12:29:54 +14 2025 +I: pbuilder-time-stamp: 1739053794