Diff of the two buildlogs: -- --- b1/build.log 2024-05-06 14:39:16.896356325 +0000 +++ b2/build.log 2024-05-06 15:15:33.499760078 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Mon May 6 01:48:11 -12 2024 -I: pbuilder-time-stamp: 1715003291 +I: Current time: Tue May 7 04:39:56 +14 2024 +I: pbuilder-time-stamp: 1715006396 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -28,52 +28,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/15490/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/25046/tmp/hooks/D01_modify_environment starting +debug: Running on ff4a. +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 May 6 14:40 /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/25046/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/25046/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='armhf' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='armhf' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="21" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='06a24fd0ece04b699972ce1414d5321b' - 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='15490' - PS1='# ' - PS2='> ' + INVOCATION_ID=15f000f89a7640e2b8bdf136639e6d13 + LANG=C + LANGUAGE=it_CH:it + LC_ALL=C + MACHTYPE=arm-unknown-linux-gnueabihf + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnueabihf + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=25046 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.uwfyzq7s/pbuilderrc_5yWV --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.uwfyzq7s/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='113' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://10.0.0.15:3142/' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.uwfyzq7s/pbuilderrc_rTDb --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.uwfyzq7s/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=113 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://10.0.0.15:3142/ I: uname -a - Linux virt64c 6.1.0-20-arm64 #1 SMP Debian 6.1.85-1 (2024-04-11) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-20-armmp-lpae #1 SMP Debian 6.1.85-1 (2024-04-11) armv7l GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 May 5 07:43 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/15490/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 6 07:44 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/25046/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -311,7 +343,7 @@ Get: 196 http://deb.debian.org/debian unstable/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 197 http://deb.debian.org/debian unstable/main armhf texlive-base all 2023.20240207-1 [22.0 MB] Get: 198 http://deb.debian.org/debian unstable/main armhf texlive-latex-base all 2023.20240207-1 [1255 kB] -Fetched 176 MB in 9s (18.9 MB/s) +Fetched 176 MB in 12s (15.0 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libapparmor1:armhf. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19445 files and directories currently installed.) @@ -973,8 +1005,8 @@ Setting up tzdata (2024a-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Mon May 6 13:51:24 UTC 2024. -Universal Time is now: Mon May 6 13:51:24 UTC 2024. +Local time is now: Mon May 6 14:42:57 UTC 2024. +Universal Time is now: Mon May 6 14:42:57 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.11-1) ... @@ -1175,7 +1207,11 @@ fakeroot is already the newest version (1.33-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/25046/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/25046/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 @@ -1429,52 +1465,31 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' \ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' @@ -1484,43 +1499,64 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' find -name X.tex -exec rm -rf {} \; dh_clean -X./ml/site.ml.orig -X./contrib/tooltool/Makefile.orig \ -X./contrib/tooltool/events.c.orig -X./contrib/tooltool/func_fix.c.orig \ @@ -1568,7 +1604,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Mon May 6 02:01:10 -12 2024 +Tue May 7 04:49:43 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2806,7 +2842,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 # mem = - : (* -> * list -> bool) @@ -2944,7 +2980,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #.............start address -T 0x7a35e8 () : void @@ -3103,7 +3139,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #.............start address -T 0x7a35e8 () : void @@ -3295,7 +3331,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 # concat = - : (string -> string -> string) @@ -3405,7 +3441,7 @@ start address -T 0x6bba28 ;; Finished loading "lisp/f-ol-net" start address -T 0x7dca40 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 6/5/24 + version 2.02 (GCL) created 7/5/24 #...start address -T 0x6c9650 () : void @@ -3734,7 +3770,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 ###########################() : void @@ -3747,7 +3783,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 ################################################################################################() : void @@ -3892,7 +3928,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 ############################() : void @@ -3935,7 +3971,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 ############################Theory ind loaded () : void @@ -3972,7 +4008,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4013,7 +4049,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4415,7 +4451,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4483,7 +4519,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4688,7 +4724,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4812,7 +4848,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4898,7 +4934,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -4991,7 +5027,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5060,7 +5096,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5165,7 +5201,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5400,7 +5436,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5426,7 +5462,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5554,7 +5590,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5602,7 +5638,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5669,7 +5705,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5728,7 +5764,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5784,7 +5820,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5797,7 +5833,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #() : void @@ -5849,7 +5885,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ##########################() : void @@ -5880,7 +5916,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ##############################() : void @@ -5967,7 +6003,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #######################################################################() : void @@ -6120,7 +6156,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ###########################() : void @@ -6155,7 +6191,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #############################() : void @@ -6216,7 +6252,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ###########################Theory arithmetic loaded () : void @@ -6711,7 +6747,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ##################################() : void @@ -6858,7 +6894,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #################################Theory list loaded () : void @@ -7197,7 +7233,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ###############################Theory list loaded () : void @@ -8694,7 +8730,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #############################() : void @@ -9078,7 +9114,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ############################() : void @@ -9376,7 +9412,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ############################() : void @@ -9516,7 +9552,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ############################################() : void @@ -9613,7 +9649,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 ##################################() : void @@ -9643,7 +9679,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -9660,7 +9696,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #Theory num loaded () : void @@ -9679,7 +9715,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -9836,7 +9872,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 # @@ -9874,7 +9910,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 # @@ -9908,7 +9944,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -9993,7 +10029,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -10034,7 +10070,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -10218,7 +10254,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 # define_load_lib_function = - : (string list -> void -> void) @@ -10294,7 +10330,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10307,7 +10343,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #() : void @@ -10371,11 +10407,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Mon May 6 02:10:52 -12 2024 +Tue May 7 04:56:12 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Mon May 6 02:10:53 -12 2024 +Tue May 7 04:56:13 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10398,7 +10434,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -10482,7 +10518,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -10588,7 +10624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11338,7 +11374,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11361,7 +11397,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11404,7 +11440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11440,7 +11476,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11492,7 +11528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11524,7 +11560,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11562,7 +11598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11590,7 +11626,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11667,7 +11703,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11689,7 +11725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11743,7 +11779,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11792,7 +11828,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11943,7 +11979,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -11987,7 +12023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12062,7 +12098,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12112,7 +12148,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12175,7 +12211,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12228,7 +12264,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12274,7 +12310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12362,7 +12398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12400,7 +12436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12461,7 +12497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12525,7 +12561,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12551,7 +12587,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12576,7 +12612,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12615,7 +12651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -12691,7 +12727,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13428,7 +13464,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13451,7 +13487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13494,7 +13530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13529,7 +13565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13570,7 +13606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13633,7 +13669,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13656,7 +13692,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13681,7 +13717,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13708,7 +13744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -13744,7 +13780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14276,7 +14312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14299,7 +14335,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14333,7 +14369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14388,7 +14424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14479,7 +14515,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14648,7 +14684,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -14793,7 +14829,7 @@ Intermediate theorems generated: 24 WOSET_POSET = |- !l. woset l ==> poset l -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 98 WOSET_FLEQ = |- !l. woset l ==> (!x. fl l x = l(x,x)) @@ -14881,7 +14917,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14891,7 +14927,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (!n. ?f. !x. l(ms x,n) ==> (f x = h f x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14911,12 +14947,12 @@ (!f g x. (!y. less l(ms y,ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... LESS_EQ_REFL = |- !m. m <= m -Run time: 0.0s +Run time: 0.1s FL_NUM = |- !n. fl(\(m,n). m <= n)n Run time: 0.0s @@ -14975,7 +15011,7 @@ Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 240 LINSEG_WOSET = |- !l a. woset l ==> woset(linseg l a) @@ -15000,7 +15036,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1172 EXTEND_FL = @@ -15030,7 +15066,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.0s +Run time: 0.1s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -15064,7 +15100,7 @@ WO_FL_RESTRICT = |- !l. woset l ==> (!P. fl(\(x,y). P x /\ P y /\ l(x,y))x = P x /\ fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -15101,7 +15137,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1083 () : void @@ -15111,7 +15147,7 @@ File mk_wellorder loaded () : void -Run time: 0.9s +Run time: 1.3s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15120,7 +15156,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -15244,14 +15280,14 @@ File ../../Library/abs_theory/monoid_def.ml loaded () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 614 Making ../../Library/abs_theory/group_def.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -15296,7 +15332,7 @@ Intermediate theorems generated: 601 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 GROUP_EXTENDS_MONOID = ... |- IS_MONOID(monoid(fn g)(id g)) @@ -15317,7 +15353,7 @@ Intermediate theorems generated: 6 LEFT_CANCELLATION = ... |- !x y a. (fn g a x = fn g a y) ==> (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 67 INVERSE_INVERSE_LEMMA = |- !g. IS_GROUP g ==> (!a. inv g(inv g a) = a) @@ -15343,7 +15379,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -15393,11 +15429,11 @@ Run time: 0.0s GROUP_THOBS = |- IS_GROUP(group(\x y. ~(x = y))F I) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) @@ -15405,7 +15441,7 @@ Intermediate theorems generated: 732 |- !a. I(I a) = a -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1106 concrete_rep = "group(\x y. x = y)T I" : term @@ -15432,15 +15468,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Mon May 6 02:14:19 -12 2024 +===> abs_theory rebuilt on Tue May 7 04:59:24 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -15600,7 +15636,7 @@ File abs_theory compiled () : void -Run time: 0.0s +Run time: 0.1s make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals' @@ -15613,7 +15649,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -15809,7 +15845,7 @@ Intermediate theorems generated: 62 TRAT_MUL_SYM_EQ = |- !h i. h trat_mul i = i trat_mul h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 58 TRAT_INV_WELLDEFINED = @@ -15913,7 +15949,7 @@ h trat_eq i \/ (?d. h trat_eq (i trat_add d)) \/ (?d. i trat_eq (h trat_add d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) @@ -15980,7 +16016,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -16040,7 +16076,7 @@ File hrat.ml loaded () : void -Run time: 0.4s +Run time: 0.6s Intermediate theorems generated: 11032 #\ @@ -16050,7 +16086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -16247,12 +16283,12 @@ HRAT_LT_MUL2 = |- !u v x y. u hrat_lt x /\ v hrat_lt y ==> (u hrat_mul v) hrat_lt (x hrat_mul y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 HRAT_LT_LMUL = |- !x y z. (z hrat_mul x) hrat_lt (z hrat_mul y) = x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 149 HRAT_LT_RMUL = @@ -16360,7 +16396,7 @@ Intermediate theorems generated: 37 CUT_DOWN = |- !X x y. cut X x /\ y hrat_lt x ==> cut X y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 49 CUT_UP = |- !X x. cut X x ==> (?y. cut X y /\ x hrat_lt y) @@ -16377,7 +16413,7 @@ Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... LESS_SUC_REFL = |- !n. n < (SUC n) -Run time: 0.1s +Run time: 0.0s Theorem NOT_LESS_0 autoloading from theory `prim_rec` ... NOT_LESS_0 = |- !n. ~n < 0 @@ -16421,7 +16457,7 @@ |- !X Y. X hreal_mul Y = hreal(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 hreal_inv = @@ -16451,12 +16487,12 @@ HREAL_ADD_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 521 HREAL_MUL_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X @@ -16508,12 +16544,12 @@ HREAL_SUB_ISACUT = |- !X Y. X hreal_lt Y ==> isacut(\w. ?x. ~cut X x /\ cut Y(x hrat_add w)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 400 HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16550,7 +16586,7 @@ File hreal.ml loaded () : void -Run time: 0.5s +Run time: 0.7s Intermediate theorems generated: 10456 #\ @@ -16560,7 +16596,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -16657,7 +16693,7 @@ File equiv loaded () : void -Run time: 0.0s +Run time: 0.1s Theorem HREAL_LDISTRIB autoloading from theory `HREAL` ... HREAL_LDISTRIB = @@ -16810,7 +16846,7 @@ TREAL_EQ_TRANS = |- !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1147 TREAL_EQ_EQUIV = |- !p q. p treal_eq q = ($treal_eq p = $treal_eq q) @@ -16868,7 +16904,7 @@ Intermediate theorems generated: 217 TREAL_ADD_LINV = |- !x. ((treal_neg x) treal_add x) treal_eq treal_0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 Theorem HREAL_SUB_ADD autoloading from theory `HREAL` ... @@ -16900,12 +16936,12 @@ 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 = |- !x y z. y treal_lt z ==> (x treal_add y) treal_lt (x treal_add z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1045 TREAL_LT_MUL = @@ -16932,7 +16968,7 @@ TREAL_ISO = |- !h i. h hreal_lt i ==> (treal_of_hreal h) treal_lt (treal_of_hreal i) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 450 TREAL_BIJ_WELLDEF = @@ -16942,7 +16978,7 @@ TREAL_NEG_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 58 TREAL_ADD_WELLDEFR = @@ -16978,7 +17014,7 @@ TREAL_LT_WELLDEFL = |- !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 TREAL_LT_WELLDEF = @@ -16990,7 +17026,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -17019,7 +17055,7 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -17035,7 +17071,7 @@ |- (!x. P x ==> r0 real_lt x) ==> ((?x. P x /\ y real_lt x) = (?X. P(real_of_hreal X) /\ y real_lt (real_of_hreal X))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 SUP_ALLPOS_LEMMA2 = |- P(real_of_hreal X) = (\h. P(real_of_hreal h))X @@ -17098,7 +17134,7 @@ File realax.ml loaded () : void -Run time: 0.9s +Run time: 1.1s Intermediate theorems generated: 26795 #\ @@ -17108,7 +17144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -17214,7 +17250,7 @@ Intermediate theorems generated: 136 REAL_0 = |- r0 = real_of_num 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 11 REAL_1 = |- r1 = real_of_num 1 @@ -17304,7 +17340,7 @@ Intermediate theorems generated: 12 REAL_ADD_RID = |- !x. x + (& 0) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 14 REAL_ADD_RINV = |- !x. x + (-- x) = & 0 @@ -17344,7 +17380,7 @@ Intermediate theorems generated: 10 REAL_RNEG_UNIQ = |- !x y. (x + y = & 0) = (y = -- x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) @@ -17420,11 +17456,11 @@ Intermediate theorems generated: 21 REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 125 REAL_LT_IMP_LE = |- !x y. x < y ==> x <= y @@ -17480,7 +17516,7 @@ Intermediate theorems generated: 73 REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) @@ -17488,7 +17524,7 @@ Intermediate theorems generated: 68 REAL_LE_01 = |- (& 0) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 6 REAL_LT_01 = |- (& 0) < (& 1) @@ -17532,7 +17568,7 @@ Intermediate theorems generated: 75 REAL_SUB_ADD = |- !x y. (x - y) + y = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 50 REAL_SUB_ADD2 = |- !x y. y + (x - y) = x @@ -17564,7 +17600,7 @@ Intermediate theorems generated: 45 REAL_NEG_0 = |- --(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x @@ -17584,7 +17620,7 @@ Intermediate theorems generated: 61 REAL_EQ_LMUL = |- !x y z. (x * y = x * z) = (x = & 0) \/ (y = z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 122 REAL_EQ_RMUL = |- !x y z. (x * z = y * z) = (z = & 0) \/ (x = y) @@ -17624,11 +17660,11 @@ Intermediate theorems generated: 133 REAL_LT_LMUL_0 = |- !x y. (& 0) < x ==> ((& 0) < (x * y) = (& 0) < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 87 REAL_LT_RMUL_0 = |- !x y. (& 0) < y ==> ((& 0) < (x * y) = (& 0) < x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) @@ -17676,7 +17712,7 @@ Intermediate theorems generated: 20 REAL_LT_ADDL = |- !x y. y < (x + y) = (& 0) < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 REAL = |- !n. &(SUC n) = (& n) + (& 1) @@ -17753,7 +17789,7 @@ Intermediate theorems generated: 26 REAL_OVER1 = |- !x. x / (& 1) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) @@ -17818,7 +17854,7 @@ Intermediate theorems generated: 22 REAL_DOUBLE = |- !x. x + x = (& 2) * x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 37 REAL_DIV_LMUL = |- !x y. ~(y = & 0) ==> (y * (x / y) = x) @@ -17843,7 +17879,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -17855,7 +17891,7 @@ Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y @@ -17879,7 +17915,7 @@ Intermediate theorems generated: 73 REAL_SUB_LZERO = |- !x. (& 0) - x = -- x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 REAL_SUB_RZERO = |- !x. x - (& 0) = x @@ -17906,7 +17942,7 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 < x2 /\ y1 < y2 ==> (x1 * y1) < (x2 * y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) @@ -17926,7 +17962,7 @@ Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 93 REAL_EQ_SUB_LADD = |- !x y z. (x = y - z) = (x + z = y) @@ -17947,7 +17983,7 @@ Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_SUB_INV2 = @@ -17957,7 +17993,7 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y @@ -17980,11 +18016,11 @@ Intermediate theorems generated: 345 REAL_LE_LDIV = |- !x y z. (& 0) < x /\ y <= (z * x) ==> (y / x) <= z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 REAL_LE_RDIV = |- !x y z. (& 0) < x /\ (y * x) <= z ==> y <= (z / x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 101 REAL_LT_1 = |- !x y. (& 0) <= x /\ x < y ==> (x / y) < (& 1) @@ -18010,7 +18046,7 @@ Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) @@ -18042,7 +18078,7 @@ Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_DIV_MUL2 = @@ -18059,11 +18095,11 @@ Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 @@ -18087,7 +18123,7 @@ Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 385 ABS_LT_MUL2 = @@ -18104,7 +18140,7 @@ Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 105 ABS_ABS = |- !x. abs(abs x) = abs x @@ -18120,12 +18156,12 @@ Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 ABS_BETWEEN = |- !x y d. (& 0) < d /\ (x - d) < y /\ y < (x + d) = (abs(y - x)) < d -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) @@ -18145,7 +18181,7 @@ Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) @@ -18153,7 +18189,7 @@ Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 41 ABS_CIRCLE = @@ -18166,7 +18202,7 @@ Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 ABS_BETWEEN2 = @@ -18179,7 +18215,7 @@ Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -18236,7 +18272,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) @@ -18248,7 +18284,7 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 @@ -18260,7 +18296,7 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) @@ -18284,14 +18320,14 @@ Intermediate theorems generated: 103 POW_MINUS1 = |- !n. (--(& 1)) pow (2 num_mul n) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 231 REAL_SUP_SOMEPOS = |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -18318,7 +18354,7 @@ Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 REAL_SUP = @@ -18355,7 +18391,7 @@ Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 342 Theorem PRE autoloading from theory `prim_rec` ... @@ -18380,7 +18416,7 @@ Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 Sum = @@ -18393,11 +18429,11 @@ Intermediate theorems generated: 109 SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -18423,7 +18459,7 @@ Intermediate theorems generated: 82 SUM_POS = |- !f. (!n. (& 0) <= (f n)) ==> (!m n. (& 0) <= (Sum(m,n)f)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 78 SUM_POS_GEN = @@ -18457,7 +18493,7 @@ |- !f N. (!n. n num_ge N ==> (f n = & 0)) ==> (!m n. m num_ge N ==> (Sum(m,n)f = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 145 SUM_ADD = @@ -18475,7 +18511,7 @@ SUM_SUB = |- !f g m n. Sum(m,n)(\n. (f n) - (g n)) = (Sum(m,n)f) - (Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 74 Theorem LESS_MONO_ADD autoloading from theory `arithmetic` ... @@ -18511,12 +18547,12 @@ |- !f K m n. (!p. m num_le p /\ p num_lt (m num_add n) ==> (f p) <= K) ==> (Sum(m,n)f) <= ((& n) * K) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 226 SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18568,7 +18604,7 @@ Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... LESS_ADD_1 = |- !m n. n num_lt m ==> (?p. m = n num_add (p num_add 1)) -Run time: 0.0s +Run time: 0.1s Definition LESS_OR_EQ autoloading from theory `arithmetic` ... LESS_OR_EQ = |- !m n. m num_le n = m num_lt n \/ (m = n) @@ -18577,7 +18613,7 @@ Theorem LESS_EQ autoloading from theory `arithmetic` ... LESS_EQ = |- !m n. m num_lt n = (SUC m) num_le n -Run time: 0.1s +Run time: 0.0s Theorem LESS_CASES autoloading from theory `arithmetic` ... LESS_CASES = |- !m n. m num_lt n \/ n num_le m @@ -18587,23 +18623,23 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2469 SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File real.ml loaded () : void -Run time: 2.9s +Run time: 4.2s Intermediate theorems generated: 23746 #\ @@ -18613,7 +18649,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -18687,7 +18723,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s [] : (string # string) list Run time: 0.0s @@ -18791,7 +18827,7 @@ OPEN_UNOPEN = |- !S top. open top S = (re_Union(\P. open top P /\ P re_subset S) = S) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 212 OPEN_SUBOPEN = @@ -18854,7 +18890,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 560 metric_tybij = @@ -18863,7 +18899,7 @@ Intermediate theorems generated: 4 METRIC_ISMET = |- !m. ismet(dist m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 METRIC_ZERO = |- !m x y. (dist m(x,y) = & 0) = (x = y) @@ -18931,7 +18967,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18973,7 +19009,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -19097,7 +19133,7 @@ File topology.ml loaded () : void -Run time: 0.3s +Run time: 0.6s Intermediate theorems generated: 4132 #\ @@ -19107,7 +19143,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -19281,7 +19317,7 @@ 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 -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_CASES autoloading from theory `arithmetic` ... LESS_EQ_CASES = |- !m n. m num_le n \/ n num_le m @@ -19384,7 +19420,7 @@ dorder g ==> (x --> x0)(mtop d,g) /\ (x --> x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 313 SEQ_TENDS = @@ -19481,7 +19517,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.0s +Run time: 0.1s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19504,7 +19540,7 @@ NET_CONV_BOUNDED = |- !g x x0. (x --> x0)(mtop mr1,g) ==> bounded(mr1,g)x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 119 Theorem REAL_LT_REFL autoloading from theory `REAL` ... @@ -19588,7 +19624,7 @@ (!x y. (x --> (& 0))(mtop mr1,g) /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) + (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 324 Theorem REAL_LT_MUL2 autoloading from theory `REAL` ... @@ -19690,7 +19726,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 NET_SUB = @@ -19775,7 +19811,7 @@ (!x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) --> (inv x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1253 NET_DIV = @@ -19784,7 +19820,7 @@ (!x x0 y y0. (x --> x0)(mtop mr1,g) /\ (y --> y0)(mtop mr1,g) /\ ~(y0 = & 0) ==> ((\n. (x n) / (y n)) --> (x0 / y0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 106 Theorem ABS_SUB_ABS autoloading from theory `REAL` ... @@ -19832,7 +19868,7 @@ File nets.ml loaded () : void -Run time: 0.5s +Run time: 0.7s Intermediate theorems generated: 7389 #\ @@ -19842,7 +19878,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -19947,7 +19983,7 @@ Intermediate theorems generated: 34 () : void -Run time: 0.1s +Run time: 0.0s [(); ()] : void list Run time: 0.0s @@ -20222,7 +20258,7 @@ Theorem NOT_LESS_0 autoloading from theory `prim_rec` ... NOT_LESS_0 = |- !n. ~n num_lt 0 -Run time: 0.0s +Run time: 0.1s MAX_LEMMA = |- !s N. ?k. !n. n num_lt N ==> (abs(s n)) < k Run time: 0.0s @@ -20356,7 +20392,7 @@ |- !f. bounded(mr1,$num_ge)f /\ (!m n. m num_ge n ==> (f m) >= (f n)) ==> convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 910 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -20500,7 +20536,7 @@ Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... REAL_SUB_RZERO = |- !x. x - (& 0) = x -Run time: 0.0s +Run time: 0.1s SEQ_ABS = |- !f. (\n. abs(f n)) --> (& 0) = f --> (& 0) Run time: 0.0s @@ -20531,7 +20567,7 @@ Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... REAL_LT_IMP_NE = |- !x y. x < y ==> ~(x = y) -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT_TRANS autoloading from theory `REAL` ... REAL_LT_TRANS = |- !x y z. x < y /\ y < z ==> x < z @@ -20615,7 +20651,7 @@ Theorem POW_ABS autoloading from theory `REAL` ... POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.0s +Run time: 0.1s SEQ_POWER = |- !c. (abs c) < (& 1) ==> (\n. c pow n) --> (& 0) Run time: 0.0s @@ -20647,7 +20683,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20661,7 +20697,7 @@ (!n. (f n) <= (g n)) /\ (\n. (f n) - (g n)) --> (& 0) ==> (?l. ((!n. (f n) <= l) /\ f --> l) /\ (!n. l <= (g n)) /\ g --> l) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 295 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -20798,7 +20834,7 @@ Intermediate theorems generated: 16 SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) @@ -20890,7 +20926,7 @@ SER_PAIR = |- !f. summable f ==> (\n. Sum(2 num_mul n,2)f) sums (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 Theorem SUM_OFFSET autoloading from theory `REAL` ... @@ -20922,7 +20958,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -20933,7 +20969,7 @@ SER_ADD = |- !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. (x n) + (y n)) sums (x0 + y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 Theorem SUM_CMUL autoloading from theory `REAL` ... @@ -20992,7 +21028,7 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 395 SER_COMPARA = @@ -21059,7 +21095,7 @@ |- !x. ~(x = & 1) ==> (!n. Sum(0,n)(\n'. x pow n') = ((x pow n) - (& 1)) / (x - (& 1))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 411 Theorem REAL_NEG_INV autoloading from theory `REAL` ... @@ -21096,7 +21132,7 @@ ABS_NEG_LEMMA = |- !c. c <= (& 0) ==> (!x y. (abs x) <= (c * (abs y)) ==> (x = & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 114 Theorem REAL_LE_LMUL autoloading from theory `REAL` ... @@ -21120,13 +21156,13 @@ Intermediate theorems generated: 683 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File seq.ml loaded () : void -Run time: 1.1s +Run time: 1.5s Intermediate theorems generated: 18704 #\ @@ -21136,7 +21172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -21452,7 +21488,7 @@ Run time: 0.0s LIM_UNIQ = |- !f l m x. (f --> l)x /\ (f --> m)x ==> (l = m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 LIM_EQUAL = @@ -21492,7 +21528,7 @@ Theorem REAL_DOWN2 autoloading from theory `REAL` ... REAL_DOWN2 = |- !x y. (& 0) < x /\ (& 0) < y ==> (?z. (& 0) < z /\ z < x /\ z < y) -Run time: 0.1s +Run time: 0.0s Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... REAL_SUB_RZERO = |- !x. x - (& 0) = x @@ -21546,7 +21582,7 @@ Run time: 0.0s CONTL_LIM = |- !f x. f contl x = (f --> (f x))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 275 CONT_CONST = |- !x. (\x. k) contl x @@ -21658,7 +21694,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.1s +Run time: 0.0s IVT = |- !f a b y. @@ -21666,7 +21702,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21828,7 +21864,7 @@ ((f(g(x + h))) - (f(g x))) / h = (((f(g(x + h))) - (f(g x))) / ((g(x + h)) - (g x))) * (((g(x + h)) - (g x)) / h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 170 Theorem REAL_LT_RADD autoloading from theory `REAL` ... @@ -21866,7 +21902,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21960,7 +21996,7 @@ |- !f l x. (f diffl l)x /\ ~(f x = & 0) ==> ((\x. inv(f x)) diffl (--(l / ((f x) pow 2))))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 106 Theorem REAL_MUL_RINV autoloading from theory `REAL` ... @@ -22023,7 +22059,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22104,7 +22140,7 @@ |- !f x l. (f diffl l)x /\ (& 0) < l ==> (?d. (& 0) < d /\ (!h. (& 0) < h /\ h < d ==> (f x) < (f(x + h)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 270 Theorem REAL_NEG_LE0 autoloading from theory `REAL` ... @@ -22127,7 +22163,7 @@ |- !f x l. (f diffl l)x /\ l < (& 0) ==> (?d. (& 0) < d /\ (!h. (& 0) < h /\ h < d ==> (f x) < (f(x - h)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 469 Theorem REAL_ADD_SUB2 autoloading from theory `REAL` ... @@ -22252,7 +22288,7 @@ File lim.ml loaded () : void -Run time: 1.1s +Run time: 1.6s Intermediate theorems generated: 21608 #\ @@ -22262,7 +22298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -22337,7 +22373,7 @@ File useful loaded () : void -Run time: 0.1s +Run time: 0.0s real_interface_map = [(`--`, `real_neg`); @@ -22371,7 +22407,7 @@ Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22657,7 +22693,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (abs(f n)) * (z pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22696,7 +22732,7 @@ Sum(0,n)(\n'. (diffs c n') * (x pow n')) = (Sum(0,n)(\n'. (& n') * ((c n') * (x pow (n' num_sub 1))))) + ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 229 Theorem REAL_EQ_SUB_LADD autoloading from theory `REAL` ... @@ -22833,7 +22869,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -23012,7 +23048,7 @@ (& 0) < (abs h) /\ (abs h) < k ==> (!n. (abs(g h n)) <= ((f n) * (abs h)))) ==> ((\h. suminf(g h)) tends_real_real (& 0))(& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 502 Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... @@ -23026,7 +23062,7 @@ Theorem REAL_LE_LMUL_IMP autoloading from theory `REAL` ... REAL_LE_LMUL_IMP = |- !x y z. (& 0) <= x /\ y <= z ==> (x * y) <= (x * z) -Run time: 0.1s +Run time: 0.0s Theorem REAL_MUL_RINV autoloading from theory `REAL` ... REAL_MUL_RINV = |- !x. ~(x = & 0) ==> (x * (inv x) = & 1) @@ -23114,7 +23150,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -23124,7 +23160,7 @@ File powser.ml loaded () : void -Run time: 0.6s +Run time: 0.8s Intermediate theorems generated: 8507 #\ @@ -23134,7 +23170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -23209,7 +23245,7 @@ File useful loaded () : void -Run time: 0.0s +Run time: 0.1s false : bool Run time: 0.0s @@ -23302,7 +23338,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23532,7 +23568,7 @@ Theorem REAL_DOWN autoloading from theory `REAL` ... REAL_DOWN = |- !x. (& 0) < x ==> (?y. (& 0) < y /\ y < x) -Run time: 0.1s +Run time: 0.0s Theorem SER_RATIO autoloading from theory `SEQ` ... SER_RATIO = @@ -23690,7 +23726,7 @@ & 0 | ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 407 Theorem SER_NEG autoloading from theory `SEQ` ... @@ -23834,7 +23870,7 @@ Run time: 0.0s EXP_LE_X = |- !x. (& 0) <= x ==> ((& 1) + x) <= (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 420 EXP_LT_1 = |- !x. (& 0) < x ==> (& 1) < (exp x) @@ -23883,7 +23919,7 @@ Run time: 0.0s EXP_ADD = |- !x y. exp(x + y) = (exp x) * (exp y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 71 Theorem REAL_LE_SQUARE autoloading from theory `REAL` ... @@ -23963,7 +23999,7 @@ Run time: 0.0s EXP_INJ = |- !x y. (exp x = exp y) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 39 Theorem DIFF_CONT autoloading from theory `LIM` ... @@ -24051,7 +24087,7 @@ Run time: 0.0s LN_INV = |- !x. (& 0) < x ==> (ln(inv x) = --(ln x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 81 LN_DIV = |- !x. (& 0) < x /\ (& 0) < y ==> (ln(x / y) = (ln x) - (ln y)) @@ -24065,7 +24101,7 @@ LN_MONO_LE = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x) <= (ln y) = x <= y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 LN_POW = |- !n x. (& 0) < x ==> (ln(x pow n) = (& n) * (ln x)) @@ -24140,7 +24176,7 @@ Run time: 0.0s SIN_0 = |- sin(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -24154,7 +24190,7 @@ Run time: 0.0s COS_0 = |- cos(& 0) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 @@ -24214,7 +24250,7 @@ Intermediate theorems generated: 160 COS_BOUNDS = |- !x. (--(& 1)) <= (cos x) /\ (cos x) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -24253,7 +24289,7 @@ |- !x. (((sin(-- x)) + (sin x)) pow 2) + (((cos(-- x)) - (cos x)) pow 2) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1099 Theorem REAL_SUMSQ autoloading from theory `REAL` ... @@ -24267,7 +24303,7 @@ COS_ADD = |- !x y. cos(x + y) = ((cos x) * (cos y)) - ((sin x) * (sin y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 Theorem REAL_LNEG_UNIQ autoloading from theory `REAL` ... @@ -24403,7 +24439,7 @@ Run time: 0.0s COS_2 = |- (cos(& 2)) < (& 0) -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 3794 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -24487,7 +24523,7 @@ Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -24523,7 +24559,7 @@ Intermediate theorems generated: 47 COS_PERIODIC = |- !x. cos(x + ((& 2) * pi)) = cos x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 47 COS_NPI = |- !n. cos((& n) * pi) = (--(& 1)) pow n @@ -24544,7 +24580,7 @@ Theorem REAL_LT_NEG autoloading from theory `REAL` ... REAL_LT_NEG = |- !x y. (-- x) < (-- y) = y < x -Run time: 0.1s +Run time: 0.0s COS_POS_PI = |- !x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) @@ -24571,7 +24607,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (& 0) <= x /\ x <= pi /\ (cos x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 766 Theorem REAL_EQ_RADD autoloading from theory `REAL` ... @@ -24687,11 +24723,11 @@ Intermediate theorems generated: 2 TAN_0 = |- tan(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 TAN_PI = |- tan pi = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 TAN_NPI = |- !n. tan((& n) * pi) = & 0 @@ -24723,7 +24759,7 @@ |- !x y. ~(cos x = & 0) /\ ~(cos y = & 0) /\ ~(cos(x + y) = & 0) ==> (tan(x + y) = ((tan x) + (tan y)) / ((& 1) - ((tan x) * (tan y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 869 TAN_DOUBLE = @@ -24742,7 +24778,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24788,7 +24824,7 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1046 TAN_TOTAL_POS = @@ -24865,11 +24901,11 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi /\ (cos(acs y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 ACS_BOUNDS = @@ -24900,7 +24936,7 @@ TAN_ATN = |- !x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) ==> (atn(tan x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 () : void @@ -24910,7 +24946,7 @@ File transc.ml loaded () : void -Run time: 1.9s +Run time: 2.6s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24923,7 +24959,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -24945,7 +24981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25011,7 +25047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25043,7 +25079,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25152,7 +25188,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25305,7 +25341,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25378,7 +25414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25458,7 +25494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25615,7 +25651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25770,7 +25806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -25987,7 +26023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26009,7 +26045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26028,7 +26064,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26073,7 +26109,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26138,7 +26174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26188,7 +26224,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26258,7 +26294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26328,7 +26364,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26364,7 +26400,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26417,7 +26453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26489,7 +26525,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26568,7 +26604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26763,7 +26799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -26800,7 +26836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -27361,2182 +27397,38 @@ WSPLIT_WSEG2 = |- !n. !w :: PWORDLEN n. !k. k <= n ==> (SND(WSPLIT k w) = WSEG k 0 w) -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) - -WORD_SPLIT = -|- !n1 n2. !w :: PWORDLEN(n1 + n2). w = WCAT(WSEG n1 n2 w,WSEG n2 0 w) - -WORDLEN_SUC_WCAT_WSEG_WSEG = -|- !w :: PWORDLEN(SUC n). w = WCAT(WSEG 1 n w,WSEG n 0 w) - -WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT = -|- !w :: PWORDLEN(SUC n). w = WCAT(WSEG n 1 w,WSEG 1 0 w) - -WORDLEN_SUC_WCAT_BIT_WSEG = -|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WORD[BIT n w],WSEG n 0 w) - -WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT = -|- !n. !w :: PWORDLEN(SUC n). w = WCAT(WSEG n 1 w,WORD[BIT 0 w]) - -WSEG_WCAT1 = -|- !n1 n2. - !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n1 n2(WCAT(w1,w2)) = w1 - -WSEG_WCAT2 = -|- !n1 n2. - !w1 :: PWORDLEN n1. !w2 :: PWORDLEN n2. WSEG n2 0(WCAT(w1,w2)) = w2 - -Theorem CONS_APPEND autoloading from theory `list` ... -CONS_APPEND = |- !x l. CONS x l = APPEND[x]l - -WORD_CONS_WCAT = |- !x l. WORD(CONS x l) = WCAT(WORD[x],WORD l) - -Theorem SNOC_APPEND autoloading from theory `list` ... -SNOC_APPEND = |- !x l. SNOC x l = APPEND l[x] - -WORD_SNOC_WCAT = |- !x l. WORD(SNOC x l) = WCAT(WORD l,WORD[x]) - -Theorem ELL_APPEND1 autoloading from theory `list` ... -ELL_APPEND1 = -|- !l2 n. - (LENGTH l2) <= n ==> - (!l1. ELL n(APPEND l1 l2) = ELL(n - (LENGTH l2))l1) - -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 ELL_APPEND2 autoloading from theory `list` ... -ELL_APPEND2 = -|- !n l2. n < (LENGTH l2) ==> (!l1. ELL n(APPEND l1 l2) = ELL n l2) - -BIT_WCAT_SND = -|- !n1 n2. - !w1 :: PWORDLEN n1. - !w2 :: PWORDLEN n2. !k. k < n2 ==> (BIT k(WCAT(w1,w2)) = BIT k w2) - -Theorem ELL_LENGTH_CONS autoloading from theory `list` ... -ELL_LENGTH_CONS = |- !l x. ELL(LENGTH l)(CONS x l) = x - -BIT_WCAT1 = |- !n. !w :: PWORDLEN n. !b. BIT n(WCAT(WORD[b],w)) = b - -Theorem BUTLASTN_APPEND1 autoloading from theory `list` ... -BUTLASTN_APPEND1 = -|- !l2 n. - (LENGTH l2) <= n ==> - (!l1. BUTLASTN n(APPEND l1 l2) = BUTLASTN(n - (LENGTH l2))l1) - -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 LASTN_APPEND2 autoloading from theory `list` ... -LASTN_APPEND2 = -|- !n l2. n <= (LENGTH l2) ==> (!l1. LASTN n(APPEND l1 l2) = LASTN n l2) - -WSEG_WCAT_WSEG2 = -|- !n1 n2. - !w1 :: PWORDLEN n1. - !w2 :: PWORDLEN n2. - !m k. (m + k) <= n2 ==> (WSEG m k(WCAT(w1,w2)) = WSEG m k w2) - -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)) - -PWORDLEN_BIT1 = |- !x. PWORDLEN 1(WORD[x]) - -Theorem LESS_SUC autoloading from theory `prim_rec` ... -LESS_SUC = |- !m n. m < n ==> m < (SUC n) - -Theorem CONS_11 autoloading from theory `list` ... -CONS_11 = |- !h t h' t'. (CONS h t = CONS h' t') = (h = h') /\ (t = t') - -BIT_EQ_IMP_WORD_EQ = -|- !n. - !w1 w2 :: PWORDLEN n. - (!k. k < n ==> (BIT k w1 = BIT k w2)) ==> (w1 = w2) - -() : void - - -File mk_word_base loaded -() : void - -#rm -f word_bitop.th -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadt `mk_word_bitop`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 -=============================================================================== - -#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_base loaded -() : void - -() : void - -() : void - -...() : void - -Theorem SUB_LESS_EQ autoloading from theory `arithmetic` ... -SUB_LESS_EQ = |- !n m. (n - m) <= n - -Theorem SEG_LASTN_BUTLASTN autoloading from theory `list` ... -SEG_LASTN_BUTLASTN = -|- !n m l. - (n + m) <= (LENGTH l) ==> - (SEG n m l = LASTN n(BUTLASTN((LENGTH l) - (n + m))l)) - -LASTN_BUTLASTN_SEG = -|- !m k l. - (m + k) <= (LENGTH l) ==> - (LASTN m(BUTLASTN k l) = SEG m((LENGTH l) - (m + k))l) - -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_PWORDLEN = -|- !op :: PBITOP. !n. !w :: PWORDLEN n. PWORDLEN n(op w) - -PBITOP_WSEG = -|- !op :: PBITOP. - !n. - !w :: PWORDLEN n. - !m k. (m + k) <= n ==> (op(WSEG m k w) = WSEG m k(op w)) - -Theorem LESS_EQ autoloading from theory `arithmetic` ... -LESS_EQ = |- !m n. m < n = (SUC m) <= n - -Theorem WSEG_BIT autoloading from theory `word_base` ... -WSEG_BIT = -|- !n. !w :: PWORDLEN n. !k. k < n ==> (WSEG 1 k w = WORD[BIT k w]) - -PBITOP_BIT = -|- !op :: PBITOP. - !n. - !w :: PWORDLEN n. - !k. k < n ==> (op(WORD[BIT k w]) = WORD[BIT k(op w)]) - -Theorem BIT0 autoloading from theory `word_base` ... -BIT0 = |- !b. BIT 0(WORD[b]) = b - -BIT_op_EXISTS = -|- !op :: PBITOP. - ?op'. - !n. !w :: PWORDLEN n. !k. k < n ==> (BIT k(op w) = op'(BIT k w)) - -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_PWORDLEN = -|- !op :: PBITBOP. - !n. !w1 :: PWORDLEN n. !w2 :: PWORDLEN n. PWORDLEN n(op w1 w2) - -PBITBOP_WSEG = -|- !op :: PBITBOP. - !n. - !w1 :: PWORDLEN n. - !w2 :: PWORDLEN n. - !m k. - (m + k) <= n ==> - (op(WSEG m k w1)(WSEG m k w2) = WSEG m k(op w1 w2)) - -Theorem word_Ax autoloading from theory `word_base` ... -word_Ax = |- !f. ?! fn. !l. fn(WORD l) = f l - -PBITBOP_EXISTS = -|- !f. ?fn. !l1 l2. fn(WORD l1)(WORD l2) = WORD(MAP2 f l1 l2) - -WMAP_DEF = |- !f l. WMAP f(WORD l) = WORD(MAP f l) - -Theorem LENGTH_MAP autoloading from theory `list` ... -LENGTH_MAP = |- !l f. LENGTH(MAP f l) = LENGTH l - -Definition PWORDLEN_DEF autoloading from theory `word_base` ... -PWORDLEN_DEF = |- !n l. PWORDLEN n(WORD l) = (n = LENGTH l) - -WMAP_PWORDLEN = |- !w :: PWORDLEN n. !f. PWORDLEN n(WMAP f w) - -Definition MAP autoloading from theory `list` ... -MAP = -|- (!f. MAP f[] = []) /\ (!f h t. MAP f(CONS h t) = CONS(f h)(MAP f t)) - -WMAP0 = |- !f. WMAP f(WORD[]) = WORD[] - -Theorem ELL_MAP autoloading from theory `list` ... -ELL_MAP = |- !n l f. n < (LENGTH l) ==> (ELL n(MAP f l) = f(ELL n l)) - -Definition BIT_DEF autoloading from theory `word_base` ... -BIT_DEF = |- !k l. BIT k(WORD l) = ELL k l - -WMAP_BIT = -|- !n. - !w :: PWORDLEN n. !k. k < n ==> (!f. BIT k(WMAP f w) = f(BIT k w)) - -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') - -Definition WSEG_DEF autoloading from theory `word_base` ... -WSEG_DEF = |- !m k l. WSEG m k(WORD l) = WORD(LASTN m(BUTLASTN k l)) - -WMAP_WSEG = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> (!f. WMAP f(WSEG m k w) = WSEG m k(WMAP f w)) - -WMAP_PBITOP = |- !f. PBITOP(WMAP f) - -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) - -WMAP_WCAT = |- !w1 w2 f. WMAP f(WCAT(w1,w2)) = WCAT(WMAP f w1,WMAP f w2) - -Theorem MAP_MAP_o autoloading from theory `list` ... -MAP_MAP_o = |- !f g l. MAP f(MAP g l) = MAP(f o g)l - -WMAP_o = |- !w f g. WMAP g(WMAP f w) = WMAP(g o f)w - -FORALLBITS_DEF = |- !P l. FORALLBITS P(WORD l) = ALL_EL P l - -Theorem ELL_CONS autoloading from theory `list` ... -ELL_CONS = |- !n l. n < (LENGTH l) ==> (!x. ELL n(CONS x l) = ELL n l) - -Theorem ELL_LENGTH_CONS autoloading from theory `list` ... -ELL_LENGTH_CONS = |- !l x. ELL(LENGTH l)(CONS x l) = x - -Definition ALL_EL autoloading from theory `list` ... -ALL_EL = -|- (!P. ALL_EL P[] = T) /\ - (!P x l. ALL_EL P(CONS x l) = P x /\ ALL_EL P l) - -Definition LENGTH autoloading from theory `list` ... -LENGTH = |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) - -FORALLBITS = -|- !n. !w :: PWORDLEN n. !P. FORALLBITS P w = (!k. k < n ==> P(BIT k w)) - -Theorem ALL_EL_LASTN autoloading from theory `list` ... -ALL_EL_LASTN = -|- !P l. ALL_EL P l ==> (!m. m <= (LENGTH l) ==> ALL_EL P(LASTN m l)) - -Theorem ALL_EL_SNOC autoloading from theory `list` ... -ALL_EL_SNOC = |- !P x l. ALL_EL P(SNOC x l) = ALL_EL P l /\ P x - -Theorem LENGTH_SNOC autoloading from theory `list` ... -LENGTH_SNOC = |- !x l. LENGTH(SNOC x l) = SUC(LENGTH l) - -Definition BUTLASTN autoloading from theory `list` ... -BUTLASTN = -|- (!l. BUTLASTN 0 l = l) /\ - (!n x l. BUTLASTN(SUC n)(SNOC x l) = BUTLASTN n l) - -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)) - -Theorem ADD_EQ_0 autoloading from theory `arithmetic` ... -ADD_EQ_0 = |- !m n. (m + n = 0) = (m = 0) /\ (n = 0) - -FORALLBITS_WSEG = -|- !n. - !w :: PWORDLEN n. - !P. - FORALLBITS P w ==> - (!m k. (m + k) <= n ==> FORALLBITS P(WSEG m k w)) - -Theorem ALL_EL_APPEND autoloading from theory `list` ... -ALL_EL_APPEND = -|- !P l1 l2. ALL_EL P(APPEND l1 l2) = ALL_EL P l1 /\ ALL_EL P l2 - -FORALLBITS_WCAT = -|- !w1 w2 P. - FORALLBITS P(WCAT(w1,w2)) = FORALLBITS P w1 /\ FORALLBITS P w2 - -EXISTSABIT_DEF = |- !P l. EXISTSABIT P(WORD l) = SOME_EL P l - -Theorem NOT_SOME_EL_ALL_EL autoloading from theory `list` ... -NOT_SOME_EL_ALL_EL = |- !P l. ~SOME_EL P l = ALL_EL($~ o P)l - -NOT_EXISTSABIT = |- !P w. ~EXISTSABIT P w = FORALLBITS($~ o P)w - -Theorem NOT_ALL_EL_SOME_EL autoloading from theory `list` ... -NOT_ALL_EL_SOME_EL = |- !P l. ~ALL_EL P l = SOME_EL($~ o P)l - -NOT_FORALLBITS = |- !P w. ~FORALLBITS P w = EXISTSABIT($~ o P)w - -Definition SOME_EL autoloading from theory `list` ... -SOME_EL = -|- (!P. SOME_EL P[] = F) /\ - (!P x l. SOME_EL P(CONS x l) = P x \/ SOME_EL P l) - -EXISTSABIT_BIT = -|- !n. !w :: PWORDLEN n. !P. EXISTSABIT P w = (?k. k < n /\ P(BIT k w)) - -Theorem SOME_EL_SEG autoloading from theory `list` ... -SOME_EL_SEG = -|- !m k l. - (m + k) <= (LENGTH l) ==> (!P. SOME_EL P(SEG m k l) ==> SOME_EL P l) - -EXISTSABIT_WSEG = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> (!P. EXISTSABIT P(WSEG m k w) ==> EXISTSABIT P w) - -Theorem SOME_EL_APPEND autoloading from theory `list` ... -SOME_EL_APPEND = -|- !P l1 l2. SOME_EL P(APPEND l1 l2) = SOME_EL P l1 \/ SOME_EL P l2 - -EXISTSABIT_WCAT = -|- !w1 w2 P. - EXISTSABIT P(WCAT(w1,w2)) = EXISTSABIT P w1 \/ EXISTSABIT P w2 - -SHR_DEF = -|- !f b w. - SHR f b w = - WCAT - ((f => WSEG 1(PRE(WORDLEN w))w | WORD[b]),WSEG(PRE(WORDLEN w))1 w), - BIT 0 w - -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])) - -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) - -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) - -Theorem PRE_SUB1 autoloading from theory `arithmetic` ... -PRE_SUB1 = |- !m. PRE m = m - 1 - -Theorem WSEG_WORDLEN autoloading from theory `word_base` ... -WSEG_WORDLEN = -|- !n. - !w :: PWORDLEN n. !m k. (m + k) <= n ==> (WORDLEN(WSEG m k w) = m) - -SHR_WSEG = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> - 0 < m ==> - (!f b. - SHR f b(WSEG m k w) = - (f => - WCAT(WSEG 1(k + (m - 1))w,WSEG(m - 1)(k + 1)w) | - WCAT(WORD[b],WSEG(m - 1)(k + 1)w)),BIT k w) - -SHR_WSEG_1F = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> - 0 < m ==> - (!b. - SHR F b(WSEG m k w) = WCAT(WORD[b],WSEG(m - 1)(k + 1)w),BIT k w) - -SHR_WSEG_NF_lem1 = |- 0 < m ==> ((m - 1) + 1 = m) - -SHR_WSEG_NF_lem2 = |- 0 < m ==> ((m - 1) + (k + 1) = m + k) - -Theorem LESS_OR autoloading from theory `arithmetic` ... -LESS_OR = |- !m n. m < n ==> (SUC m) <= n - -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) - -Theorem LESS_IMP_LESS_OR_EQ autoloading from theory `arithmetic` ... -LESS_IMP_LESS_OR_EQ = |- !m n. m < n ==> m <= n - -SHR_WSEG_NF = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) < n ==> - 0 < m ==> - (SHR F(BIT(m + k)w)(WSEG m k w) = WSEG m(k + 1)w,BIT k w) - -SHL_WSEG = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> - 0 < m ==> - (!f b. - SHL f(WSEG m k w)b = - BIT(k + (m - 1))w, - (f => - WCAT(WSEG(m - 1)k w,WSEG 1 k w) | - WCAT(WSEG(m - 1)k w,WORD[b]))) - -SHL_WSEG_1F = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> - 0 < m ==> - (!b. - SHL F(WSEG m k w)b = - BIT(k + (m - 1))w,WCAT(WSEG(m - 1)k w,WORD[b])) - -SHL_WSEG_NF = -|- !n. - !w :: PWORDLEN n. - !m k. - (m + k) <= n ==> - 0 < m ==> - 0 < k ==> - (SHL F(WSEG m k w)(BIT(k - 1)w) = - BIT(k + (m - 1))w,WSEG m(k - 1)w) - -Theorem PWORDLEN1 autoloading from theory `word_base` ... -PWORDLEN1 = |- !x. PWORDLEN 1(WORD[x]) - -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 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 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 PWORDLEN autoloading from theory `word_base` ... -PWORDLEN = |- !n w. PWORDLEN n w = (WORDLEN w = n) - -WSEG_SHL = -|- !n. - !w :: PWORDLEN(SUC n). - !m k. - 0 < k /\ (m + k) <= (SUC n) ==> - (!b. WSEG m k(SND(SHL f w b)) = WSEG m(k - 1)w) - -Theorem WSEG_WORD_LENGTH autoloading from theory `word_base` ... -WSEG_WORD_LENGTH = |- !n. !w :: PWORDLEN n. WSEG n 0 w = w - -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)) - -WSEG_SHL_0 = -|- !n. - !w :: PWORDLEN(SUC n). - !m b. - 0 < m /\ m <= (SUC n) ==> - (WSEG m 0(SND(SHL f w b)) = - WCAT(WSEG(m - 1)0 w,(f => WSEG 1 0 w | WORD[b]))) - -() : void - - -File mk_word_bitop loaded -() : void - -#rm -f word_num.th -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadt `mk_word_num`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 -=============================================================================== - -#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 - -Theory word_base loaded -() : void - -[()] : void list - -() : void - -...() : void - -LVAL_DEF = |- !f b l. LVAL f b l = FOLDL(\e x. (b * e) + (f x))0 l - -Theorem LEFT_ADD_DISTRIB autoloading from theory `arithmetic` ... -LEFT_ADD_DISTRIB = |- !m n p. p * (m + n) = (p * m) + (p * n) - -Theorem ADD_ASSOC autoloading from theory `arithmetic` ... -ADD_ASSOC = |- !m n p. m + (n + p) = (m + n) + p - -Theorem MULT_SYM autoloading from theory `arithmetic` ... -MULT_SYM = |- !m n. m * n = n * m - -Theorem MULT_ASSOC autoloading from theory `arithmetic` ... -MULT_ASSOC = |- !m n p. m * (n * p) = (m * n) * p - -Theorem LENGTH_SNOC autoloading from theory `list` ... -LENGTH_SNOC = |- !x l. LENGTH(SNOC x l) = SUC(LENGTH l) - -Theorem FOLDL_SNOC autoloading from theory `list` ... -FOLDL_SNOC = |- !f e x l. FOLDL f e(SNOC x l) = f(FOLDL f e l)x - -Definition EXP autoloading from theory `arithmetic` ... -EXP = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n)) - -Definition LENGTH autoloading from theory `list` ... -LENGTH = |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) - -Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... -ADD_CLAUSES = -|- (0 + m = m) /\ - (m + 0 = m) /\ - ((SUC m) + n = SUC(m + n)) /\ - (m + (SUC n) = SUC(m + n)) - -Theorem MULT_CLAUSES autoloading from theory `arithmetic` ... -MULT_CLAUSES = -|- !m n. - (0 * m = 0) /\ - (m * 0 = 0) /\ - (1 * m = m) /\ - (m * 1 = m) /\ - ((SUC m) * n = (m * n) + n) /\ - (m * (SUC n) = m + (m * n)) - -Definition FOLDL autoloading from theory `list` ... -FOLDL = -|- (!f e. FOLDL f e[] = e) /\ - (!f e x l. FOLDL f e(CONS x l) = FOLDL f(f e x)l) - -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_Ax autoloading from theory `word_base` ... -word_Ax = |- !f. ?! fn. !l. fn(WORD l) = f l - -NVAL_DEF = |- !f b l. NVAL f b(WORD l) = LVAL f b l - -Theorem RIGHT_ADD_DISTRIB autoloading from theory `arithmetic` ... -RIGHT_ADD_DISTRIB = |- !m n p. (m + n) * p = (m * p) + (n * p) - -Definition MULT autoloading from theory `arithmetic` ... -MULT = |- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n) - -Definition SNOC autoloading from theory `list` ... -SNOC = -|- (!x. SNOC x[] = [x]) /\ - (!x x' l. SNOC x(CONS x' l) = CONS x'(SNOC x l)) - -LVAL_SNOC = |- !l h f b. LVAL f b(SNOC h l) = ((LVAL f b l) * b) + (f h) - -Definition LESS_OR_EQ autoloading from theory `arithmetic` ... -LESS_OR_EQ = |- !m n. m <= n = m < n \/ (m = n) - -Theorem LESS_THM autoloading from theory `prim_rec` ... -LESS_THM = |- !m n. m < (SUC n) = (m = n) \/ m < n - -LESS_SUC_IMP_LESS_EQ = |- !m n. m < (SUC n) = m <= n - -Theorem LESS_LESS_EQ_TRANS autoloading from theory `arithmetic` ... -LESS_LESS_EQ_TRANS = |- !m n p. m < n /\ n <= p ==> m < p - -Theorem LESS_MONO_ADD autoloading from theory `arithmetic` ... -LESS_MONO_ADD = |- !m n p. m < n ==> (m + p) < (n + p) - -Theorem ADD_SYM autoloading from theory `arithmetic` ... -ADD_SYM = |- !m n. m + n = n + m - -LVAL_MAX_lem = |- !a b c y. (a + b) < (SUC c) /\ y < b ==> (a + y) < c - -Theorem LESS_OR autoloading from theory `arithmetic` ... -LESS_OR = |- !m n. m < n ==> (SUC m) <= n - -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) - -Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... -LESS_EQ_REFL = |- !m. m <= m - -Theorem INDUCTION autoloading from theory `num` ... -INDUCTION = |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> (!n. P n) - -LESS_MULT_PLUS_DIFF = |- !n k l. k < l ==> ((k * n) + n) <= (l * n) - -Theorem LESS_EQ_IMP_LESS_SUC autoloading from theory `arithmetic` ... -LESS_EQ_IMP_LESS_SUC = |- !n m. n <= m ==> n < (SUC m) - -Theorem LESS_0 autoloading from theory `prim_rec` ... -LESS_0 = |- !n. 0 < (SUC n) - -LVAL_MAX = -|- !l f b. (!x. (f x) < b) ==> (LVAL f b l) < (b EXP (LENGTH l)) - -NVAL_MAX = -|- !f b. - (!x. (f x) < b) ==> (!n. !w :: PWORDLEN n. (NVAL f b w) < (b EXP n)) - -NVAL0 = |- !f b. NVAL f b(WORD[]) = 0 - -NVAL1 = |- !f b x. NVAL f b(WORD[x]) = f x - -Theorem PWORDLEN0 autoloading from theory `word_base` ... -PWORDLEN0 = |- !w. PWORDLEN 0 w ==> (w = WORD[]) - -NVAL_WORDLEN_0 = |- !w :: PWORDLEN 0. !fv r. NVAL fv r w = 0 - -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) - -NVAL_WCAT1 = -|- !w f b x. NVAL f b(WCAT(w,WORD[x])) = ((NVAL f b w) * b) + (f x) - -Theorem CONS_APPEND autoloading from theory `list` ... -CONS_APPEND = |- !x l. CONS x l = APPEND[x]l - -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) - -Theorem EXP_ADD autoloading from theory `arithmetic` ... -EXP_ADD = |- !p q n. n EXP (p + q) = (n EXP p) * (n EXP q) - -Theorem EQ_MONO_ADD_EQ autoloading from theory `arithmetic` ... -EQ_MONO_ADD_EQ = |- !m n p. (m + p = n + p) = (m = n) - -Theorem WCAT_PWORDLEN autoloading from theory `word_base` ... -WCAT_PWORDLEN = -|- !n1. - !w1 :: PWORDLEN n1. - !n2. !w2 :: PWORDLEN n2. PWORDLEN(n1 + n2)(WCAT(w1,w2)) - -Theorem WCAT_ASSOC autoloading from theory `word_base` ... -WCAT_ASSOC = |- !w1 w2 w3. WCAT(w1,WCAT(w2,w3)) = WCAT(WCAT(w1,w2),w3) - -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) - -Definition ADD autoloading from theory `arithmetic` ... -ADD = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n)) - -Theorem WCAT0 autoloading from theory `word_base` ... -WCAT0 = |- !w. (WCAT(WORD[],w) = w) /\ (WCAT(w,WORD[]) = w) - -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 LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... -LESS_EQ_SUC_REFL = |- !m. m <= (SUC m) - -Theorem ADD_0 autoloading from theory `arithmetic` ... -ADD_0 = |- !m. m + 0 = m - -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) - -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))) - -NWORD_DEF = |- !n frep b m. NWORD n frep b m = WORD(NLIST n frep b m) - -NLIST_LENGTH = |- !n f b m. LENGTH(NLIST n f b m) = n - -Definition WORDLEN_DEF autoloading from theory `word_base` ... -WORDLEN_DEF = |- !l. WORDLEN(WORD l) = LENGTH l - -NWORD_LENGTH = |- !n f b m. WORDLEN(NWORD n f b m) = n - -Definition PWORDLEN_DEF autoloading from theory `word_base` ... -PWORDLEN_DEF = |- !n l. PWORDLEN n(WORD l) = (n = LENGTH l) - -NWORD_PWORDLEN = |- !n f b m. PWORDLEN n(NWORD n f b m) - -() : void - - -File mk_word_num loaded -() : void - -#rm -f bword_bitop.th -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadt `mk_bword_bitop`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 -=============================================================================== - -#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 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 6/5/24 -=============================================================================== - -#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 6/5/24 -=============================================================================== - -#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) - -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 6/5/24 -=============================================================================== - -#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 6/5/24 -=============================================================================== - -#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 +Error: ERROR "Caught fatal error [memory may be damaged]" +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%8638%55. +ERROR "Caught fatal error [memory may be damaged]" + +Broken at FUN%8638%55. 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%8638%55. + +UNBOUND-VARIABLE :NAME QUIT + +Broken at FUN%8638%55. + 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%8638%55. + +ERROR "Caught fatal error [memory may be damaged]" + +Broken at FUN%8638%55. + 1 (abort) Return to debug level 2. + 2 Return to debug level 1. + 3 Return to top level. +>>>>make[4]: *** [Makefile:69: word_base.th] Error 255 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);;'\ @@ -29545,7 +27437,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -29744,7 +27636,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -29776,7 +27668,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -29910,7 +27802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30213,7 +28105,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30245,7 +28137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30284,7 +28176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30316,7 +28208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30477,7 +28369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30610,7 +28502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30799,7 +28691,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30859,7 +28751,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -30984,7 +28876,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -31095,7 +28987,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -31120,7 +29012,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -31148,7 +29040,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -31261,7 +29153,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -31764,7 +29656,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32012,7 +29904,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32238,7 +30130,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32280,7 +30172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32312,7 +30204,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32535,7 +30427,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -32928,7 +30820,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -33041,7 +30933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -33544,7 +31436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -33792,7 +31684,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34018,7 +31910,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34053,7 +31945,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34092,7 +31984,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34129,7 +32021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34150,7 +32042,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34247,7 +32139,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34269,7 +32161,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34765,7 +32657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34788,7 +32680,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34866,7 +32758,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34925,7 +32817,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34969,7 +32861,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -34987,7 +32879,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35014,7 +32906,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35058,7 +32950,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35171,7 +33063,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35218,7 +33110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35257,7 +33149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35331,7 +33223,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35420,7 +33312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35491,7 +33383,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35561,7 +33453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35610,7 +33502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35651,7 +33543,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35692,7 +33584,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35716,7 +33608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35817,7 +33709,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35838,7 +33730,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -35863,7 +33755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36489,7 +34381,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36566,7 +34458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36593,7 +34485,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36710,7 +34602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36805,7 +34697,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -36891,7 +34783,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37006,7 +34898,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37099,7 +34991,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37275,7 +35167,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37379,7 +35271,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37674,7 +35566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37777,7 +35669,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37845,7 +35737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -37907,7 +35799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -38087,7 +35979,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -38128,7 +36020,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -38158,7 +36050,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -38184,7 +36076,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -38702,7 +36594,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -39239,7 +37131,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -39427,7 +37319,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #false : bool @@ -39445,10 +37337,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Mon May 6 02:27:42 -12 2024 +Tue May 7 05:10:07 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Mon May 6 02:27:42 -12 2024 +Tue May 7 05:10:07 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39468,20 +37360,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/5/24 + HOL88 Version 2.02 (GCL), built on 7/5/24 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 6/5/24 +BASIC-HOL version 2.02 (GCL) created 7/5/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 6/5/24 +HOL-LCF version 2.02 (GCL) created 7/5/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41219,7 +39111,7 @@ make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -42984,7 +40876,7 @@ make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -44727,7 +42619,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' @@ -44981,7 +42873,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' @@ -45217,7 +43109,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' @@ -45394,7 +43286,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' @@ -45582,7 +43474,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' @@ -45700,7 +43592,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' @@ -45815,7 +43707,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' @@ -46054,7 +43946,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' @@ -46394,7 +44286,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' @@ -46600,7 +44492,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' @@ -46942,7 +44834,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' @@ -47133,7 +45025,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' @@ -47400,7 +45292,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' @@ -47560,7 +45452,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' @@ -47704,7 +45596,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' @@ -47855,7 +45747,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' @@ -48010,7 +45902,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' @@ -48187,7 +46079,7 @@ \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' @@ -48382,7 +46274,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' @@ -48606,7 +46498,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex - makeindex is not built for aarch64. + makeindex is not built for armv7l. make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' @@ -48866,7 +46758,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.05.06:0235' -> endpages.ps +' TeX output 2024.05.07:0513' -> endpages.ps @@ -48930,7 +46822,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.05.06:0235' -> titlepages.ps +' TeX output 2024.05.07:0513' -> titlepages.ps @@ -49009,8 +46901,8 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_armhf.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_armhf.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_armhf.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install find ml -type f -name "*ml" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install @@ -49057,10 +46949,12 @@ dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_strip: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_compress: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_fixperms dh_makeshlibs dh_installdeb @@ -49069,16 +46963,17 @@ dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) +dh_shlibdeps: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_gencontrol dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_armhf.buildinfo @@ -49088,12 +46983,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/25046/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/25046/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/15490 and its subdirectories -I: Current time: Mon May 6 02:39:05 -12 2024 -I: pbuilder-time-stamp: 1715006345 +I: removing directory /srv/workspace/pbuilder/25046 and its subdirectories +I: Current time: Tue May 7 05:15:27 +14 2024 +I: pbuilder-time-stamp: 1715008527