Diff of the two buildlogs: -- --- b1/build.log 2024-11-06 02:12:04.513622340 +0000 +++ b2/build.log 2024-11-06 03:12:41.552280256 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Nov 5 13:26:22 -12 2024 -I: pbuilder-time-stamp: 1730856382 +I: Current time: Wed Nov 6 16:13:37 +14 2024 +I: pbuilder-time-stamp: 1730859217 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/17935/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/19671/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 Nov 6 02:14 /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/19671/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/19671/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]="32" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.32(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='1683214688024e47bc8f227d79215cae' - 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='17935' - PS1='# ' - PS2='> ' + INVOCATION_ID=31928e7007b742998ad4049082a2380f + 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=19671 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.qTt4TwJz/pbuilderrc_hUBs --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.qTt4TwJz/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.qTt4TwJz/pbuilderrc_glqD --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.qTt4TwJz/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-26-arm64 #1 SMP Debian 6.1.112-1 (2024-09-30) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-26-armmp-lpae #1 SMP Debian 6.1.112-1 (2024-09-30) armv7l GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Aug 4 21:30 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/17935/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/19671/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -304,7 +336,7 @@ Get: 189 http://deb.debian.org/debian unstable/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 190 http://deb.debian.org/debian unstable/main armhf texlive-base all 2024.20241102-1 [22.7 MB] Get: 191 http://deb.debian.org/debian unstable/main armhf texlive-latex-base all 2024.20241102-1 [1278 kB] -Fetched 172 MB in 7s (24.6 MB/s) +Fetched 172 MB in 26s (6726 kB/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 ... 19688 files and directories currently installed.) @@ -944,8 +976,8 @@ Setting up tzdata (2024b-3) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Nov 6 01:28:59 UTC 2024. -Universal Time is now: Wed Nov 6 01:28:59 UTC 2024. +Local time is now: Wed Nov 6 02:20:06 UTC 2024. +Universal Time is now: Wed Nov 6 02:20:06 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.12-1) ... @@ -1144,7 +1176,11 @@ fakeroot is already the newest version (1.36-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/19671/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/19671/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 @@ -1398,52 +1434,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' @@ -1453,43 +1468,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 \ @@ -1499,7 +1535,6 @@ -X./contrib/Xhelp/xholhelp.h.orig -X./contrib/Xhelp/hol_thm.orig dh_clean: warning: Compatibility levels before 10 are deprecated (level 9 in use) for i in $(find Library -name "*.sve") ; do mv $i $(echo $i | sed "s,\.sve,,1"); done -libfakeroot internal error: payload not recognized! rm -f debian/hol88.install debian/hol88-library.install debian/hol88-source.install debian/hol88-help.install debian/hol88-library-source.install debian/hol88-library-help.install debian/hol88-contrib-source.install debian/hol88-contrib-help.install debian/hol88-doc.install debian/hol88.links debian/hol88-library.links debian/hol88.sh find -name "*.dvi" -exec rm {} \; rm -f Manual/Tutorial/ack.tex Manual/Reference/ack.tex Manual/Description/ack.tex @@ -1538,7 +1573,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Nov 5 13:40:23 -12 2024 +Wed Nov 6 16:31:26 +14 2024 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2776,7 +2811,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 # mem = - : (* -> * list -> bool) @@ -2914,7 +2949,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #.............start address -T 0x88a938 () : void @@ -3073,7 +3108,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #.............start address -T 0x88a938 () : void @@ -3265,7 +3300,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 # concat = - : (string -> string -> string) @@ -3375,7 +3410,7 @@ start address -T 0x887950 ;; Finished loading "lisp/f-ol-net" start address -T 0x6c49c0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 5/11/24 + version 2.02 (GCL) created 6/11/24 #...start address -T 0x730bb0 () : void @@ -3704,7 +3739,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 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 ###########################() : void @@ -3717,7 +3752,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 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 ################################################################################################() : void @@ -3862,7 +3897,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 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 ############################() : void @@ -3905,7 +3940,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 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 ############################Theory ind loaded () : void @@ -3942,7 +3977,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3983,7 +4018,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4385,7 +4420,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4453,7 +4488,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4658,7 +4693,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4782,7 +4817,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4868,7 +4903,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -4961,7 +4996,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5030,7 +5065,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5135,7 +5170,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5370,7 +5405,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5396,7 +5431,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5524,7 +5559,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5572,7 +5607,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5639,7 +5674,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5698,7 +5733,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5754,7 +5789,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 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5767,7 +5802,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #() : void @@ -5819,7 +5854,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ##########################() : void @@ -5850,7 +5885,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ##############################() : void @@ -5937,7 +5972,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #######################################################################() : void @@ -6090,7 +6125,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ###########################() : void @@ -6125,7 +6160,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #############################() : void @@ -6186,7 +6221,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ###########################Theory arithmetic loaded () : void @@ -6681,7 +6716,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ##################################() : void @@ -6828,7 +6863,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #################################Theory list loaded () : void @@ -7167,7 +7202,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ###############################Theory list loaded () : void @@ -8664,7 +8699,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #############################() : void @@ -9048,7 +9083,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ############################() : void @@ -9346,7 +9381,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ############################() : void @@ -9486,7 +9521,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ############################################() : void @@ -9583,7 +9618,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 ##################################() : void @@ -9613,7 +9648,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -9630,7 +9665,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #Theory num loaded () : void @@ -9649,7 +9684,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -9806,7 +9841,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 # @@ -9844,7 +9879,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 # @@ -9878,7 +9913,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -9963,7 +9998,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -10004,7 +10039,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -10188,7 +10223,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 # define_load_lib_function = - : (string list -> void -> void) @@ -10264,7 +10299,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 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10277,7 +10312,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #() : void @@ -10341,11 +10376,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Nov 5 13:52:15 -12 2024 +Wed Nov 6 16:43:16 +14 2024 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Nov 5 13:52:16 -12 2024 +Wed Nov 6 16:43:16 +14 2024 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10368,7 +10403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -10452,7 +10487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -10558,7 +10593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11308,7 +11343,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11331,7 +11366,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11374,7 +11409,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11410,7 +11445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11462,7 +11497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11494,7 +11529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11532,7 +11567,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11560,7 +11595,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11637,7 +11672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11659,7 +11694,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11713,7 +11748,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11762,7 +11797,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11913,7 +11948,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -11957,7 +11992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12032,7 +12067,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12082,7 +12117,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12145,7 +12180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12198,7 +12233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12244,7 +12279,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12332,7 +12367,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12370,7 +12405,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12431,7 +12466,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12495,7 +12530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12521,7 +12556,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12546,7 +12581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12585,7 +12620,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -12661,7 +12696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -13398,7 +13433,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -13421,7 +13456,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -13464,7 +13499,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -13499,7 +13534,48 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 +=============================================================================== + +#false : bool + + +() : void + +ascii_Axiom = +|- !f. + ?! fn. + !b0 b1 b2 b3 b4 b5 b6 b7. + fn(ASCII b0 b1 b2 b3 b4 b5 b6 b7) = f b0 b1 b2 b3 b4 b5 b6 b7 + +ascii_Induct = +|- !P. + (!b0 b1 b2 b3 b4 b5 b6 b7. P(ASCII b0 b1 b2 b3 b4 b5 b6 b7)) ==> + (!a. P a) + +ascii_CASES = +|- !a. ?b0 b1 b2 b3 b4 b5 b6 b7. a = ASCII b0 b1 b2 b3 b4 b5 b6 b7 + +ASCII_11 = +|- !b0 b1 b2 b3 b4 b5 b6 b7 b0' b1' b2' b3' b4' b5' b6' b7'. + (ASCII b0 b1 b2 b3 b4 b5 b6 b7 = + ASCII b0' b1' b2' b3' b4' b5' b6' b7') = + (b0 = b0') /\ + (b1 = b1') /\ + (b2 = b2') /\ + (b3 = b3') /\ + (b4 = b4') /\ + (b5 = b5') /\ + (b6 = b6') /\ + (b7 = b7') + +rm -f string.th +echo 'set_flag(`abort_when_fail`,true);;'\ + 'loadt `mk_string`;;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -13507,9 +13583,164 @@ () : void -evaluation failed EVERY_CONV -evaluation failed load -- mk_ascii -make[4]: *** [Makefile:42: ascii.th] Error 1 +Theory ascii loaded +() : void + +() : void + +() : void + +() : void + +() : void + +string_Axiom = `string_Axiom` : string + +spec = `string = `` | STRING ascii string` : string + +tok = `tok` : string + +string_Induct = `string_Induct` : string + +string_CASES = `string_CASES` : string + +STRING_11 = `STRING_11` : string + +NOT_STRING_EMPTY = `NOT_STRING_EMPTY` : string + +NOT_EMPTY_STRING = `NOT_EMPTY_STRING` : string + +() : void + +string_Axiom = +|- !e f. ?! fn. (fn `` = e) /\ (!a s. fn(STRING a s) = f(fn s)a s) + +() : void + +string_Induct = +|- !P. P `` /\ (!s. P s ==> (!a. P(STRING a s))) ==> (!s. P s) + +string_CASES = |- !s. (s = ``) \/ (?s' a. s = STRING a s') + +STRING_11 = +|- !a s a' s'. (STRING a s = STRING a' s') = (a = a') /\ (s = s') + +NOT_STRING_EMPTY = |- !a s. ~(`` = STRING a s) + +NOT_EMPTY_STRING = |- !a s. ~(STRING a s = ``) + +() : void + +echo 'set_flag(`abort_when_fail`,true);;'\ + 'load_theory `ascii`;;'\ + 'compilet `ascii`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/11/24 +=============================================================================== + +#false : bool + +Theory ascii loaded +() : void + + +ascii_EQ_CONV = - : conv + +Calling Lisp compiler + +File ascii compiled +() : void + +#echo 'set_flag(`abort_when_fail`,true);;'\ + 'load_theory `string`;;'\ + 'compilet `stringconv`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/11/24 +=============================================================================== + +#false : bool + +Theory string loaded +() : void + + +string_CONV = - : conv + +Calling Lisp compiler + +File stringconv compiled +() : void + +#echo 'set_flag(`abort_when_fail`,true);;'\ + 'load_theory `string`;;'\ + 'loadf `stringconv`;;'\ + 'loadf `ascii`;;'\ + 'compilet `string_rules`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/11/24 +=============================================================================== + +#false : bool + +Theory string loaded +() : void + +.() : void + +.() : void + + +string_EQ_CONV = - : conv + +Calling Lisp compiler + +File string_rules compiled +() : void + +#echo 'set_flag(`abort_when_fail`,true);;'\ + 'load_theory `string`;;'\ + 'compilet `string`;;'\ + 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol + + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/11/24 +=============================================================================== + +#false : bool + +Theory string loaded +() : void + + +Updating search path +() : void + +Updating help search path +() : void + +Theory string loaded +() : void + +() : void + +() : void + +Calling Lisp compiler + +File string compiled +() : void + +#===> library string rebuilt make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets' rm -f finite_sets.th @@ -13518,7 +13749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14050,7 +14281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14073,7 +14304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14107,7 +14338,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14162,7 +14393,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14253,7 +14484,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14422,7 +14653,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14630,7 +14861,7 @@ |- !l. woset l ==> (!x y. fl l x /\ fl l y ==> (x = y) \/ less l(x,y) \/ less l(y,x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 172 WO_INDUCT = @@ -14655,7 +14886,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 = @@ -14675,7 +14906,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (?f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 444 WO_RECURSE = @@ -14685,7 +14916,7 @@ (!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` ... @@ -14709,7 +14940,7 @@ Run time: 0.0s WOSET_NUM = |- woset(\(m,n). m <= n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 Theorem LESS_NOT_EQ autoloading from theory `prim_rec` ... @@ -14737,7 +14968,7 @@ Intermediate theorems generated: 232 INSEG_SUBSET = |- !l m. m inseg l ==> (!x y. m(x,y) ==> l(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) @@ -14745,7 +14976,7 @@ Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -14762,7 +14993,7 @@ INSEG_PROPER_SUBSET = |- !l m. m inseg l /\ ~(l = m) ==> (?x y. l(x,y) /\ ~m(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 213 INSEG_PROPER_SUBSET_FL = @@ -14774,12 +15005,12 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1172 EXTEND_FL = |- !l x. woset l ==> (fl(\(x,y). l(x,y) /\ l(y,a))x = l(x,a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 143 EXTEND_INSEG = @@ -14797,14 +15028,14 @@ ORDINAL_CHAINED = |- !l m. ordinal l /\ ordinal m ==> m inseg l \/ l inseg m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 997 FL_SUC = |- !l a. fl(\(x,y). l(x,y) \/ (y = a) /\ (fl l x \/ (x = a)))x = fl l x \/ (x = a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -14813,7 +15044,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -14885,7 +15116,7 @@ File mk_wellorder loaded () : void -Run time: 1.0s +Run time: 1.5s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -14894,7 +15125,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14929,13 +15160,103 @@ Run time: 0.0s Intermediate theorems generated: 1 -evaluation failed EVERY_CONV -evaluation failed load -- ../../Library/abs_theory/monoid_def.ml +MONOID = |- !f. ?! fn. !f' x. fn(monoid f' x) = f f' x +Run time: 0.0s +Intermediate theorems generated: 431 + +() : void +Run time: 0.0s +Intermediate theorems generated: 2 + +"!f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m)" + 3 ["!x y z. op m x(op m y z) = op m(op m x y)z" ] + 2 ["!x. op m(e m)x = x" ] + 1 ["!x. op m x(e m) = x" ] + +() : void +Run time: 0.0s +Intermediate theorems generated: 1 + +OK.. +"f = e m" + 4 ["!x y z. op m x(op m y z) = op m(op m x y)z" ] + 3 ["!x. op m(e m)x = x" ] + 2 ["!x. op m x(e m) = x" ] + 1 ["!a. (op m a f = a) /\ (op m f a = a)" ] + +() : void +Run time: 0.0s +Intermediate theorems generated: 6 + +OK.. +"f = e m" + 5 ["!x y z. op m x(op m y z) = op m(op m x y)z" ] + 4 ["!x. op m(e m)x = x" ] + 3 ["!x. op m x(e m) = x" ] + 2 ["!a. (op m a f = a) /\ (op m f a = a)" ] + 1 ["e m = op m(e m)f" ] + +() : void +Run time: 0.0s +Intermediate theorems generated: 10 + +OK.. +"f = op m(e m)f" + 5 ["!x y z. op m x(op m y z) = op m(op m x y)z" ] + 4 ["!x. op m(e m)x = x" ] + 3 ["!x. op m x(e m) = x" ] + 2 ["!a. (op m a f = a) /\ (op m f a = a)" ] + 1 ["e m = op m(e m)f" ] + +() : void +Run time: 0.0s +Intermediate theorems generated: 4 + +OK.. +goal proved +. |- f = op m(e m)f +.. |- f = e m +.. |- f = e m +. |- !f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m) + +Previous subproof: +goal proved +() : void +Run time: 0.0s +Intermediate theorems generated: 43 + +IDENTITY_UNIQUE = +. |- !f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m) +Run time: 0.0s +Intermediate theorems generated: 36 + +. |- !f. (!a. (op m a f = a) /\ (op m f a = a)) ==> (f = e m) +Run time: 0.0s +Intermediate theorems generated: 2 + +OP_DETERMINES_IDENTITY = .. |- (op m1 = op m2) ==> (e m1 = e m2) +Run time: 0.0s +Intermediate theorems generated: 73 + +.. |- (op m1 = op m2) ==> (e m1 = e m2) +Run time: 0.0s +Intermediate theorems generated: 4 + +() : void +Run time: 0.0s +Intermediate theorems generated: 1 + + +File ../../Library/abs_theory/monoid_def.ml loaded +() : void +Run time: 0.1s +Intermediate theorems generated: 614 + Making ../../Library/abs_theory/group_def.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -14970,42 +15291,64 @@ Run time: 0.0s Intermediate theorems generated: 1 +Theory monoid_def loaded +() : void +Run time: 0.0s +Intermediate theorems generated: 6 -Error: FILE-ERROR :PATHNAME "monoid_def.th" "Cannot open" -Fast links are on: do (si::use-fast-links nil) for debugging -Signalled by FUNCALL. -FILE-ERROR :PATHNAME "monoid_def.th" "Cannot open" +GROUP = |- !f. ?! fn. !f0 x f1. fn(group f0 x f1) = f f0 x f1 +Run time: 0.1s +Intermediate theorems generated: 601 -Broken at FUNCALL. 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 FUNCALL. +() : void +Run time: 0.0s +Intermediate theorems generated: 2 -UNBOUND-VARIABLE :NAME QUIT +GROUP_EXTENDS_MONOID = ... |- IS_MONOID(monoid(fn g)(id g)) +Run time: 0.0s +Intermediate theorems generated: 144 -Broken at FUNCALL. - 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 FUNCALL. +IDENTITY_UNIQUE = +... |- !f. (!a. (fn g a f = a) /\ (fn g f a = a)) ==> (f = id g) +Run time: 0.0s +Intermediate theorems generated: 144 -ERROR "Caught fatal error [memory may be damaged]" +":(*)group" : type +Run time: 0.0s +Intermediate theorems generated: 3 + +... |- !f. (!a. (fn g a f = a) /\ (fn g f a = a)) ==> (f = id g) +Run time: 0.0s +Intermediate theorems generated: 6 -Broken at FUNCALL. - 1 (abort) Return to debug level 2. - 2 Return to debug level 1. - 3 Return to top level. ->>>>Making ../../Library/abs_theory/example.th... +LEFT_CANCELLATION = ... |- !x y a. (fn g a x = fn g a y) ==> (x = y) +Run time: 0.0s +Intermediate theorems generated: 67 + +INVERSE_INVERSE_LEMMA = |- !g. IS_GROUP g ==> (!a. inv g(inv g a) = a) +Run time: 0.0s +Intermediate theorems generated: 45 + +ALTERNATE_INVERSE_INVERSE_LEMMA = +|- !g. IS_GROUP g ==> (!a. inv g(inv g a) = a) +Run time: 0.1s +Intermediate theorems generated: 69 + +() : void +Run time: 0.0s +Intermediate theorems generated: 1 + + +File ../../Library/abs_theory/group_def.ml loaded +() : void +Run time: 0.2s +Intermediate theorems generated: 1089 + +Making ../../Library/abs_theory/example.th... =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -15045,43 +15388,64 @@ Run time: 0.0s Intermediate theorems generated: 153 +Theory group_def loaded +() : void +Run time: 0.1s +Intermediate theorems generated: 7 + +Theorem I_THM autoloading from theory `combin` ... +I_THM = |- !x. I x = x +Run time: 0.0s + +GROUP_THOBS = |- IS_GROUP(group(\x y. ~(x = y))F I) +Run time: 0.0s +Intermediate theorems generated: 378 + +|- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f +Run time: 0.0s +Intermediate theorems generated: 733 + +|- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) +Run time: 0.1s +Intermediate theorems generated: 732 + +|- !a. I(I a) = a +Run time: 0.0s +Intermediate theorems generated: 1106 + +concrete_rep = "group(\x y. x = y)T I" : term +Run time: 0.0s + +GROUP_THOBS = |- IS_GROUP(group(\x y. x = y)T I) +Run time: 0.0s +Intermediate theorems generated: 356 + +inst_func = - : (string -> thm) +Run time: 0.0s + +[|- !f. (!a. ((a = f) = a) /\ ((f = a) = a)) ==> f; + |- !x y a. ((a = x) = (a = y)) ==> (x = y); + |- !a. I(I a) = a] +: thm list +Run time: 0.2s +Intermediate theorems generated: 2546 + +() : void +Run time: 0.0s +Intermediate theorems generated: 1 + + +File ../../Library/abs_theory/example.ml loaded +() : void +Run time: 0.4s +Intermediate theorems generated: 6013 -Error: FILE-ERROR :PATHNAME "group_def.th" "Cannot open" -Fast links are on: do (si::use-fast-links nil) for debugging -Signalled by FUNCALL. -FILE-ERROR :PATHNAME "group_def.th" "Cannot open" - -Broken at FUNCALL. 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 FUNCALL. - -UNBOUND-VARIABLE :NAME QUIT - -Broken at FUNCALL. - 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 FUNCALL. - -ERROR "Caught fatal error [memory may be damaged]" - -Broken at FUNCALL. - 1 (abort) Return to debug level 2. - 2 Return to debug level 1. - 3 Return to top level. ->>>>===> abs_theory rebuilt on Tue Nov 5 13:56:48 -12 2024 +===> abs_theory rebuilt on Wed Nov 6 16:47:59 +14 2024 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -15254,7 +15618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -15476,7 +15840,7 @@ TRAT_MUL_WELLDEFINED = |- !p q r. p trat_eq q ==> (p trat_mul r) trat_eq (q trat_mul r) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 207 TRAT_MUL_WELLDEFINED2 = @@ -15518,7 +15882,7 @@ |- !h i j. (h trat_mul (i trat_add j)) trat_eq ((h trat_mul i) trat_add (h trat_mul j)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h @@ -15590,7 +15954,7 @@ Run time: 0.0s TRAT_ARCH = |- !h. ?n d. (trat_sucint n) trat_eq (h trat_add d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 TRAT_SUCINT = @@ -15600,7 +15964,7 @@ Intermediate theorems generated: 37 TRAT_EQ_EQUIV = |- !p q. p trat_eq q = ($trat_eq p = $trat_eq q) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -15621,7 +15985,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -15681,7 +16045,7 @@ File hrat.ml loaded () : void -Run time: 0.5s +Run time: 0.6s Intermediate theorems generated: 11032 #\ @@ -15691,7 +16055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -15934,7 +16298,7 @@ Intermediate theorems generated: 85 HRAT_UP = |- !x. ?y. x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 HRAT_DOWN = |- !x. ?y. y hrat_lt x @@ -15942,7 +16306,7 @@ Intermediate theorems generated: 45 HRAT_DOWN2 = |- !x y. ?z. z hrat_lt x /\ z hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 154 HRAT_MEAN = |- !x y. x hrat_lt y ==> (?z. x hrat_lt z /\ z hrat_lt y) @@ -16028,11 +16392,11 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.0s +Run time: 0.1s Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.1s +Run time: 0.0s Theorem HRAT_ARCH autoloading from theory `HRAT` ... HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16079,7 +16443,7 @@ Intermediate theorems generated: 2 hreal_lt = |- !X Y. X hreal_lt Y = ~(X = Y) /\ (!x. cut X x ==> cut Y x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 HREAL_INV_ISACUT = @@ -16115,7 +16479,7 @@ HREAL_MUL_ASSOC = |- !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 490 HREAL_LDISTRIB = @@ -16130,7 +16494,7 @@ Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) @@ -16158,7 +16522,7 @@ Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 492 HREAL_LT = |- !X Y. X hreal_lt Y = (?D. Y = X hreal_add D) @@ -16167,7 +16531,7 @@ HREAL_ADD_TOTAL = |- !X Y. (X = Y) \/ (?D. Y = X hreal_add D) \/ (?D. X = Y hreal_add D) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 HREAL_SUP_ISACUT = @@ -16191,7 +16555,7 @@ File hreal.ml loaded () : void -Run time: 0.5s +Run time: 0.9s Intermediate theorems generated: 10456 #\ @@ -16201,7 +16565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -16282,7 +16646,7 @@ Intermediate theorems generated: 12 () : void -Run time: 0.0s +Run time: 0.1s define_equivalence_type = @@ -16376,7 +16740,7 @@ |- !x1 x2 y1 y2. x1 hreal_lt y1 /\ x2 hreal_lt y2 ==> (x1 hreal_add x2) hreal_lt (y1 hreal_add y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 HREAL_LT_LADD = @@ -16482,7 +16846,7 @@ Theorem HREAL_MUL_ASSOC autoloading from theory `HREAL` ... HREAL_MUL_ASSOC = |- !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z -Run time: 0.0s +Run time: 0.1s TREAL_MUL_ASSOC = |- !x y z. x treal_mul (y treal_mul z) = (x treal_mul y) treal_mul z @@ -16493,7 +16857,7 @@ |- !x y z. x treal_mul (y treal_add z) = (x treal_mul y) treal_add (x treal_mul z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 345 TREAL_ADD_LID = |- !x. (treal_0 treal_add x) treal_eq x @@ -16528,7 +16892,7 @@ TREAL_MUL_LINV = |- !x. ~x treal_eq treal_0 ==> ((treal_inv x) treal_mul x) treal_eq treal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x @@ -16541,7 +16905,7 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16568,12 +16932,12 @@ |- (!h. hreal_of_treal(treal_of_hreal h) = h) /\ (!r. treal_0 treal_lt r = (treal_of_hreal(hreal_of_treal r)) treal_eq r) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 986 TREAL_ISO = |- !h i. h hreal_lt i ==> (treal_of_hreal h) treal_lt (treal_of_hreal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 450 TREAL_BIJ_WELLDEF = @@ -16589,7 +16953,7 @@ TREAL_ADD_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1044 TREAL_ADD_WELLDEF = @@ -16631,7 +16995,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -16660,12 +17024,12 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.2s +Run time: 0.4s Intermediate theorems generated: 7766 REAL_ISO_EQ = |- !h i. h hreal_lt i = (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 98 REAL_POS = |- !X. r0 real_lt (real_of_hreal X) @@ -16680,7 +17044,7 @@ Intermediate theorems generated: 68 SUP_ALLPOS_LEMMA2 = |- P(real_of_hreal X) = (\h. P(real_of_hreal h))X -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 5 SUP_ALLPOS_LEMMA3 = @@ -16730,16 +17094,16 @@ |- !x y z. y real_lt z ==> (x real_add y) real_lt (x real_add z); |- !x y. r0 real_lt x /\ r0 real_lt y ==> r0 real_lt (x real_mul y)] : thm list -Run time: 0.0s +Run time: 0.1s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File realax.ml loaded () : void -Run time: 0.9s +Run time: 1.4s Intermediate theorems generated: 26795 #\ @@ -16749,7 +17113,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -16829,7 +17193,7 @@ Run time: 0.0s real_sub = |- !x y. x real_sub y = x real_add (real_neg y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 real_le = |- !x y. x real_le y = ~y real_lt x @@ -16969,7 +17333,7 @@ Intermediate theorems generated: 50 REAL_EQ_RADD = |- !x y z. (x + z = y + z) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 21 REAL_ADD_LID_UNIQ = |- !x y. (x + y = y) = (x = & 0) @@ -17017,7 +17381,7 @@ Intermediate theorems generated: 56 REAL_ENTIRE = |- !x y. (x * y = & 0) = (x = & 0) \/ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 116 REAL_LT_LADD = |- !x y z. (x + y) < (x + z) = y < z @@ -17061,7 +17425,7 @@ 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) @@ -17073,7 +17437,7 @@ Intermediate theorems generated: 22 REAL_LTE_TRANS = |- !x y z. x < y /\ y <= z ==> x < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 47 REAL_LET_TRANS = |- !x y z. x <= y /\ y < z ==> x < z @@ -17113,7 +17477,7 @@ Intermediate theorems generated: 25 REAL_LT_NEGTOTAL = |- !x. (x = & 0) \/ (& 0) < x \/ (& 0) < (-- x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 REAL_LE_NEGTOTAL = |- !x. (& 0) <= x \/ (& 0) <= (-- x) @@ -17125,7 +17489,7 @@ Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 REAL_LE_01 = |- (& 0) <= (& 1) @@ -17145,7 +17509,7 @@ Intermediate theorems generated: 20 REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 55 REAL_LE_ADD2 = |- !w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z) @@ -17225,7 +17589,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) @@ -17293,7 +17657,7 @@ Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17334,7 +17698,7 @@ Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... LESS_EQ_MONO = |- !n m. (SUC n) num_le (SUC m) = n num_le m @@ -17386,7 +17750,7 @@ Run time: 0.0s REAL_MUL = |- !m n. (& m) * (& n) = &(m num_mul n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 148 REAL_INV1 = |- inv(& 1) = & 1 @@ -17439,7 +17803,7 @@ Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 184 Theorem NOT_SUC autoloading from theory `num` ... @@ -17500,7 +17864,7 @@ Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 38 REAL_LE_SUB_RADD = |- !x y z. (x - y) <= z = x <= (z + y) @@ -17524,7 +17888,7 @@ Intermediate theorems generated: 20 REAL_SUB_RZERO = |- !x. x - (& 0) = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 REAL_LET_ADD2 = |- !w x y z. w <= x /\ y < z ==> (w + y) < (x + z) @@ -17540,7 +17904,7 @@ Intermediate theorems generated: 33 REAL_LTE_ADD = |- !x y. (& 0) < x /\ (& 0) <= y ==> (& 0) < (x + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 REAL_LT_MUL2 = @@ -17551,7 +17915,7 @@ Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -17588,7 +17952,7 @@ Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 REAL_SUB_INV2 = @@ -17634,7 +17998,7 @@ REAL_LE_LMUL_IMP = |- !x y z. (& 0) <= x /\ y <= z ==> (x * y) <= (x * z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 65 REAL_LE_RMUL_IMP = @@ -17655,7 +18019,7 @@ Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) @@ -17679,7 +18043,7 @@ Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) @@ -17688,7 +18052,7 @@ REAL_DIV_MUL2 = |- !x z. ~(x = & 0) /\ ~(z = & 0) ==> (!y. y / z = (x * y) / (x * z)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 169 REAL_MIDDLE1 = |- !a b. a <= b ==> a <= ((a + b) / (& 2)) @@ -17700,7 +18064,7 @@ Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) @@ -17733,7 +18097,7 @@ ABS_LT_MUL2 = |- !w x y z. (abs w) < y /\ (abs x) < z ==> (abs(w * x)) < (y * z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 ABS_SUB = |- !x y. abs(x - y) = abs(y - x) @@ -17770,7 +18134,7 @@ Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) @@ -17782,7 +18146,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -17790,7 +18154,7 @@ Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) @@ -17816,7 +18180,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -17828,7 +18192,7 @@ Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) @@ -17840,12 +18204,12 @@ Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 83 POW_PLUS1 = |- !e. (& 0) < e ==> (!n. ((& 1) + ((& n) * e)) <= (((& 1) + e) pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... @@ -17873,7 +18237,7 @@ Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 @@ -17881,7 +18245,7 @@ Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 135 REAL_LE_POW2 = |- !x. (& 0) <= (x pow 2) @@ -17889,7 +18253,7 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 @@ -17932,7 +18296,7 @@ |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -17943,7 +18307,7 @@ Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 SUP_LEMMA3 = @@ -17955,7 +18319,7 @@ |- !P. (?x. P 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: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) @@ -18021,12 +18385,12 @@ Intermediate theorems generated: 202 Sum_DEF = |- !m n f. Sum(m,n)f = sum m n f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18053,14 +18417,14 @@ |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r) <= (g r)) ==> (Sum(m,n)f) <= (Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 272 SUM_EQ = |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r = g r)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 82 SUM_POS = |- !f. (!n. (& 0) <= (f n)) ==> (!m n. (& 0) <= (Sum(m,n)f)) @@ -18070,7 +18434,7 @@ SUM_POS_GEN = |- !f m. (!n. m num_le n ==> (& 0) <= (f n)) ==> (!n. (& 0) <= (Sum(m,n)f)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 SUM_ABS = @@ -18103,7 +18467,7 @@ SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) @@ -18116,7 +18480,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` ... @@ -18141,7 +18505,7 @@ SUM_NSUB = |- !n f c. (Sum(0,n)f) - ((& n) * c) = Sum(0,n)(\p. (f p) - c) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 239 Theorem LESS_SUC autoloading from theory `prim_rec` ... @@ -18161,7 +18525,7 @@ Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) @@ -18176,7 +18540,7 @@ SUM_REINDEX = |- !f m k n. Sum(m num_add k,n)f = Sum(m,n)(\r. f(r num_add k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 117 SUM_0 = |- !m n. Sum(m,n)(\r. & 0) = & 0 @@ -18238,13 +18602,13 @@ Intermediate theorems generated: 206 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File real.ml loaded () : void -Run time: 2.9s +Run time: 4.9s Intermediate theorems generated: 23746 #\ @@ -18254,7 +18618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -18395,7 +18759,7 @@ L re_universe /\ (!a b. L a /\ L b ==> L(a re_intersect b)) /\ (!P. P re_subset L ==> L(re_Union P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 topology_tydef = |- ?rep. TYPE_DEFINITION istopology rep @@ -18459,7 +18823,7 @@ Intermediate theorems generated: 2 CLOSED_LIMPT = |- !top S. closed top S = (!x. limpt top x S ==> S x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 433 ismet = @@ -18495,7 +18859,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 560 metric_tybij = @@ -18659,7 +19023,7 @@ Intermediate theorems generated: 2 MR1_DEF = |- !x y. dist mr1(x,y) = abs(y - x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -18732,13 +19096,13 @@ Intermediate theorems generated: 143 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File topology.ml loaded () : void -Run time: 0.4s +Run time: 0.7s Intermediate theorems generated: 4132 #\ @@ -18748,7 +19112,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -18853,7 +19217,7 @@ Intermediate theorems generated: 30 () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -18914,7 +19278,7 @@ (?n. g n n /\ (!m. g m n ==> P m)) /\ (?n. g n n /\ (!m. g m n ==> Q m)) ==> (?n. g n n /\ (!m. g m n ==> P m /\ Q m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 312 DORDER_THEN = - : ((thm -> *) -> thm -> *) @@ -18971,7 +19335,7 @@ Definition neigh autoloading from theory `TOPOLOGY` ... neigh = |- !top N x. neigh top(N,x) = (?P. open top P /\ P re_subset N /\ P x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem METRIC_SYM autoloading from theory `TOPOLOGY` ... @@ -19122,7 +19486,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19164,7 +19528,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> (?N. g N N /\ (!n. g n N ==> ~(x n = & 0))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 165 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -19261,7 +19625,7 @@ (!x y. bounded(mr1,g)x /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) * (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 484 Theorem REAL_LT_LMUL autoloading from theory `REAL` ... @@ -19340,7 +19704,7 @@ (!x x0 y y0. (x --> x0)(mtop mr1,g) /\ (y --> y0)(mtop mr1,g) ==> ((\n. (x n) - (y n)) --> (x0 - y0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 95 Theorem REAL_ADD_LID autoloading from theory `REAL` ... @@ -19378,7 +19742,7 @@ Theorem REAL_INV_NZ autoloading from theory `REAL` ... REAL_INV_NZ = |- !x. ~(x = & 0) ==> ~(inv x = & 0) -Run time: 0.1s +Run time: 0.0s Theorem ABS_LT_MUL2 autoloading from theory `REAL` ... ABS_LT_MUL2 = @@ -19416,7 +19780,7 @@ (!x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) --> (inv x0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1253 NET_DIV = @@ -19473,7 +19837,7 @@ File nets.ml loaded () : void -Run time: 0.5s +Run time: 0.8s Intermediate theorems generated: 7389 #\ @@ -19483,7 +19847,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -19584,11 +19948,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 () : void -Run time: 0.0s +Run time: 0.1s [(); ()] : void list Run time: 0.0s @@ -19789,7 +20153,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.0s +Run time: 0.1s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -19997,7 +20361,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` ... @@ -20056,7 +20420,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20070,7 +20434,7 @@ Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m -Run time: 0.1s +Run time: 0.0s SEQ_SUBLE = |- !f. subseq f ==> (!n. n num_le (f n)) Run time: 0.0s @@ -20106,7 +20470,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20190,7 +20554,7 @@ SEQ_INV0 = |- !f. (!y. ?N. !n. n num_ge N ==> (f n) > y) ==> (\n. inv(f n)) --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 423 Theorem POW_0 autoloading from theory `REAL` ... @@ -20208,7 +20572,7 @@ Theorem REAL_LT_ADDL autoloading from theory `REAL` ... REAL_LT_ADDL = |- !x y. y < (x + y) = (& 0) < x -Run time: 0.1s +Run time: 0.0s Theorem REAL_LE autoloading from theory `REAL` ... REAL_LE = |- !m n. (& m) <= (& n) = m num_le n @@ -20288,7 +20652,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` ... @@ -20419,7 +20783,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.2s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20491,7 +20855,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) < (f m)) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 209 Theorem LESS_REFL autoloading from theory `prim_rec` ... @@ -20563,13 +20927,13 @@ ((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.0s +Run time: 0.1s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s SER_ADD = |- !x x0 y y0. @@ -20615,7 +20979,7 @@ Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 Theorem SUM_LE autoloading from theory `REAL` ... @@ -20767,7 +21131,7 @@ File seq.ml loaded () : void -Run time: 1.1s +Run time: 1.7s Intermediate theorems generated: 18704 #\ @@ -20777,7 +21141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -20875,11 +21239,11 @@ Run time: 0.0s () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 43 () : void -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -20972,7 +21336,7 @@ Run time: 0.0s LIM_CONST = |- !k x. ((\x. k) --> k)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 193 Theorem DORDER_TENDSTO autoloading from theory `NETS` ... @@ -21124,7 +21488,7 @@ Theorem REAL_HALF_DOUBLE autoloading from theory `REAL` ... REAL_HALF_DOUBLE = |- !x. (x / (& 2)) + (x / (& 2)) = x -Run time: 0.0s +Run time: 0.1s Theorem REAL_LTE_TRANS autoloading from theory `REAL` ... REAL_LTE_TRANS = |- !x y z. x < y /\ y <= z ==> x < z @@ -21146,7 +21510,7 @@ LIM_TRANSFORM = |- !f g x0 l. ((\x. (f x) - (g x)) --> (& 0))x0 /\ (g --> l)x0 ==> (f --> l)x0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 473 diffl = @@ -21187,7 +21551,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 @@ -21299,7 +21663,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.0s +Run time: 0.1s IVT = |- !f a b y. @@ -21307,7 +21671,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` ... @@ -21365,7 +21729,7 @@ Theorem REAL_MUL_ASSOC autoloading from theory `REAL` ... REAL_MUL_ASSOC = |- !x y z. x * (y * z) = (x * y) * z -Run time: 0.1s +Run time: 0.0s Theorem REAL_SUB_RDISTRIB autoloading from theory `REAL` ... REAL_SUB_RDISTRIB = |- !x y z. (x - y) * z = (x * z) - (y * z) @@ -21391,7 +21755,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) * (g x)) diffl ((l * (g x)) + (m * (f x))))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 567 DIFF_CMUL = @@ -21469,7 +21833,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` ... @@ -21477,7 +21841,7 @@ Run time: 0.0s CHAIN_LEMMA2 = |- !x y d. (abs(x - y)) < d ==> (abs x) < ((abs y) + d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 65 Theorem ABS_POS autoloading from theory `REAL` ... @@ -21507,7 +21871,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` ... @@ -21515,7 +21879,7 @@ Run time: 0.0s DIFF_X = |- !x. ((\x. x) diffl (& 1))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 Theorem REAL_MUL_RID autoloading from theory `REAL` ... @@ -21528,7 +21892,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.1s +Run time: 0.0s Theorem ADD_SUB autoloading from theory `arithmetic` ... ADD_SUB = |- !a c. (a num_add c) num_sub c = a @@ -21590,7 +21954,7 @@ DIFF_XM1 = |- !x. ~(x = & 0) ==> ((\x. inv x) diffl (--((inv x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 818 Theorem POW_INV autoloading from theory `REAL` ... @@ -21623,7 +21987,7 @@ ((\x. (f x) / (g x)) diffl (((l * (g x)) - (m * (f x))) / ((g x) pow 2))) x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 293 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -21664,7 +22028,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` ... @@ -21721,7 +22085,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -21811,7 +22175,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -21847,7 +22211,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -21879,7 +22243,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (!x. a <= x /\ x <= b ==> (f x = f a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 310 DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) @@ -21893,7 +22257,7 @@ File lim.ml loaded () : void -Run time: 1.1s +Run time: 1.9s Intermediate theorems generated: 21608 #\ @@ -21903,7 +22267,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -22381,7 +22745,7 @@ summable(\n. (diffs c n) * (x pow n)) ==> (\n. (& n) * ((c n) * (x pow (n num_sub 1)))) sums (suminf(\n. (diffs c n) * (x pow n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 180 Theorem SUB_ADD autoloading from theory `arithmetic` ... @@ -22474,7 +22838,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` ... @@ -22546,7 +22910,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22621,7 +22985,7 @@ (& 0) < k /\ (!h. (& 0) < (abs h) /\ (abs h) < k ==> (abs(f h)) <= (K * (abs h))) ==> (f tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 917 Theorem SER_LE autoloading from theory `SEQ` ... @@ -22653,7 +23017,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` ... @@ -22765,7 +23129,7 @@ File powser.ml loaded () : void -Run time: 0.6s +Run time: 0.8s Intermediate theorems generated: 8507 #\ @@ -22775,7 +23139,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -22880,7 +23244,7 @@ Run time: 0.0s MULT_DIV_2 = |- !n. (2 * n) DIV 2 = n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 66 Theorem LEFT_ADD_DISTRIB autoloading from theory `arithmetic` ... @@ -22943,7 +23307,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23106,7 +23470,7 @@ Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s Theorem NOT_SUC autoloading from theory `num` ... NOT_SUC = |- !n. ~(SUC n = 0) @@ -23331,7 +23695,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` ... @@ -23475,7 +23839,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) @@ -23500,7 +23864,7 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 @@ -23659,7 +24023,7 @@ Intermediate theorems generated: 2 LN_EXP = |- !x. ln(exp x) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 52 EXP_LN = |- !x. (exp(ln x) = x) = (& 0) < x @@ -23672,7 +24036,7 @@ LN_MUL = |- !x y. (& 0) < x /\ (& 0) < y ==> (ln(x * y) = (ln x) + (ln y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 113 LN_INJ = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x = ln y) = (x = y)) @@ -23728,7 +24092,7 @@ ROOT_LT_LEMMA = |- !n x. (& 0) < x ==> ((exp((ln x) / (&(SUC n)))) pow (SUC n) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 123 ROOT_LN = @@ -23757,7 +24121,7 @@ Intermediate theorems generated: 28 ROOT_POW_POS = |- !n x. (& 0) <= x ==> ((root(SUC n)x) pow (SUC n) = x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 66 SQRT_0 = |- sqrt(& 0) = & 0 @@ -23843,7 +24207,7 @@ Run time: 0.0s SIN_BOUNDS = |- !x. (--(& 1)) <= (sin x) /\ (sin x) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 Theorem REAL_LET_ADD autoloading from theory `REAL` ... @@ -23851,7 +24215,7 @@ Run time: 0.0s COS_BOUND = |- !x. (abs(cos x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 160 COS_BOUNDS = |- !x. (--(& 1)) <= (cos x) /\ (cos x) <= (& 1) @@ -23887,7 +24251,7 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -23958,7 +24322,7 @@ (((--(& 1)) pow n) / (&(FACT((2 num_mul n) num_add 1)))) * (x pow ((2 num_mul n) num_add 1))) sums (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... @@ -24004,7 +24368,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24092,7 +24456,7 @@ Run time: 0.0s COS_ISZERO = |- ?! x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24212,7 +24576,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` ... @@ -24277,7 +24641,7 @@ |- !x. (& 0) <= x /\ (cos x = & 0) ==> (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 675 Theorem REAL_LE_ADDR autoloading from theory `REAL` ... @@ -24320,7 +24684,7 @@ (sin x = & 0) = (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 319 tan = |- !x. tan x = (sin x) / (cos x) @@ -24344,7 +24708,7 @@ Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 Theorem REAL_LDISTRIB autoloading from theory `REAL` ... @@ -24364,7 +24728,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 = @@ -24383,7 +24747,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24456,7 +24820,7 @@ TAN_TOTAL = |- !y. ?! x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1301 asn = @@ -24483,7 +24847,7 @@ (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) /\ (sin(asn y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 ASN_SIN = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (sin(asn y) = y) @@ -24494,7 +24858,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 SIN_ASN = @@ -24532,7 +24896,7 @@ Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) @@ -24541,7 +24905,7 @@ TAN_ATN = |- !x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) ==> (atn(tan x) = x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 103 () : void @@ -24551,7 +24915,7 @@ File transc.ml loaded () : void -Run time: 1.9s +Run time: 3.0s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24564,7 +24928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -24586,7 +24950,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -24652,7 +25016,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -24684,7 +25048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -24793,7 +25157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -24946,7 +25310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25019,7 +25383,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25099,7 +25463,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25256,7 +25620,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25411,7 +25775,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25628,7 +25992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25650,7 +26014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25669,7 +26033,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25714,7 +26078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25779,7 +26143,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25829,7 +26193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25899,7 +26263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -25969,7 +26333,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26005,7 +26369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26058,7 +26422,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26130,7 +26494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26209,7 +26573,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26404,7 +26768,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26441,7 +26805,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26789,9 +27153,2395 @@ (LASTN((m + k) - (LENGTH l2))l1) (LASTN((LENGTH l2) - k)(BUTLASTN k l2))) -evaluation failed EVERY_CONV -evaluation failed load -- mk_word_base -make[4]: *** [Makefile:69: word_base.th] Error 1 +word_Ax = |- !f. ?! fn. !l. fn(WORD l) = f l + +WORD_11 = |- !l l'. (WORD l = WORD l') = (l = l') + +word_induct = |- !P. (!l. P(WORD l)) ==> (!w. P w) + +word_cases = |- !w. ?l. w = WORD l + +WORDLEN_DEF = |- !l. WORDLEN(WORD l) = LENGTH l + +PWORDLEN_DEF = |- !n l. PWORDLEN n(WORD l) = (n = LENGTH l) + + +word_CASES_TAC = - : (term -> tactic) + +word_INDUCT_TAC = - : tactic + +RESQ_WORDLEN_TAC = - : tactic + + +File word_funs loaded +() : void + +PWORDLEN = |- !n w. PWORDLEN n w = (WORDLEN w = n) + +Theorem NOT_SUC autoloading from theory `num` ... +NOT_SUC = |- !n. ~(SUC n = 0) + +PWORDLEN0 = |- !w. PWORDLEN 0 w ==> (w = WORD[]) + +PWORDLEN1 = |- !x. PWORDLEN 1(WORD[x]) + +WSEG_DEF = |- !m k l. WSEG m k(WORD l) = WORD(LASTN m(BUTLASTN k l)) + +WSEG0 = |- !k w. WSEG 0 k w = WORD[] + +Theorem LENGTH_LASTN autoloading from theory `list` ... +LENGTH_LASTN = |- !n l. n <= (LENGTH l) ==> (LENGTH(LASTN n l) = n) + +WSEG_PWORDLEN = +|- !n. !w :: PWORDLEN n. !m k. (m + k) <= n ==> PWORDLEN m(WSEG m k w) + +WSEG_WORDLEN = +|- !n. + !w :: PWORDLEN n. !m k. (m + k) <= n ==> (WORDLEN(WSEG m k w) = m) + +WSEG_WORD_LENGTH = |- !n. !w :: PWORDLEN n. WSEG n 0 w = w + +BIT_DEF = |- !k l. BIT k(WORD l) = ELL k l + +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 LAST autoloading from theory `list` ... +LAST = |- !x l. LAST(SNOC x l) = x + +Definition ELL autoloading from theory `list` ... +ELL = +|- (!l. ELL 0 l = LAST l) /\ (!n l. ELL(SUC n)l = ELL n(BUTLAST l)) + +BIT0 = |- !b. BIT 0(WORD[b]) = b + +Theorem BUTLAST autoloading from theory `list` ... +BUTLAST = |- !x l. BUTLAST(SNOC x l) = l + +WSEG_BIT = +|- !n. !w :: PWORDLEN n. !k. k < n ==> (WSEG 1 k w = WORD[BIT k w]) + +BIT_WSEG = +|- !n. + !w :: PWORDLEN n. + !m k j. + (m + k) <= n ==> j < m ==> (BIT j(WSEG m k w) = BIT(j + k)w) + +MSB_DEF = |- !l. MSB(WORD l) = HD l + +Theorem ELL_PRE_LENGTH autoloading from theory `list` ... +ELL_PRE_LENGTH = |- !l. ~(l = []) ==> (ELL(PRE(LENGTH l))l = HD l) + +Theorem NULL_EQ_NIL autoloading from theory `list` ... +NULL_EQ_NIL = |- !l. NULL l = (l = []) + +Theorem LENGTH_NOT_NULL autoloading from theory `list` ... +LENGTH_NOT_NULL = |- !l. 0 < (LENGTH l) = ~NULL l + +MSB = |- !n. !w :: PWORDLEN n. 0 < n ==> (MSB w = BIT(PRE n)w) + +LSB_DEF = |- !l. LSB(WORD l) = LAST l + +Theorem ELL_LAST autoloading from theory `list` ... +ELL_LAST = |- !l. ~NULL l ==> (ELL 0 l = LAST l) + +LSB = |- !n. !w :: PWORDLEN n. 0 < n ==> (LSB w = BIT 0 w) + +WSPLIT_DEF = +|- !m l. WSPLIT m(WORD l) = WORD(BUTLASTN m l),WORD(LASTN m l) + +th = |- ?bt. !l. bt(WORD l) = l + +word_bits = |- ?bt. (!l. bt(WORD l) = l) /\ (!w. WORD(bt w) = w) + +WCAT_lemma = +|- ?WCAT. !l1 l2. WCAT(WORD l1,WORD l2) = WORD(APPEND l1 l2) + +WCAT_DEF = |- !l1 l2. WCAT(WORD l1,WORD l2) = WORD(APPEND l1 l2) + +Theorem APPEND_BUTLASTN_LASTN autoloading from theory `list` ... +APPEND_BUTLASTN_LASTN = +|- !n l. n <= (LENGTH l) ==> (APPEND(BUTLASTN n l)(LASTN n l) = l) + +WCAT_WSPLIT = +|- !n. !w :: PWORDLEN n. !m. m <= n ==> (WCAT(WSPLIT m w) = w) + +Theorem LASTN_LENGTH_APPEND autoloading from theory `list` ... +LASTN_LENGTH_APPEND = |- !l1 l2. LASTN(LENGTH l2)(APPEND l1 l2) = l2 + +Theorem BUTLASTN_LENGTH_APPEND autoloading from theory `list` ... +BUTLASTN_LENGTH_APPEND = +|- !l2 l1. BUTLASTN(LENGTH l2)(APPEND l1 l2) = l1 + +WSPLIT_WCAT = +|- !n m. + !w1 :: PWORDLEN n. !w2 :: PWORDLEN m. WSPLIT m(WCAT(w1,w2)) = w1,w2 + +WORD_PARTITION = +|- (!n. !w :: PWORDLEN n. !m. m <= n ==> (WCAT(WSPLIT m w) = w)) /\ + (!n m. + !w1 :: PWORDLEN n. !w2 :: PWORDLEN m. WSPLIT m(WCAT(w1,w2)) = w1,w2) + +Theorem APPEND_ASSOC autoloading from theory `list` ... +APPEND_ASSOC = +|- !l1 l2 l3. APPEND l1(APPEND l2 l3) = APPEND(APPEND l1 l2)l3 + +WCAT_ASSOC = |- !w1 w2 w3. WCAT(w1,WCAT(w2,w3)) = WCAT(WCAT(w1,w2),w3) + +WCAT0 = |- !w. (WCAT(WORD[],w) = w) /\ (WCAT(w,WORD[]) = w) + +Theorem APPEND_LENGTH_EQ autoloading from theory `list` ... +APPEND_LENGTH_EQ = +|- !l1 l1'. + (LENGTH l1 = LENGTH l1') ==> + (!l2 l2'. + (LENGTH l2 = LENGTH l2') ==> + ((APPEND l1 l2 = APPEND l1' l2') = (l1 = l1') /\ (l2 = l2'))) + +WCAT_11 = +|- !m n. + !wm1 wm2 :: PWORDLEN m. + !wn1 wn2 :: PWORDLEN n. + (WCAT(wm1,wn1) = WCAT(wm2,wn2)) = (wm1 = wm2) /\ (wn1 = wn2) + +WSPLIT_PWORDLEN = +|- !n. + !w :: PWORDLEN n. + !m. + m <= n ==> + PWORDLEN(n - m)(FST(WSPLIT m w)) /\ PWORDLEN m(SND(WSPLIT m w)) + +Theorem LENGTH_APPEND autoloading from theory `list` ... +LENGTH_APPEND = +|- !l1 l2. LENGTH(APPEND l1 l2) = (LENGTH l1) + (LENGTH l2) + +WCAT_PWORDLEN = +|- !n1. + !w1 :: PWORDLEN n1. + !n2. !w2 :: PWORDLEN n2. PWORDLEN(n1 + n2)(WCAT(w1,w2)) + +Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... +LESS_EQ_SUC_REFL = |- !m. m <= (SUC m) + +WORDLEN_SUC_WCAT = +|- !n w. + PWORDLEN(SUC n)w ==> + (?b :: PWORDLEN 1. ?w' :: PWORDLEN n. w = WCAT(b,w')) + +Theorem LASTN_LASTN autoloading from theory `list` ... +LASTN_LASTN = +|- !l n m. + m <= (LENGTH l) ==> n <= m ==> (LASTN n(LASTN m l) = LASTN n l) + +Theorem BUTLASTN_BUTLASTN autoloading from theory `list` ... +BUTLASTN_BUTLASTN = +|- !m n l. + (n + m) <= (LENGTH l) ==> + (BUTLASTN n(BUTLASTN m l) = BUTLASTN(n + m)l) + +Theorem BUTLASTN_LASTN autoloading from theory `list` ... +BUTLASTN_LASTN = +|- !m n l. + m <= n /\ n <= (LENGTH l) ==> + (BUTLASTN m(LASTN n l) = LASTN(n - m)(BUTLASTN m l)) + +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) + +WSPLIT_WSEG = +|- !n. + !w :: PWORDLEN n. + !k. k <= n ==> (WSPLIT k w = WSEG(n - k)k w,WSEG k 0 w) + +WSPLIT_WSEG1 = +|- !n. + !w :: PWORDLEN n. !k. k <= n ==> (FST(WSPLIT k w) = WSEG(n - k)k w) + +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/11/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/11/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/11/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/11/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/11/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/11/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/11/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 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);;'\ @@ -26800,7 +29550,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -26999,7 +29749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27031,7 +29781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27165,7 +29915,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27468,7 +30218,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27500,7 +30250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27539,7 +30289,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27571,7 +30321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27732,7 +30482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -27865,7 +30615,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28054,7 +30804,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28114,7 +30864,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28239,7 +30989,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28350,7 +31100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28375,7 +31125,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28403,7 +31153,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -28516,7 +31266,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29019,7 +31769,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29267,7 +32017,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29493,7 +32243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29535,7 +32285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29567,7 +32317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -29790,7 +32540,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -30183,7 +32933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -30296,7 +33046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -30799,7 +33549,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31047,7 +33797,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31273,7 +34023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31308,7 +34058,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31347,7 +34097,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31384,7 +34134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31405,7 +34155,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31502,7 +34252,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -31524,7 +34274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32020,7 +34770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32043,7 +34793,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32121,7 +34871,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32180,7 +34930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32224,7 +34974,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32242,7 +34992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32269,7 +35019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32313,7 +35063,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32426,7 +35176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32473,7 +35223,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32512,7 +35262,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32586,7 +35336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32675,7 +35425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32746,7 +35496,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32816,7 +35566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32865,7 +35615,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32906,7 +35656,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32947,7 +35697,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -32971,7 +35721,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33072,7 +35822,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33093,7 +35843,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33118,7 +35868,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33744,7 +36494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33821,7 +36571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33848,7 +36598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -33965,7 +36715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34060,7 +36810,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34146,7 +36896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34261,7 +37011,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34354,7 +37104,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34530,7 +37280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34634,7 +37384,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -34929,7 +37679,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35032,7 +37782,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35100,7 +37850,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35162,7 +37912,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35342,7 +38092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35383,7 +38133,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35413,7 +38163,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35439,7 +38189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -35957,7 +38707,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -36494,7 +39244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -36682,7 +39432,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #false : bool @@ -36700,10 +39450,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Tue Nov 5 14:07:11 -12 2024 +Wed Nov 6 17:04:28 +14 2024 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Nov 5 14:07:11 -12 2024 +Wed Nov 6 17:04:28 +14 2024 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -36723,20 +39473,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 5/11/24 + HOL88 Version 2.02 (GCL), built on 6/11/24 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 5/11/24 +BASIC-HOL version 2.02 (GCL) created 6/11/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 5/11/24 +HOL-LCF version 2.02 (GCL) created 6/11/24 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39058,7 +41808,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' @@ -41838,7 +44588,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' @@ -44270,7 +47020,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' @@ -44577,7 +47327,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' @@ -44878,7 +47628,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' @@ -45125,7 +47875,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' @@ -45381,7 +48131,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' @@ -45541,7 +48291,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' @@ -45682,7 +48432,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' @@ -45994,7 +48744,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' @@ -46530,7 +49280,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' @@ -46957,7 +49707,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' @@ -47426,7 +50176,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' @@ -47700,7 +50450,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' @@ -48075,7 +50825,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' @@ -48306,7 +51056,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' @@ -48484,7 +51234,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' @@ -48697,7 +51447,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' @@ -48941,7 +51691,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' @@ -49183,7 +51933,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' @@ -49493,7 +52243,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' @@ -49853,7 +52603,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' @@ -50164,7 +52914,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.11.05:1410' -> endpages.ps +' TeX output 2024.11.06:1709' -> endpages.ps @@ -50236,7 +52986,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.11.05:1410' -> titlepages.ps +' TeX output 2024.11.06:1709' -> titlepages.ps @@ -50315,8 +53065,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 @@ -50364,10 +53114,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_makeshlibs: warning: Compatibility levels before 10 are deprecated (level 9 in use) @@ -50377,16 +53129,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-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-source' in '../hol88-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 @@ -50396,12 +53149,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/19671/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/19671/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/17935 and its subdirectories -I: Current time: Tue Nov 5 14:11:50 -12 2024 -I: pbuilder-time-stamp: 1730859110 +I: removing directory /srv/workspace/pbuilder/19671 and its subdirectories +I: Current time: Wed Nov 6 17:12:35 +14 2024 +I: pbuilder-time-stamp: 1730862755