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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3fd27cd700>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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'en_US.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3fd27cd700>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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\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/cmbx10.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texliv
e/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf
-dist/fonts/type1/public/amsfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texliv
e/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
m/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti1
0.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/t
exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf
-dist/fonts/type1/public/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/cm-super/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/cm-super/sftt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/cm-super/sftt1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-su
per/sftt1200.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/fo
nts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
ex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmitt10.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy1
0.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-s
uper/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sf
rm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt0800.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.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/fo
nts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
ex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmitt10.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy1
0.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-s
uper/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sf
rm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt0800.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.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/fo
nts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
m/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-s
uper/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sf
tt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.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/fo
nts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
m/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-s
uper/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sf
tt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.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