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-344961-59228/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=1600300800 Wrote: /builddir/build/SRPMS/metamath-0.193-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-344961-59228/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=1600300800 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.sV6Qdq + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf metamath + /usr/bin/bzip2 -dc /builddir/build/SOURCES/metamath.tar.bz2 + /usr/bin/tar -xof - + 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.0WxmJp + umask 022 + cd /builddir/build/BUILD + cd metamath + CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection' + export CFLAGS + CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection' + export CXXFLAGS + FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules' + export FFLAGS + FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 + CC=gcc + export CC + CXX=g++ + export CXX + '[' '-flto=auto -ffat-lto-objectsx' '!=' x ']' ++ find . -type f -name configure -print + for file in $(find . -type f -name configure -print) + /usr/bin/sed -r --in-place=.backup 's/^char \(\*f\) \(\) = /__attribute__ ((used)) char (*f) () = /g' ./configure + diff -u ./configure.backup ./configure + mv ./configure.backup ./configure + /usr/bin/sed -r --in-place=.backup 's/^char \(\*f\) \(\);/__attribute__ ((used)) char (*f) ();/g' ./configure + diff -u ./configure.backup ./configure + mv ./configure.backup ./configure + /usr/bin/sed -r --in-place=.backup 's/^char \$2 \(\);/__attribute__ ((used)) char \$2 ();/g' ./configure + diff -u ./configure.backup ./configure --- ./configure.backup 2020-11-27 13:02:14.945151568 -0500 +++ ./configure 2020-11-27 13:03:01.095152362 -0500 @@ -1813,7 +1813,7 @@ #ifdef __cplusplus extern "C" #endif -char $2 (); +__attribute__ ((used)) char $2 (); /* The GNU C library defines this for functions which it implements to always fail with ENOSYS. Some functions are actually named something starting with __ and the normal name is an alias. */ + /usr/bin/sed --in-place=.backup '1{$!N;$!N};$!N;s/int x = 1;\nint y = 0;\nint z;\nint nan;/volatile int x = 1; volatile int y = 0; volatile int z, nan;/;P;D' ./configure + diff -u ./configure.backup ./configure + mv ./configure.backup ./configure + /usr/bin/sed --in-place=.backup 's#^lt_cv_sys_global_symbol_to_cdecl=.*#lt_cv_sys_global_symbol_to_cdecl="sed -n -e '\''s/^T .* \\(.*\\)$/extern int \\1();/p'\'' -e '\''s/^$symcode* .* \\(.*\\)$/extern char \\1;/p'\''"#' ./configure + diff -u ./configure.backup ./configure + mv ./configure.backup ./configure + '[' 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 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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... 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 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 + /usr/bin/make -O -j4 V=1 VERBOSE=1 /usr/bin/make all-am make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' mmdata.c: In function 'getContrib': mmdata.c:3579:45: warning: comparison is always false due to limited range of data type [-Wtype-limits] 3579 | (vstring)(reviseDateList[stmtNum])) == -1) { | ^~ mmdata.c:3584:46: warning: comparison is always false due to limited range of data type [-Wtype-limits] 3584 | (vstring)(shortenDateList[stmtNum])) == -1) { | ^~ mmdata.c:3830:51: warning: comparison is always true due to limited range of data type [-Wtype-limits] 3830 | && compareDates(contribDate, reviseDate) != -1) | ^~ mmdata.c:3832:52: warning: comparison is always true due to limited range of data type [-Wtype-limits] 3832 | && compareDates(contribDate, shortenDate) != -1))) { | ^~ make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' mmcmds.c: In function 'verifyMarkup': mmcmds.c:5843:46: warning: comparison is always false due to limited range of data type [-Wtype-limits] 5843 | if (compareDates(mostRecentDate, str1) == -1) { | ^~ make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' metamath.c: In function 'command': metamath.c:1135:15: warning: ignoring return value of 'system' declared with attribute 'warn_unused_result' [-Wunused-result] 1135 | (void)system(str1); | ^~~~~~~~~~~~ make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DHAVE_CONFIG_H -I. -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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 make[1]: Leaving directory '/builddir/build/BUILD/metamath' mmwtex.c: In function 'printTexComment': mmwtex.c:2133:18: warning: comparison is always false due to limited range of data type [-Wtype-limits] 2133 | if (mode == -1) { /* Math mode */ | ^~ make[1]: Entering directory '/builddir/build/BUILD/metamath' gcc -DINLINE=inline -O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -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.21 (TeX Live 2020) (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/.texlive2020/texmf-config/web2c/fmtutil.cnf mktexfmt [INFO]: writing formats under /builddir/.texlive2020/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.21 (TeX Live 2020) (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 <2020-02-02> patch level 5 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/omsenc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd) (/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/omsenc.dfu) (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu) (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu)) (/usr/share/texlive/texmf-dist/tex/latex/base/ltexpl.ltx (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.ltx (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3deprecation.def)))) ) ) Beginning to dump on file pdflatex.fmt (preloaded format=pdflatex 2020.11.27) 17445 strings of total length 297856 233798 memory locations dumped; current usage is 165&226831 15747 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 \font\c__fp_exp_intarray=cmr10 at 0.00002pt \font\c__fp_trig_intarray=cmr10 at 0.00003pt \font\g__regex_charcode_intarray=cmr10 at 0.00005pt \font\g__regex_catcode_intarray=cmr10 at 0.00006pt \font\g__regex_balance_intarray=cmr10 at 0.00008pt \font\g__regex_state_active_intarray=cmr10 at 0.00009pt \font\g__regex_thread_state_intarray=cmr10 at 0.0001pt \font\g__regex_submatch_prev_intarray=cmr10 at 0.00012pt \font\g__regex_submatch_begin_intarray=cmr10 at 0.00014pt \font\g__regex_submatch_end_intarray=cmr10 at 0.00015pt 532331 words of font info for 24 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]: log file copied to: /builddir/.texlive2020/texmf-var/web2c/pdftex/pdflatex.log mktexfmt [INFO]: /builddir/.texlive2020/texmf-var/web2c/pdftex/pdflatex.fmt installed. mktexfmt [INFO]: successfully rebuilt formats: 1 mktexfmt [INFO]: not selected formats: 20 mktexfmt [INFO]: total formats: 21 mktexfmt [INFO]: exiting with status 0 entering extended mode (./metamath.tex LaTeX2e <2020-02-02> patch level 5 L3 programming layer <2020-04-06> 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 2019/12/20 v1.4l 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/ltxcmds/ltxcmds.sty) (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty) (/usr/share/texlive/texmf-dist/tex/latex/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/generic/atbegshi/atbegshi.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/atveryend/atveryend.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.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/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.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/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/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] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) [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. 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] Package amsmath Warning: Foreign command \atop; (amsmath) \frac or \genfrac should be used instead (amsmath) on input line 6661. [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 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\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] LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined (Font) using `TS1/cmtt/m/n' instead (Font) for symbol `textdollar' on input line 9416. [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/enc/dvips/cm-super/cm-super-ts1.enc}< /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb> Output written on metamath.pdf (228 pages, 1041311 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2020-02-02> patch level 5 L3 programming layer <2020-04-06> 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 2019/12/20 v1.4l 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/ltxcmds/ltxcmds.sty) (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty) (/usr/share/texlive/texmf-dist/tex/latex/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/generic/atbegshi/atbegshi.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/atveryend/atveryend.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.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/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.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/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/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] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) 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. 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/cmtt/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] Package amsmath Warning: Foreign command \atop; (amsmath) \frac or \genfrac should be used instead (amsmath) on input line 6661. [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 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\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] LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined (Font) using `TS1/cmtt/m/n' instead (Font) for symbol `textdollar' on input line 9416. [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){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}< /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb> Output written on metamath.pdf (232 pages, 1065583 bytes). Transcript written on metamath.log. + bibtex metamath This is BibTeX, Version 0.99d (TeX Live 2020) 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 2020] (kpathsea + Thai support). Scanning input file metamath.idx.....done (1591 entries accepted, 0 rejected). Sorting entries................done (18502 comparisons). Generating output file metamath.ind.....done (929 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.21 (TeX Live 2020) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2020-02-02> patch level 5 L3 programming layer <2020-04-06> 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 2019/12/20 v1.4l 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/ltxcmds/ltxcmds.sty) (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty) (/usr/share/texlive/texmf-dist/tex/latex/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/generic/atbegshi/atbegshi.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/atveryend/atveryend.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.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/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.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/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/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] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) 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. 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/cmtt/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] Package amsmath Warning: Foreign command \atop; (amsmath) \frac or \genfrac should be used instead (amsmath) on input line 6661. [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 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\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] LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined (Font) using `TS1/cmtt/m/n' instead (Font) for symbol `textdollar' on input line 9416. [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){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}< /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb> Output written on metamath.pdf (247 pages, 1146683 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2020-02-02> patch level 5 L3 programming layer <2020-04-06> 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 2019/12/20 v1.4l 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/ltxcmds/ltxcmds.sty) (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty) (/usr/share/texlive/texmf-dist/tex/latex/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/generic/atbegshi/atbegshi.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/atveryend/atveryend.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.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/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.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/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/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] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) 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] [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/cmtt/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] Package amsmath Warning: Foreign command \atop; (amsmath) \frac or \genfrac should be used instead (amsmath) on input line 6661. [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 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\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] LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined (Font) using `TS1/cmtt/m/n' instead (Font) for symbol `textdollar' on input line 9416. [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){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}< /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb> Output written on metamath.pdf (247 pages, 1144480 bytes). Transcript written on metamath.log. + pdflatex metamath This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./metamath.tex LaTeX2e <2020-02-02> patch level 5 L3 programming layer <2020-04-06> 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 2019/12/20 v1.4l 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/ltxcmds/ltxcmds.sty) (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty) (/usr/share/texlive/texmf-dist/tex/latex/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/generic/atbegshi/atbegshi.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/atveryend/atveryend.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.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/l3backend/l3backend-pdfmode.def)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.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/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (./metamath.out) (./metamath.out) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/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] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) 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] [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/cmtt/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] Package amsmath Warning: Foreign command \atop; (amsmath) \frac or \genfrac should be used instead (amsmath) on input line 6661. [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 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr Underfull \hbox (badness 2582) in paragraph at lines 8177--8177 []\TS1/cmr/m/n/10 $\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] LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined (Font) using `TS1/cmtt/m/n' instead (Font) for symbol `textdollar' on input line 9416. [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){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}< /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb> Output written on metamath.pdf (247 pages, 1144480 bytes). Transcript written on metamath.log. + RPM_EC=0 ++ jobs -p + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.yhFUJn + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 ++ dirname /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 + cd metamath + /usr/bin/make install DESTDIR=/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/bin' /usr/bin/install -p metamath '/builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/bin' /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/share/metamath' /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/man/man1' /usr/bin/install -p -m 644 metamath.1 '/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/share/metamath + mkdir -p /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/doc/metamath + cp -p metamath.pdf /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/doc/metamath + /usr/lib/rpm/find-debuginfo.sh -j4 --strict-build-id -m -i --build-id-seed 0.193-1.fc33 --unique-debug-suffix -0.193-1.fc33.riscv64 --unique-debug-src-base metamath-0.193-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.193-1.fc33.riscv64/usr/bin/metamath extracting debug info from /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/bin/metamath original debug info size: 4684kB, size after compression: 4612kB /usr/lib/rpm/sepdebugcrcfix: Updated 1 CRC32s, 0 CRC32s did match. 3798 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 '' 1 0 + /usr/lib/rpm/brp-python-hardlink + /usr/lib/rpm/redhat/brp-mangle-shebangs Processing files: metamath-0.193-1.fc33.riscv64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.ZEcIbp + umask 022 + cd /builddir/build/BUILD + cd metamath + DOCDIR=/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/share/doc/metamath + cp -pr README.TXT /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/doc/metamath + RPM_EC=0 ++ jobs -p + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.vWvAjq + umask 022 + cd /builddir/build/BUILD + cd metamath + LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/share/licenses/metamath + cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/licenses/metamath + RPM_EC=0 ++ jobs -p + exit 0 Provides: metamath = 0.193-1.fc33 metamath(riscv-64) = 0.193-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.193-1.fc33.noarch Provides: metamath-theories = 0.193-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.193-1.fc33.noarch Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.UM7hpp + umask 022 + cd /builddir/build/BUILD + cd metamath + LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.193-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.193-1.fc33.riscv64/usr/share/licenses/metamath-doc + cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64/usr/share/licenses/metamath-doc + RPM_EC=0 ++ jobs -p + exit 0 Provides: metamath-doc = 0.193-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.193-1.fc33.riscv64 Provides: metamath-debugsource = 0.193-1.fc33 metamath-debugsource(riscv-64) = 0.193-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.193-1.fc33.riscv64 Provides: debuginfo(build-id) = a7c9d8ce7e41a3d0de4665e5ead5bf489465a3d4 metamath-debuginfo = 0.193-1.fc33 metamath-debuginfo(riscv-64) = 0.193-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.193-1.fc33 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 Wrote: /builddir/build/RPMS/metamath-doc-0.193-1.fc33.noarch.rpm Wrote: /builddir/build/RPMS/metamath-0.193-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-debuginfo-0.193-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-debugsource-0.193-1.fc33.riscv64.rpm Wrote: /builddir/build/RPMS/metamath-theories-0.193-1.fc33.noarch.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.r4eWdp + umask 022 + cd /builddir/build/BUILD + cd metamath + /usr/bin/rm -rf /builddir/build/BUILDROOT/metamath-0.193-1.fc33.riscv64 + RPM_EC=0 ++ jobs -p + exit 0 Child return code was: 0