Mock Version: 1.4.21 Mock Version: 1.4.21 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f33-build-132696-41244/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'}shell=Falselogger=timeout=432000uid=987gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'} and shell False Building target platforms: riscv64 Building for target riscv64 setting SOURCE_DATE_EPOCH=1581552000 Wrote: /builddir/build/SRPMS/metamath-0.181-1.fc33.src.rpm Child return code was: 0 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f33-build-132696-41244/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'}shell=Falselogger=timeout=432000uid=987gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'} and shell False Building target platforms: riscv64 Building for target riscv64 setting SOURCE_DATE_EPOCH=1581552000 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.gskJLr + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf metamath + /usr/bin/tar -xof - + /usr/bin/bzip2 -dc /builddir/build/SOURCES/metamath.tar.bz2 + STATUS=0 + '[' 0 -ne 0 ']' + cd metamath + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + cp -p /builddir/build/SOURCES/metamath.tex . + touch special-settings.sty + rm metamath.exe + sed -i '/Try to optimize/,/^$/d' configure.ac + autoreconf -fi configure.ac:13: installing './compile' configure.ac:9: installing './install-sh' configure.ac:9: installing './missing' Makefile.am: installing './depcomp' + RPM_EC=0 ++ jobs -p + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.9vVF1r + umask 022 + cd /builddir/build/BUILD + cd metamath + CFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection' + export CFLAGS + CXXFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection' + export CXXFLAGS + FFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules' + export FFLAGS + FCFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules' + export FCFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + '[' 1 = 1 ']' +++ dirname ./configure ++ find . -name config.guess -o -name config.sub + '[' 1 = 1 ']' + '[' x '!=' 'x-Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld' ']' ++ find . -name ltmain.sh + ./configure --build=riscv64-redhat-linux-gnu --host=riscv64-redhat-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info 'CFLAGS=-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv' checking for a BSD-compatible install... /usr/bin/install -c checking whether build environment is sane... yes checking for a thread-safe mkdir -p... /usr/bin/mkdir -p checking for gawk... gawk checking whether make sets $(MAKE)... yes checking whether make supports nested variables... yes checking for riscv64-redhat-linux-gnu-gcc... no checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking whether gcc understands -c and -o together... yes checking whether make supports the include directive... yes (GNU style) checking dependency style of gcc... none checking how to run the C preprocessor... gcc -E checking for grep that handles long lines and -e... /usr/bin/grep checking for egrep... /usr/bin/grep -E checking for ANSI C header files... yes checking for sys/types.h... yes checking for sys/stat.h... yes checking for stdlib.h... yes checking for string.h... yes checking for memory.h... yes checking for strings.h... yes checking for inttypes.h... yes checking for stdint.h... yes checking for unistd.h... yes checking limits.h usability... yes checking limits.h presence... yes checking for limits.h... yes checking for stdlib.h... (cached) yes checking for string.h... (cached) yes checking for stdbool.h that conforms to C99... yes checking for _Bool... yes checking for size_t... yes checking for stdlib.h... (cached) yes checking for GNU libc compatible malloc... yes checking for stdlib.h... (cached) yes checking for GNU libc compatible realloc... yes checking for strchr... yes checking for strcspn... yes checking for strstr... yes checking for gcc warning flags... yes checking for 'inline' support... yes CFLAGS=-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra checking that generated files are newer than configure... done configure: creating ./config.status config.status: creating Makefile config.status: creating config.h config.status: executing depfiles commands + make -j4 make all-am make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o metamath.o metamath.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmdl.o mmcmdl.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmds.o mmcmds.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmdata.o mmdata.c mmdata.c: In function 'getContrib': mmdata.c:3436:45: warning: comparison is always false due to limited range of data type [-Wtype-limits] 3436 | (vstring)(reviseDateList[stmtNum])) == -1) { | ^~ mmdata.c:3441:46: warning: comparison is always false due to limited range of data type [-Wtype-limits] 3441 | (vstring)(shortenDateList[stmtNum])) == -1) { | ^~ mmdata.c:3687:51: warning: comparison is always true due to limited range of data type [-Wtype-limits] 3687 | && compareDates(contribDate, reviseDate) != -1) | ^~ mmdata.c:3689:52: warning: comparison is always true due to limited range of data type [-Wtype-limits] 3689 | && compareDates(contribDate, shortenDate) != -1))) { | ^~ mmcmds.c: In function 'verifyMarkup': mmcmds.c:4999:46: warning: comparison is always false due to limited range of data type [-Wtype-limits] 4999 | if (compareDates(mostRecentDate, str1) == -1) { | ^~ metamath.c: In function 'command': metamath.c:1075:15: warning: ignoring return value of 'system' declared with attribute 'warn_unused_result' [-Wunused-result] 1075 | (void)system(str1); | ^~~~~~~~~~~~ gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpa.o mmhlpa.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpb.o mmhlpb.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mminou.o mminou.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmmaci.o mmmaci.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpars.o mmpars.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpfas.o mmpfas.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmunif.o mmunif.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmutil.o mmutil.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmveri.o mmveri.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmvstr.o mmvstr.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmword.o mmword.c gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmwtex.o mmwtex.c mmwtex.c: In function 'printTexComment': mmwtex.c:2108:18: warning: comparison is always false due to limited range of data type [-Wtype-limits] 2108 | if (mode == -1) { /* Math mode */ | ^~ gcc -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -Wl,-z,relro -Wl,--as-needed -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -o metamath metamath.o mmcmdl.o mmcmds.o mmdata.o mmhlpa.o mmhlpb.o mminou.o mmmaci.o mmpars.o mmpfas.o mmunif.o mmutil.o mmveri.o mmvstr.o mmword.o mmwtex.o make[1]: Leaving directory '/builddir/build/BUILD/metamath' + touch metamath.ind + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (preloaded format=pdflatex) restricted \write18 enabled. kpathsea: Running mktexfmt pdflatex.fmt mktexfmt: mktexfmt is using the following fmtutil.cnf files (in precedence order): mktexfmt: /usr/share/texlive/texmf-dist/web2c/fmtutil.cnf mktexfmt: mktexfmt is using the following fmtutil.cnf file for writing changes: mktexfmt: /builddir/.texlive2019/texmf-config/web2c/fmtutil.cnf mktexfmt [INFO]: writing formats under /builddir/.texlive2019/texmf-var/web2c mktexfmt [INFO]: --- remaking pdflatex with pdftex mktexfmt: running `pdftex -ini -jobname=pdflatex -progname=pdflatex -translate-file=cp227.tcx *pdflatex.ini' ... This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (INITEX) restricted \write18 enabled. (/usr/share/texlive/texmf-dist/web2c/cp227.tcx) entering extended mode (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/pdflatex.ini (/usr/share/texlive/texmf-dist/tex/generic/tex-ini-files/pdftexconfig.tex) (/usr/share/texlive/texmf-dist/tex/latex/base/latex.ltx (/usr/share/texlive/texmf-dist/tex/latex/base/texsys.cfg) ./texsys.aux found \@currdir set to: ./. Assuming \openin and \input have the same search path. Defining UNIX/DOS style filename parser. catcodes, registers, parameters, LaTeX2e <2018-12-01> hacks, control, par, spacing, files, font encodings, lengths, ==================================== Local config file fonttext.cfg used ==================================== (/usr/share/texlive/texmf-dist/tex/latex/base/fonttext.cfg (/usr/share/texlive/texmf-dist/tex/latex/base/fonttext.ltx === Don't modify this file, use a .cfg file instead === (/usr/share/texlive/texmf-dist/tex/latex/base/omlenc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/t1cmr.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmr.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmss.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmtt.fd))) ==================================== Local config file fontmath.cfg used ==================================== (/usr/share/texlive/texmf-dist/tex/latex/base/fontmath.cfg (/usr/share/texlive/texmf-dist/tex/latex/base/fontmath.ltx === Don't modify this file, use a .cfg file instead === (/usr/share/texlive/texmf-dist/tex/latex/base/omlcmm.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/omscmsy.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/omxcmex.fd) (/usr/share/texlive/texmf-dist/tex/latex/base/ucmr.fd))) ==================================== Local config file preload.cfg used ===================================== (/usr/share/texlive/texmf-dist/tex/latex/base/preload.cfg (/usr/share/texlive/texmf-dist/tex/latex/base/preload.ltx)) page nos., x-ref, environments, center, verbatim, math definitions, boxes, title, sectioning, contents, floats, footnotes, index, bibliography, output, =========================================== Local configuration file hyphen.cfg used =========================================== (/usr/share/texlive/texmf-dist/tex/generic/babel/hyphen.cfg (/usr/share/texlive/texmf-dist/tex/generic/babel/switch.def) (/usr/share/texlive/texmf-dist/tex/generic/hyphen/hyphen.tex) (/usr/share/texlive/texmf-dist/tex/generic/hyphen/dumyhyph.tex) (/usr/share/texlive/texmf-dist/tex/generic/hyphen/zerohyph.tex)) (/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu) (/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)) ) ) Beginning to dump on file pdflatex.fmt (preloaded format=pdflatex 2020.3.28) 5447 strings of total length 72682 51327 memory locations dumped; current usage is 144&51153 3775 multiletter control sequences \font\nullfont=nullfont \font\OMX/cmex/m/n/10=cmex10 \font\tenln=line10 \font\tenlnw=linew10 \font\tencirc=lcircle10 \font\tencircw=lcirclew10 \font\OT1/cmr/m/n/5=cmr5 \font\OT1/cmr/m/n/7=cmr7 \font\OT1/cmr/m/n/10=cmr10 \font\OML/cmm/m/it/5=cmmi5 \font\OML/cmm/m/it/7=cmmi7 \font\OML/cmm/m/it/10=cmmi10 \font\OMS/cmsy/m/n/5=cmsy5 \font\OMS/cmsy/m/n/7=cmsy7 \font\OMS/cmsy/m/n/10=cmsy10 3633 words of font info for 14 preloaded fonts 14 hyphenation exceptions Hyphenation trie of length 6081 has 183 ops out of 35111 2 for language 1 181 for language 0 0 words of pdfTeX memory 0 indirect objects No pages of output. Transcript written on pdflatex.log. mktexfmt [INFO]: /builddir/.texlive2019/texmf-var/web2c/pdftex/pdflatex.fmt installed. mktexfmt [INFO]: Successfully rebuilt formats: 1 mktexfmt [INFO]: Not selected formats: 15 mktexfmt [INFO]: Total formats: 16 mktexfmt [INFO]: exiting with status 0 entering extended mode (./metamath.tex LaTeX2e <2018-12-01> LaTeX Warning: Writing file `./realref.sty'. LaTeX Warning: Writing file `./metamath.bib'. (/usr/share/texlive/texmf-dist/tex/latex/base/book.cls Document Class: book 2018/09/03 v1.4i Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo) (/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty) (/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty (/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym) (/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty (/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty document style option `anysize' loaded Michael Salzenberg, Thomas Esser, Dirk Hillbrecht Version 1.0, Aug 13, 1994 ) (./special-settings.sty) Writing index file metamath.idx No file metamath.aux. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] [3] [4] [5] [6] LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page vii undefined o n input line 1118. LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page vii undefined on input line 1123. [7] [8] LaTeX Warning: Citation `Barrow' on page ix undefined on input line 1220. [9] LaTeX Warning: Citation `Davis' on page x undefined on input line 1245. [10] [11] [12] [13] [14] Chapter 1. LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428. [1] LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521. [2] [3] LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588. [4] LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625. LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631. [5] LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663. [6] [7] LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783. [8] [9] [10] [11] LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998. [12] [13] LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072. LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080. LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089. LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111. [14] LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140. LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156. LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164. LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169. [15] LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220. [16] LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254. LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254. LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256. LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258. LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275. LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288. LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288. [17] LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302. LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322. [18] [19] LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417. LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442. [20] LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477. LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489. [21] LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523. LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530. (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546. LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549. [22] LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577. LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587. LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591. LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593. LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604. LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605. [23] LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634. LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 2663. [24] LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26 79. LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688. LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698. LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703. LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713. [25] LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755. [26] LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783. LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792. LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800. LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831. [27] [28] LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 2910. LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932. [29] [30] [31] [32] LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143. LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144. LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152. LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164. LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172. [33] LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202. LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214. LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260. LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262. [34] LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277. [35] [36] Chapter 2. [37] LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380. [38] [39] LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516. LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517. [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58] Chapter 3. LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512. [59] [60] [61] LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724. [62] Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739 []\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut ed to Jan []ukasiewicz [63] [64] Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873 \OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz ation.''[] LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919. [65] LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932. LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973. [66] LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001. LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018. LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037. [67] [68] [69] [70] Overfull \hbox (23.8602pt too wide) in paragraph at lines 5320--5320 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarski's Overfull \hbox (33.01625pt too wide) in paragraph at lines 5400--5400 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxiliary [71] [72] [73] LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722. LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723. LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724. LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724. [74] [75] [76] LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986. LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988. LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989. [77] [78] [79] [80] [81] [82] [83] [84] [85] LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946. [86] [87] [88] Overfull \hbox (7.99037pt too wide) in paragraph at lines 7289--7289 []\OT1/cmr/bx/n/12 The Ax-ioms for Real and Com-plex Num-bers Them- [89] [90] [91] LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649. [92] [93] LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789. [94] [95] [96] [97] LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056. [98] LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093. LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109. [99] Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Ex- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Trans- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Ration- Underfull \hbox (badness 7379) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Ra- Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmtt/m/n/10 pm2.65da Package longtable Warning: Column widths have changed (longtable) in table 3.4 on input line 8218. [100] [101] LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8338. [102] [103] [104] LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477. [105] [106] [107] [108] [109] [110] Chapter 4. LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768. [111] LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820. [112] [113] [114] [115] [116] [117] [118] [119] [120] [121] [122] [123] [124] LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777. [125] [126] [127] [128] [129] [130] [131] LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined (Font) using `OMS/cmtt/m/n' instead (Font) for symbol `textbraceleft' on input line 10257. [132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149] LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675. [150] LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686 . LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702. LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780. LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789. [151] LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824. [152] [153] [154] Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023 []\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases [155] [156] Chapter 5. [157] [158] [159] [160] [161] [162] [163] [164] [165] Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677 \OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m /n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1 0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth [166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] Appendix A. LaTeX Warning: Hyper reference `df-bi' on page 183 undefined on input line 1387 4. Underfull \hbox (badness 3780) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for LaTeX Warning: Hyper reference `df-or' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-3or' on page 183 undefined on input line 138 74. LaTeX Warning: Hyper reference `df-an' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-3an' on page 183 undefined on input line 138 74. LaTeX Warning: Hyper reference `df-ex' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-sb' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-eu' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-clab' on page 183 undefined on input line 13 874. LaTeX Warning: Hyper reference `df-cleq' on page 183 undefined on input line 13 874. LaTeX Warning: Hyper reference `df-clel' on page 183 undefined on input line 13 874. LaTeX Warning: Hyper reference `df-v' on page 183 undefined on input line 13874 . LaTeX Warning: Hyper reference `df-ss' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-un' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-in' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-dif' on page 183 undefined on input line 138 74. LaTeX Warning: Hyper reference `df-nul' on page 183 undefined on input line 138 74. LaTeX Warning: Hyper reference `df-pw' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-op' on page 183 undefined on input line 1387 4. LaTeX Warning: Hyper reference `df-fv' on page 183 undefined on input line 1387 4. Underfull \hbox (badness 4266) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion; Package longtable Warning: Column widths have changed (longtable) in table A.1 on input line 13874. [183] [184] [185] [186] Appendix B. [187] [188] Appendix C. LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141. LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155. LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172. [189] [190] [191] LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359. [192] [193] [194] LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580. LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581. (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14635. [195] [196] [197] LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805. LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812. [198] LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896. [199] [200] [201] LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136. LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137. [202] [203] [204] [205] [206] Appendix D. [207] [208] LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417. [209] [210] Appendix E. [211] [212] [213] [214] No file metamath.bbl. (./metamath.ind) Package longtable Warning: Table widths have changed. Rerun LaTeX. (./metamath.aux) Package rerunfilecheck Warning: File `metamath.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Font Warning: Some font shapes were not available, defaults substituted. LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. ) (see the transcript file for additional information)pdfTeX warning (dest): name {page.\\page@num.exampleref\040} has been referenced but does not exist, replac ed by a fixed one pdfTeX warning (dest): name{page.\\page@num.frameconvert\040} has been referenc ed but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.tcomment\040} has been referenced b ut does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.htmlout\040} has been referenced bu t does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.framelist\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.redeclaration\040} has been referen ced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.spec1chars\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.mathcomments\040} has been referenc ed but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.tut1\040} has been referenced but d oes not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.ax1\040} has been referenced but do es not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.dfbr\040} has been referenced but d oes not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.dfopr\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.effectivelybound\040} has been refe renced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.expandom\040} has been referenced b ut does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.dfom\040} has been referenced but d oes not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.dfclel\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.dollardollar\040} has been referenc ed but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.zeroproof\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.treeproof\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.includef\040} has been referenced b ut does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.demo0\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.demoproof\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.nodd\040} has been referenced but d oes not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.envision\040} has been referenced b ut does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.languagespec\040} has been referenc ed but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.using\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.spec\040} has been referenced but d oes not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.poincare\040} has been referenced b ut does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.namespace\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.categoryth\040} has been referenced but does not exist, replaced by a fixed one pdfTeX warning (dest): name{page.\\page@num.bourbaki\040} has been referenced b ut does not exist, replaced by a fixed one < /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb> Output written on metamath.pdf (228 pages, 1018989 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2018-12-01> LaTeX Warning: File `realref.sty' already exists on the system. Not generating it from this source. LaTeX Warning: File `metamath.bib' already exists on the system. Not generating it from this source. (/usr/share/texlive/texmf-dist/tex/latex/base/book.cls Document Class: book 2018/09/03 v1.4i Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo) (/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty) (/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty (/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym) (/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty (/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty document style option `anysize' loaded Michael Salzenberg, Thomas Esser, Dirk Hillbrecht Version 1.0, Aug 13, 1994 ) (./special-settings.sty) Writing index file metamath.idx (./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] (./metamath.toc [3] [4] LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 108. [5] [6]) [7] [8] [9] [10] LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on input line 1118. LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i nput line 1123. [11] [12] LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1220. [13] LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1245. [14] [15] [16] [17] [18] Chapter 1. LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428. [1] LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521. [2] [3] LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588. [4] LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625. LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631. [5] LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663. [6] [7] LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783. [8] [9] [10] [11] LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998. [12] [13] LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072. LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080. LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089. LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111. [14] LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140. LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156. LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164. LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169. [15] LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220. [16] LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254. LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254. LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256. LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258. LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275. LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288. LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288. [17] LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302. LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322. [18] [19] LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417. LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442. [20] LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477. LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489. [21] LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523. LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530. (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546. LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549. [22] LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577. LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587. LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591. LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593. LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604. LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605. [23] LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634. [24] LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26 79. LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688. LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698. LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703. LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713. [25] LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755. [26] LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783. LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792. LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800. LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831. [27] [28] LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 2910. LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932. [29] [30] [31] [32] LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143. LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144. LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152. LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164. LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172. [33] LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202. LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214. LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260. LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262. [34] LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277. [35] [36] Chapter 2. [37] LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380. [38] [39] LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516. LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517. [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58] Chapter 3. LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512. [59] [60] [61] LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724. [62] Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739 []\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut ed to Jan []ukasiewicz [63] [64] Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873 \OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz ation.''[] LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919. [65] LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932. LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973. [66] LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001. LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018. LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037. [67] [68] [69] [70] Overfull \hbox (23.8602pt too wide) in paragraph at lines 5320--5320 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarski's Overfull \hbox (33.01625pt too wide) in paragraph at lines 5400--5400 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxiliary [71] [72] [73] LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722. LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723. LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724. LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724. [74] [75] [76] LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986. LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988. LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989. [77] [78] [79] [80] [81] [82] [83] [84] [85] LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946. [86] [87] [88] Overfull \hbox (7.99037pt too wide) in paragraph at lines 7289--7289 []\OT1/cmr/bx/n/12 The Ax-ioms for Real and Com-plex Num-bers Them- [89] [90] [91] LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649. [92] [93] LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789. [94] [95] [96] [97] LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056. [98] LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093. LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109. [99] Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Ex- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Trans- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Ration- Underfull \hbox (badness 7379) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Ra- Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmtt/m/n/10 pm2.65da [100] [101] LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8338. [102] [103] [104] LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477. [105] [106] [107] [108] [109] [110] Chapter 4. LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768. [111] LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820. [112] [113] [114] [115] [116] [117] [118] [119] [120] [121] [122] [123] [124] LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777. [125] [126] [127] [128] [129] [130] [131] LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined (Font) using `OMS/cmtt/m/n' instead (Font) for symbol `textbraceleft' on input line 10257. [132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149] LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675. [150] LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686 . LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702. LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780. LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789. [151] LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824. [152] [153] [154] Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023 []\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases [155] [156] Chapter 5. [157] [158] [159] [160] [161] [162] [163] [164] [165] Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677 \OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m /n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1 0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth [166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] Appendix A. Underfull \hbox (badness 3780) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for Underfull \hbox (badness 4266) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion; [183] [184] [185] [186] Appendix B. [187] [188] Appendix C. LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141. LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155. LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172. [189] [190] [191] LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359. [192] [193] [194] LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580. LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581. [195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) LaTeX Warning: Citation `Tarski1965' on page 196 undefined on input line 14635. [196] [197] LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805. LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812. [198] LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896. [199] [200] [201] LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136. LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137. [202] [203] [204] [205] [206] Appendix D. [207] [208] LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417. [209] [210] Appendix E. [211] [212] [213] [214] No file metamath.bbl. (./metamath.ind) (./metamath.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. ) (see the transcript file for additional information) Output written on metamath.pdf (232 pages, 1043112 bytes). Transcript written on metamath.log. + bibtex metamath This is BibTeX, Version 0.99d (TeX Live 2019) The top-level auxiliary file: metamath.aux The style file: plain.bst Database file #1: metamath.bib Warning--empty journal in CarneiroND Warning--empty journal in Knill Warning--empty publisher in Clemente Warning--empty journal in Schmidt Warning--empty journal in Wiedijk-revisited (There were 5 warnings) + makeindex metamath.idx This is makeindex, version 2.15 [TeX Live 2019] (kpathsea + Thai support). Scanning input file metamath.idx.....done (1591 entries accepted, 0 rejected). Sorting entries................done (18500 comparisons). Generating output file metamath.ind.....done (930 lines written, 0 warnings). Output written in metamath.ind. Transcript written in metamath.ilg. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2018-12-01> LaTeX Warning: File `realref.sty' already exists on the system. Not generating it from this source. LaTeX Warning: File `metamath.bib' already exists on the system. Not generating it from this source. (/usr/share/texlive/texmf-dist/tex/latex/base/book.cls Document Class: book 2018/09/03 v1.4i Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo) (/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty) (/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty (/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym) (/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty (/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty document style option `anysize' loaded Michael Salzenberg, Thomas Esser, Dirk Hillbrecht Version 1.0, Aug 13, 1994 ) (./special-settings.sty) Writing index file metamath.idx (./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] (./metamath.toc [3] [4] LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 108. [5] [6]) [7] [8] [9] [10] LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on input line 1118. LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i nput line 1123. [11] [12] LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1220. [13] LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1245. [14] [15] [16] [17] [18] Chapter 1. LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428. [1] LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521. [2] [3] LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588. [4] LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625. LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631. [5] LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663. [6] [7] LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783. [8] [9] [10] [11] LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998. [12] [13] LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072. LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080. LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089. LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111. [14] LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140. LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156. LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164. LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169. [15] LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220. [16] LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254. LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254. LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256. LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258. LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275. LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288. LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288. [17] LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302. LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322. [18] [19] LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417. LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442. [20] LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477. LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489. [21] LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523. LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530. (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546. LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549. [22] LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566. LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577. LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587. LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591. LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593. LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604. LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605. [23] LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634. [24] LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26 79. LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688. LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698. LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703. LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713. [25] LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755. [26] LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783. LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792. LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800. LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831. [27] [28] LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 2910. LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932. [29] [30] [31] [32] LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143. LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144. LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152. LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164. LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172. [33] LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193. LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202. LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214. LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245. LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260. LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262. [34] LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277. [35] [36] Chapter 2. [37] LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379. LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380. [38] [39] LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516. LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517. [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58] Chapter 3. LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512. [59] [60] [61] LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724. [62] Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739 []\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut ed to Jan []ukasiewicz [63] [64] Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873 \OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz ation.''[] LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919. [65] LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932. LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973. [66] LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001. LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018. LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037. [67] [68] [69] [70] Overfull \hbox (23.8602pt too wide) in paragraph at lines 5320--5320 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarski's Overfull \hbox (33.01625pt too wide) in paragraph at lines 5400--5400 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxiliary [71] [72] [73] LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722. LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723. LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724. LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724. [74] [75] [76] LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986. LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988. LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989. [77] [78] [79] [80] [81] [82] [83] [84] [85] LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946. [86] [87] [88] Overfull \hbox (7.99037pt too wide) in paragraph at lines 7289--7289 []\OT1/cmr/bx/n/12 The Ax-ioms for Real and Com-plex Num-bers Them- [89] [90] [91] LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649. [92] [93] LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789. [94] [95] [96] [97] LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056. [98] LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093. LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109. [99] Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Ex- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Trans- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Ration- Underfull \hbox (badness 7379) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Ra- Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmtt/m/n/10 pm2.65da [100] [101] LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8338. [102] [103] [104] LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477. [105] [106] [107] [108] [109] [110] Chapter 4. LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768. [111] LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820. [112] [113] [114] [115] [116] [117] [118] [119] [120] [121] [122] [123] [124] LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770. LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777. [125] [126] [127] [128] [129] [130] [131] LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined (Font) using `OMS/cmtt/m/n' instead (Font) for symbol `textbraceleft' on input line 10257. [132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149] LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675. [150] LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686 . LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702. LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780. LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789. [151] LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824. [152] [153] [154] Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023 []\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases [155] [156] Chapter 5. [157] [158] [159] [160] [161] [162] [163] [164] [165] Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677 \OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m /n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1 0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth [166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] Appendix A. Underfull \hbox (badness 3780) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for Underfull \hbox (badness 4266) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion; [183] [184] [185] [186] Appendix B. [187] [188] Appendix C. LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141. LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155. LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172. [189] [190] [191] LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359. [192] [193] [194] LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580. LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581. [195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) LaTeX Warning: Citation `Tarski1965' on page 196 undefined on input line 14635. [196] [197] LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805. LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812. [198] LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885. LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896. [199] [200] [201] LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136. LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137. [202] [203] [204] [205] [206] Appendix D. [207] [208] LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417. [209] [210] Appendix E. [211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220] (./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229]) (./metamath.aux) Package rerunfilecheck Warning: File `metamath.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Font Warning: Some font shapes were not available, defaults substituted. LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. ) (see the transcript file for additional information) Output written on metamath.pdf (247 pages, 1124291 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2018-12-01> LaTeX Warning: File `realref.sty' already exists on the system. Not generating it from this source. LaTeX Warning: File `metamath.bib' already exists on the system. Not generating it from this source. (/usr/share/texlive/texmf-dist/tex/latex/base/book.cls Document Class: book 2018/09/03 v1.4i Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo) (/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty) (/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty (/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym) (/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty (/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty document style option `anysize' loaded Michael Salzenberg, Thomas Esser, Dirk Hillbrecht Version 1.0, Aug 13, 1994 ) (./special-settings.sty) Writing index file metamath.idx (./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] (./metamath.toc [3] [4] LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 108. [5] [6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] Chapter 1. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20] [21] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36] Chapter 2. [37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58] Chapter 3. [59] [60] [61] [62] Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739 []\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut ed to Jan []ukasiewicz [63] [64] Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873 \OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz ation.''[] [65] [66] [67] [68] [69] [70] Overfull \hbox (23.8602pt too wide) in paragraph at lines 5320--5320 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarski's Overfull \hbox (33.01625pt too wide) in paragraph at lines 5400--5400 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxiliary [71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82] [83] [84] [85] [86] [87] [88] Overfull \hbox (7.99037pt too wide) in paragraph at lines 7289--7289 []\OT1/cmr/bx/n/12 The Ax-ioms for Real and Com-plex Num-bers Them- [89] [90] [91] [92] [93] [94] [95] [96] [97] [98] [99] Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Ex- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Trans- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Ration- Underfull \hbox (badness 7379) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Ra- Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmtt/m/n/10 pm2.65da [100] [101] [102] [103] [104] [105] [106] [107] [108] [109] [110] Chapter 4. [111] [112] [113] [114] [115] [116] [117] [118] [119] [120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130] [131] LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined (Font) using `OMS/cmtt/m/n' instead (Font) for symbol `textbraceleft' on input line 10257. [132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151] [152] [153] [154] Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023 []\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases [155] [156] Chapter 5. [157] [158] [159] [160] [161] [162] [163] [164] [165] Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677 \OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m /n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1 0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth [166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] Appendix A. Underfull \hbox (badness 3780) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for Underfull \hbox (badness 4266) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion; [183] [184] [185] [186] Appendix B. [187] [188] Appendix C. [189] [190] [191] [192] [193] [194] [195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [196] [197] [198] [199] [200] [201] [202] [203] [204] [205] [206] Appendix D. [207] [208] [209] [210] Appendix E. [211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220] (./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229]) (./metamath.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. ) (see the transcript file for additional information) Output written on metamath.pdf (247 pages, 1121711 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2018-12-01> LaTeX Warning: File `realref.sty' already exists on the system. Not generating it from this source. LaTeX Warning: File `metamath.bib' already exists on the system. Not generating it from this source. (/usr/share/texlive/texmf-dist/tex/latex/base/book.cls Document Class: book 2018/09/03 v1.4i Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo) (/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty) (/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty (/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym) (/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty (/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty document style option `anysize' loaded Michael Salzenberg, Thomas Esser, Dirk Hillbrecht Version 1.0, Aug 13, 1994 ) (./special-settings.sty) Writing index file metamath.idx (./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] (./metamath.toc [3] [4] LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 108. [5] [6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] Chapter 1. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20] [21] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36] Chapter 2. [37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58] Chapter 3. [59] [60] [61] [62] Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739 []\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut ed to Jan []ukasiewicz [63] [64] Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873 \OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz ation.''[] [65] [66] [67] [68] [69] [70] Overfull \hbox (23.8602pt too wide) in paragraph at lines 5320--5320 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarski's Overfull \hbox (33.01625pt too wide) in paragraph at lines 5400--5400 []\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxiliary [71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82] [83] [84] [85] [86] [87] [88] Overfull \hbox (7.99037pt too wide) in paragraph at lines 7289--7289 []\OT1/cmr/bx/n/12 The Ax-ioms for Real and Com-plex Num-bers Them- [89] [90] [91] [92] [93] [94] [95] [96] [97] [98] [99] Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Ex- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Trans- Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 ND Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 \OT1/cmr/bx/n/10 Ration- Underfull \hbox (badness 7379) in paragraph at lines 8177--8177 []\OT1/cmr/bx/n/10 MPE Ra- Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2478) in paragraph at lines 8177--8177 []\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 10000) in paragraph at lines 8177--8177 []\OT1/cmtt/m/n/10 pm2.65da [100] [101] [102] [103] [104] [105] [106] [107] [108] [109] [110] Chapter 4. [111] [112] [113] [114] [115] [116] [117] [118] [119] [120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130] [131] LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined (Font) using `OMS/cmtt/m/n' instead (Font) for symbol `textbraceleft' on input line 10257. [132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151] [152] [153] [154] Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023 []\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases [155] [156] Chapter 5. [157] [158] [159] [160] [161] [162] [163] [164] [165] Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677 \OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m /n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1 0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth [166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] Appendix A. Underfull \hbox (badness 3780) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for Underfull \hbox (badness 4266) in paragraph at lines 13874--13874 []\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion; [183] [184] [185] [186] Appendix B. [187] [188] Appendix C. [189] [190] [191] [192] [193] [194] [195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [196] [197] [198] [199] [200] [201] [202] [203] [204] [205] [206] Appendix D. [207] [208] [209] [210] Appendix E. [211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220] (./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229]) (./metamath.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. ) (see the transcript file for additional information) Output written on metamath.pdf (247 pages, 1121711 bytes). Transcript written on metamath.log. + RPM_EC=0 ++ jobs -p + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.w5RvNo + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 ++ dirname /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 + cd metamath + /usr/bin/make install DESTDIR=/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 'INSTALL=/usr/bin/install -p' make[1]: Entering directory '/builddir/build/BUILD/metamath' /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/bin' /usr/bin/install -p metamath '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/bin' /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/metamath' /usr/bin/install -p -m 644 big-unifier.mm demo0.mm miu.mm peano.mm ql.mm set.mm '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/metamath' /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/man/man1' /usr/bin/install -p -m 644 metamath.1 '/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/man/man1' make[1]: Leaving directory '/builddir/build/BUILD/metamath' + cp -p big-unifier.mm demo0.mm hol.mm iset.mm miu.mm nf.mm peano.mm ql.mm set.mm /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/metamath + mkdir -p /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/doc/metamath + cp -p metamath.pdf /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/doc/metamath + /usr/lib/rpm/find-debuginfo.sh -j4 --strict-build-id -m -i --build-id-seed 0.181-1.fc33 --unique-debug-suffix -0.181-1.fc33.riscv64 --unique-debug-src-base metamath-0.181-1.fc33.riscv64 --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 -S debugsourcefiles.list /builddir/build/BUILD/metamath explicitly decompress any DWARF compressed ELF sections in /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/bin/metamath extracting debug info from /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/bin/metamath original debug info size: 1372kB, size after compression: 1316kB /usr/lib/rpm/sepdebugcrcfix: Updated 1 CRC32s, 0 CRC32s did match. 3619 blocks + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-ldconfig + /usr/lib/rpm/brp-compress + /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip + /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/redhat/brp-python-bytecompile /usr/bin/python 1 0 + /usr/lib/rpm/brp-python-hardlink + /usr/lib/rpm/redhat/brp-mangle-shebangs Processing files: metamath-0.181-1.fc33.riscv64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.njPfFo + umask 022 + cd /builddir/build/BUILD + cd metamath + DOCDIR=/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/doc/metamath + export LC_ALL=C + LC_ALL=C + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/doc/metamath + cp -pr README.TXT /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/doc/metamath + RPM_EC=0 ++ jobs -p + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.3jtmlq + umask 022 + cd /builddir/build/BUILD + cd metamath + LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath + export LC_ALL=C + LC_ALL=C + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath + cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath + RPM_EC=0 ++ jobs -p + exit 0 Provides: metamath = 0.181-1.fc33 metamath(riscv-64) = 0.181-1.fc33 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Requires: ld-linux-riscv64-lp64d.so.1()(64bit) ld-linux-riscv64-lp64d.so.1(GLIBC_2.27)(64bit) libc.so.6()(64bit) libc.so.6(GLIBC_2.27)(64bit) rtld(GNU_HASH) Suggests: rlwrap Processing files: metamath-theories-0.181-1.fc33.noarch Provides: metamath-theories = 0.181-1.fc33 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: metamath-doc-0.181-1.fc33.noarch Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.RIMW3p + umask 022 + cd /builddir/build/BUILD + cd metamath + LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath-doc + export LC_ALL=C + LC_ALL=C + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath-doc + cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64/usr/share/licenses/metamath-doc + RPM_EC=0 ++ jobs -p + exit 0 Provides: metamath-doc = 0.181-1.fc33 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: metamath-debugsource-0.181-1.fc33.riscv64 Provides: metamath-debugsource = 0.181-1.fc33 metamath-debugsource(riscv-64) = 0.181-1.fc33 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: metamath-debuginfo-0.181-1.fc33.riscv64 Provides: debuginfo(build-id) = bf598058dfc1b47af11afc7df003612fdcb2c895 metamath-debuginfo = 0.181-1.fc33 metamath-debuginfo(riscv-64) = 0.181-1.fc33 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Recommends: metamath-debugsource(riscv-64) = 0.181-1.fc33 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 Wrote: /builddir/build/RPMS/metamath-doc-0.181-1.fc33.noarch.rpm Wrote: /builddir/build/RPMS/metamath-0.181-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-debuginfo-0.181-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-debugsource-0.181-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-theories-0.181-1.fc33.noarch.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.iwx4uq + umask 022 + cd /builddir/build/BUILD + cd metamath + /usr/bin/rm -rf /builddir/build/BUILDROOT/metamath-0.181-1.fc33.riscv64 + RPM_EC=0 ++ jobs -p + exit 0 Child return code was: 0