Mock Version: 1.4.14
Mock Version: 1.4.14
ENTER ['do'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f31-build-86884-31706/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 0x15580c1cf8>timeout=345600uid=986gid=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=1564012800
Wrote: /builddir/build/SRPMS/metamath-0.177-2.fc31.src.rpm
Child return code was: 0
ENTER ['do'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f31-build-86884-31706/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 0x15580c1cf8>timeout=345600uid=986gid=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=1564012800
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.zFwop9
+ umask 022
+ cd /builddir/build/BUILD
+ cd /builddir/build/BUILD
+ rm -rf metamath
+ /usr/bin/tar -xof -
+ /usr/bin/bzip2 -dc /builddir/build/SOURCES/metamath.tar.bz2
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd metamath
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ cp -p /builddir/build/SOURCES/metamath.tex .
+ touch special-settings.sty
+ rm metamath.exe
+ sed -i '/Try to optimize/,/^$/d' configure.ac
+ autoreconf -fi
BUILDSTDERR: configure.ac:13: installing './compile'
BUILDSTDERR: configure.ac:9: installing './install-sh'
BUILDSTDERR: configure.ac:9: installing './missing'
BUILDSTDERR: Makefile.am: installing './depcomp'
+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.KIHwya
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ CFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CFLAGS
+ CXXFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CXXFLAGS
+ FFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FFLAGS
+ FCFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FCFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld'
+ export LDFLAGS
+ '[' 1 = 1 ']'
BUILDSTDERR: +++ dirname ./configure
BUILDSTDERR: ++ find . -name config.guess -o -name config.sub
+ '[' 1 = 1 ']'
+ '[' x '!=' 'x-Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld' ']'
BUILDSTDERR: ++ find . -name ltmain.sh
+ ./configure --build=riscv64-koji-linux-gnu --host=riscv64-koji-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info 'CFLAGS=-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv'
+ make -j4
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-koji-linux-gnu-gcc... no
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking whether gcc understands -c and -o together... yes
checking whether make supports the include directive... yes (GNU style)
checking dependency style of gcc... none
checking how to run the C preprocessor... gcc -E
checking for grep that handles long lines and -e... /usr/bin/grep
checking for egrep... /usr/bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking limits.h usability... yes
checking limits.h presence... yes
checking for limits.h... yes
checking for stdlib.h... (cached) yes
checking for string.h... (cached) yes
checking for stdbool.h that conforms to C99... yes
checking for _Bool... yes
checking for size_t... yes
checking for stdlib.h... (cached) yes
checking for GNU libc compatible malloc... yes
checking for stdlib.h... (cached) yes
checking for GNU libc compatible realloc... yes
checking for strchr... yes
checking for strcspn... yes
checking for strstr... yes
checking for gcc warning flags... yes
checking for 'inline' support... yes
CFLAGS=-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra
checking that generated files are newer than configure... done
configure: creating ./config.status
config.status: creating Makefile
config.status: creating config.h
config.status: executing depfiles commands
make  all-am
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o metamath.o metamath.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmdl.o mmcmdl.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmds.o mmcmds.c
BUILDSTDERR: gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhmmdata.c: In function 'getContrib':
BUILDSTDERR: mmdata.c:3431:45: warning: comparison is always false due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  3431 |         (vstring)(reviseDateList[stmtNum])) == -1) {
BUILDSTDERR:       |                                             ^~
BUILDSTDERR: mmdata.c:3436:46: warning: comparison is always false due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  3436 |         (vstring)(shortenDateList[stmtNum])) == -1) {
BUILDSTDERR:       |                                              ^~
BUILDSTDERR: mmdata.c:3682:51: warning: comparison is always true due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  3682 |          && compareDates(contribDate, reviseDate) != -1)
BUILDSTDERR:       |                                                   ^~
BUILDSTDERR: mmdata.c:3684:52: warning: comparison is always true due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  3684 |          && compareDates(contribDate, shortenDate) != -1))) {
BUILDSTDERR:       |                                                    ^~
BUILDSTDERR: mmcmds.c: In function 'verifyMarkup':
BUILDSTDERR: mmcmds.c:4990:46: warning: comparison is always false due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  4990 |       if (compareDates(mostRecentDate, str1) == -1) {
BUILDSTDERR:       |                                              ^~
BUILDSTDERR: metamath.c: In function 'command':
BUILDSTDERR: metamath.c:1054:15: warning: ignoring return value of 'system', declared with attribute warn_unused_result [-Wunused-result]
BUILDSTDERR:  1054 |         (void)system(str1);
BUILDSTDERR:       |               ^~~~~~~~~~~~
at/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmdata.o mmdata.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpa.o mmhlpa.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpb.o mmhlpb.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mminou.o mminou.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmmaci.o mmmaci.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpars.o mmpars.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpfas.o mmpfas.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmunif.o mmunif.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmutil.o mmutil.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmveri.o mmveri.c
BUILDSTDERR: gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tammwtex.c: In function 'printTexComment':
BUILDSTDERR: mmwtex.c:2105:18: warning: comparison is always false due to limited range of data type [-Wtype-limits]
BUILDSTDERR:  2105 |         if (mode == -1) { /* Math mode */
BUILDSTDERR:       |                  ^~
+ touch metamath.ind
+ pdflatex metamath
BUILDSTDERR: kpathsea: Running mktexfmt pdflatex.fmt
BUILDSTDERR: mktexfmt: mktexfmt is using the following fmtutil.cnf files (in precedence order):
BUILDSTDERR: mktexfmt:   /usr/share/texlive/texmf-dist/web2c/fmtutil.cnf
BUILDSTDERR: mktexfmt: mktexfmt is using the following fmtutil.cnf file for writing changes:
BUILDSTDERR: mktexfmt:   /builddir/.texlive2018/texmf-config/web2c/fmtutil.cnf
BUILDSTDERR: mktexfmt [INFO]: writing formats under /builddir/.texlive2018/texmf-var/web2c
BUILDSTDERR: mktexfmt [INFO]: --- remaking pdflatex with pdftex
BUILDSTDERR: mktexfmt: running `pdftex -ini   -jobname=pdflatex -progname=pdflatex -translate-file=cp227.tcx *pdflatex.ini' ...
BUILDSTDERR: This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (INITEX)
BUILDSTDERR:  restricted \write18 enabled.
BUILDSTDERR:  (/usr/share/texlive/texmf-dist/web2c/cp227.tcx)
BUILDSTDERR: entering extended mode
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/pdflatex.ini
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/tex-ini-files/pdftexconfig.tex)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/latex.ltx
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/texsys.cfg)
BUILDSTDERR: ./texsys.aux found
BUILDSTDERR: \@currdir set to: ./.
BUILDSTDERR: Assuming \openin and \input 
BUILDSTDERR: have the same search path.
BUILDSTDERR: Defining UNIX/DOS style filename parser.
BUILDSTDERR: catcodes, registers, parameters,
BUILDSTDERR: LaTeX2e <2018-04-01> patch level 5
BUILDSTDERR: hacks, control, par, spacing, files, font encodings, lengths,
BUILDSTDERR: ====================================
BUILDSTDERR: Local config file fonttext.cfg used
BUILDSTDERR: ====================================
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/fonttext.cfg
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/fonttext.ltx
BUILDSTDERR: === Don't modify this file, use a .cfg file instead ===
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omlenc.def)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.def)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.def)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.def)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/t1cmr.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmr.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmss.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ot1cmtt.fd)))
BUILDSTDERR: ====================================
BUILDSTDERR: Local config file fontmath.cfg used
BUILDSTDERR: ====================================
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/fontmath.cfg
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/fontmath.ltx
BUILDSTDERR: === Don't modify this file, use a .cfg file instead ===
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omlcmm.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omscmsy.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omxcmex.fd)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ucmr.fd)))
BUILDSTDERR: ====================================
BUILDSTDERR: Local config file preload.cfg used
BUILDSTDERR: =====================================
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/preload.cfg
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/preload.ltx)) page nos., x-ref,
BUILDSTDERR: environments, center, verbatim, math definitions, boxes, title, sectioning,
BUILDSTDERR: contents, floats, footnotes, index, bibliography, output,
BUILDSTDERR: ===========================================
BUILDSTDERR: Local configuration file hyphen.cfg used
BUILDSTDERR: ===========================================
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/babel/hyphen.cfg
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/babel/switch.def)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/hyphen/hyphen.tex)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/hyphen/dumyhyph.tex)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/generic/hyphen/zerohyph.tex))
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
BUILDSTDERR: (/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))
BUILDSTDERR:  ) )
BUILDSTDERR: Beginning to dump on file pdflatex.fmt
BUILDSTDERR:  (preloaded format=pdflatex 2019.8.10)
BUILDSTDERR: 5413 strings of total length 72241
BUILDSTDERR: 50531 memory locations dumped; current usage is 144&50357
BUILDSTDERR: 3741 multiletter control sequences
BUILDSTDERR: \font\nullfont=nullfont
BUILDSTDERR: \font\OMX/cmex/m/n/10=cmex10
BUILDSTDERR: \font\tenln=line10
BUILDSTDERR: \font\tenlnw=linew10
BUILDSTDERR: \font\tencirc=lcircle10
BUILDSTDERR: \font\tencircw=lcirclew10
BUILDSTDERR: \font\OT1/cmr/m/n/5=cmr5
BUILDSTDERR: \font\OT1/cmr/m/n/7=cmr7
BUILDSTDERR: \font\OT1/cmr/m/n/10=cmr10
BUILDSTDERR: \font\OML/cmm/m/it/5=cmmi5
BUILDSTDERR: \font\OML/cmm/m/it/7=cmmi7
BUILDSTDERR: \font\OML/cmm/m/it/10=cmmi10
BUILDSTDERR: \font\OMS/cmsy/m/n/5=cmsy5
BUILDSTDERR: \font\OMS/cmsy/m/n/7=cmsy7
BUILDSTDERR: \font\OMS/cmsy/m/n/10=cmsy10
BUILDSTDERR: 3633 words of font info for 14 preloaded fonts
BUILDSTDERR: 14 hyphenation exceptions
BUILDSTDERR: Hyphenation trie of length 6081 has 183 ops out of 35111
BUILDSTDERR:   2 for language 1
BUILDSTDERR:   181 for language 0
BUILDSTDERR: 0 words of pdfTeX memory
BUILDSTDERR: 0 indirect objects
BUILDSTDERR: No pages of output.
BUILDSTDERR: Transcript written on pdflatex.log.
BUILDSTDERR: mktexfmt [INFO]: /builddir/.texlive2018/texmf-var/web2c/pdftex/pdflatex.fmt installed.
BUILDSTDERR: mktexfmt [INFO]: Successfully rebuilt formats: 1
BUILDSTDERR: mktexfmt [INFO]: Not selected formats: 13
BUILDSTDERR: mktexfmt [INFO]: Total formats: 14
BUILDSTDERR: mktexfmt [INFO]: exiting with status 0
bles -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmvstr.o mmvstr.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmword.o mmword.c
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmwtex.o mmwtex.c
gcc -DINLINE=inline -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fstack-clash-protection -DINLINE=inline -fwrapv -Wall -Wextra  -Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -o metamath metamath.o mmcmdl.o mmcmds.o mmdata.o mmhlpa.o mmhlpb.o mminou.o mmmaci.o mmpars.o mmpfas.o mmunif.o mmutil.o mmveri.o mmvstr.o mmword.o mmwtex.o   
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2018-04-01> patch level 5
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 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex)
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
No file metamath.aux.
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te
xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2] [3] [4]
[5] [6]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page vii undefined o
n input line 1112.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page vii undefined on 
input line 1117.
[7] [8]
LaTeX Warning: Citation `Barrow' on page ix undefined on input line 1214.
[9]
LaTeX Warning: Citation `Davis' on page x undefined on input line 1239.
[10] [11] [12] [13] [14]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1414.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1507.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1574.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1611.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1617.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1649.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1769.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1988.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2062.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2070.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2079.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2101.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2129.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2145.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2152.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2157.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2205.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2241.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2243.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2260.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2273.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2273.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2287.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2307.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2402.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2427.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2461.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2473.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2507.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2514.
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2533.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2546.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2550.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2561.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2571.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2575.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2588.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2589.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2618.
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 2647.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
63.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2672.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2682.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2687.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2697.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2739.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2767.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2776.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2784.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2815.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2894.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2916.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3127.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3128.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3136.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3148.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3156.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3186.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3198.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3244.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3246.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3261.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3360.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3363.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3364.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3500.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3501.
[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 4489.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4701.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4712--4716
[]\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 4845--4850
\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 4896.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4909.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4950.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4978.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4995.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5014.
[67] [68] [69] [70]
Overfull \hbox (18.1588pt too wide) in paragraph at lines 5297--5297
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with equal-ity - Tarski's
Overfull \hbox (2.30984pt too wide) in paragraph at lines 5377--5377
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equal-ity - Aux-
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5697.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5698.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5699.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5699.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5952.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5954.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5955.
[77] [78] [79] [80] [81] [82] [83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6909.
[86] [87] [88] [89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7596.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7736.
[94] [95]
Overfull \hbox (3.24176pt too wide) in paragraph at lines 7878--7883
\OT1/cmr/m/n/10 (-20) Today there is a pref-er-ence for writ-ing as-ser-tions i
n some-thing called``deduction
[96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8001.
LaTeX Warning: Citation `CarneiroND' on page 98 undefined on input line 8038.
[98]
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8054.
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Ration-
Underfull \hbox (badness 7379) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmtt/m/n/10 pm2.65da
[99]
Package longtable Warning: Column widths have changed
(longtable)                in table 3.4 on input line 8163.
[100] [101]
LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8277.
[102] [103]
LaTeX Warning: Citation `Hamilton' on page 104 undefined on input line 8396.
[104] [105] [106] [107] [108]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 109 undefined on input line 8661.
[109]
LaTeX Warning: Citation `deMillo' on page 110 undefined on input line 8713.
[110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120] [121]
[122]
LaTeX Warning: Citation `Nemeti' on page 123 undefined on input line 9650.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9651.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9658.
[123] [124] [125] [126] [127] [128] [129]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10136.
[130] [131] [132] [133] [134] [135] [136] [137] [138] [139] [140] [141]
[142] [143] [144] [145] [146] [147]
LaTeX Warning: Citation `Behnke' on page 148 undefined on input line 11548.
[148]
LaTeX Warning: Citation `Nemesszeghy' on page 149 undefined on input line 11559
.
LaTeX Warning: Citation `Lejewski' on page 149 undefined on input line 11575.
LaTeX Warning: Citation `Goodstein' on page 149 undefined on input line 11653.
LaTeX Warning: Citation `Robinsont' on page 149 undefined on input line 11662.
[149]
LaTeX Warning: Citation `Quine' on page 150 undefined on input line 11683.
[150]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 11811--11819
[]\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
[151] [152]
Chapter 5.
[153] [154] [155] [156] [157]
Overfull \hbox (51.2085pt too wide) in paragraph at lines 12208--12213
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 write source \OT1/cmr/m/it/10 (-
20) file-name \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /rewrap\OT1/cmr/m/n/10 (-
20) ] [\OT1/cmtt/m/n/10 /split\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /keep[]
includes\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /no[]versioning\OT1/cmr/m/n/1
0 (-20) ] 
[158] [159] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169]
[170] [171] [172] [173] [174] [175] [176]
Appendix A.
LaTeX Warning: Hyper reference `df-bi' on page 177 undefined on input line 1359
0.
Underfull \hbox (badness 3780) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
LaTeX Warning: Hyper reference `df-or' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-3or' on page 177 undefined on input line 135
90.
LaTeX Warning: Hyper reference `df-an' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-3an' on page 177 undefined on input line 135
90.
LaTeX Warning: Hyper reference `df-ex' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-sb' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-eu' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-clab' on page 177 undefined on input line 13
590.
LaTeX Warning: Hyper reference `df-cleq' on page 177 undefined on input line 13
590.
LaTeX Warning: Hyper reference `df-clel' on page 177 undefined on input line 13
590.
LaTeX Warning: Hyper reference `df-ss' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-un' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-in' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-dif' on page 177 undefined on input line 135
90.
LaTeX Warning: Hyper reference `df-nul' on page 177 undefined on input line 135
90.
LaTeX Warning: Hyper reference `df-op' on page 177 undefined on input line 1359
0.
LaTeX Warning: Hyper reference `df-fv' on page 177 undefined on input line 1359
0.
Underfull \hbox (badness 4266) in paragraph at lines 13590--13590
[]\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 13590.
[177] [178] [179] [180]
Appendix B.
[181] [182]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 183 undefined on input line 13857.
LaTeX Warning: Citation `Munkres' on page 183 undefined on input line 13871.
LaTeX Warning: Citation `Tarski1965' on page 183 undefined on input line 13888.
[183] [184] [185]
LaTeX Warning: Citation `Nemeti' on page 186 undefined on input line 14075.
[186] [187] [188]
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14296.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14297.
(/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 189 undefined on input line 14351.
[189] [190] [191]
LaTeX Warning: Citation `Hamilton' on page 192 undefined on input line 14521.
LaTeX Warning: Citation `Tarski1965' on page 192 undefined on input line 14528.
[192]
LaTeX Warning: Citation `Kalish' on page 193 undefined on input line 14588.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14601.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14612.
[193] [194] [195]
LaTeX Warning: Citation `Takeuti' on page 196 undefined on input line 14851.
LaTeX Warning: Citation `Quine' on page 196 undefined on input line 14852.
[196] [197] [198] [199] [200]
Appendix D.
[201] [202]
LaTeX Warning: Citation `Hofstadter' on page 203 undefined on input line 15132.
[203] [204]
Appendix E.
Overfull \hbox (2.96838pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 /* File inclusion command.  The file is processed as a datab
ase.[] 
[205]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15231--15231
[]   \OT1/cmtt/m/n/10 If '?' is anywhere in a proof then it is an "incomplete" 
proof. */[] 
Overfull \hbox (0.8684pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 filename ::= MATH-SYMBOL /* Cannot include whitespace or '$'
 */[] 
[206]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 _PRINTABLE-CHARACTER ::= [#x21-#x7e] /* ASCII printable char
acters */[] 
Overfull \hbox (6.64334pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 /* Define whitespace between tokens. The -> SKIP means that 
when[] 
Overfull \hbox (11.3683pt too wide) in paragraph at lines 15291--15291
[]   \OT1/cmtt/m/n/10 whitespace is seen, it is skipped and we simply read agai
n. */[] 
[207] [208]
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{htmlmkup} has been referenced but does not exist, r
eplaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlmkup\040} has been referenced b
ut 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.redeclarationf\040} has been refere
nced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.mathcomments\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.tut1\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.ax1\040} has been referenced but do
es not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfbr\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfopr\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.effectivelybound\040} has been refe
renced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.expandom\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfom\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfclel\040} has been referenced but
 does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dollardollar\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.zeroproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.treeproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.includef\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.demo0\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.demoproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.nodd\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.envision\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.languagespec\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.using\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.spec\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.poincare\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.namespace\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.categoryth\040} has been referenced
 but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.bourbaki\040} has been referenced b
ut does not exist, replaced by a fixed one
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/
share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/
texlive/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/fonts/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/cmextra/cmex8.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
mi8.pfb></usr/share/texlive/texmf-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/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/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/cmsl8.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
msy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/shar
+ pdflatex metamath
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/symbols/msbm7.pfb>
Output written on metamath.pdf (222 pages, 1023805 bytes).
Transcript written on metamath.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2018-04-01> patch level 5
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 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex)
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te
xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] [4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 106.
[5] [6]) [7] [8] [9] [10]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on
 input line 1112.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i
nput line 1117.
[11] [12]
LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1214.
[13]
LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1239.
[14] [15] [16] [17] [18]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1414.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1507.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1574.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1611.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1617.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1649.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1769.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1988.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2062.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2070.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2079.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2101.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2129.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2145.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2152.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2157.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2205.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2241.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2243.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2260.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2273.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2273.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2287.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2307.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2402.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2427.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2461.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2473.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2507.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2514.
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2533.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2546.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2550.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2561.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2571.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2575.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2588.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2589.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2618.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
63.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2672.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2682.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2687.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2697.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2739.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2767.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2776.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2784.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2815.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2894.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2916.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3127.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3128.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3136.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3148.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3156.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3186.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3198.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3244.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3246.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3261.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3360.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3363.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3364.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3500.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3501.
[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 4489.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4701.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4712--4716
[]\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 4845--4850
\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 4896.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4909.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4950.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4978.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4995.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5014.
[67] [68] [69] [70]
Overfull \hbox (18.1588pt too wide) in paragraph at lines 5297--5297
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with equal-ity - Tarski's
Overfull \hbox (2.30984pt too wide) in paragraph at lines 5377--5377
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equal-ity - Aux-
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5697.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5698.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5699.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5699.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5952.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5954.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5955.
[77] [78] [79] [80] [81] [82] [83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6909.
[86] [87] [88] [89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7596.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7736.
[94] [95]
Overfull \hbox (3.24176pt too wide) in paragraph at lines 7878--7883
\OT1/cmr/m/n/10 (-20) Today there is a pref-er-ence for writ-ing as-ser-tions i
n some-thing called``deduction
[96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8001.
LaTeX Warning: Citation `CarneiroND' on page 98 undefined on input line 8038.
[98]
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8054.
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Ration-
Underfull \hbox (badness 7379) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmtt/m/n/10 pm2.65da
[99] [100] [101]
LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8277.
[102] [103]
LaTeX Warning: Citation `Hamilton' on page 104 undefined on input line 8396.
[104] [105] [106] [107] [108]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 109 undefined on input line 8661.
[109]
LaTeX Warning: Citation `deMillo' on page 110 undefined on input line 8713.
[110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120] [121]
[122]
LaTeX Warning: Citation `Nemeti' on page 123 undefined on input line 9650.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9651.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9658.
[123] [124] [125] [126] [127] [128] [129]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10136.
[130] [131] [132] [133] [134] [135] [136] [137] [138] [139] [140] [141]
[142] [143] [144] [145] [146] [147]
LaTeX Warning: Citation `Behnke' on page 148 undefined on input line 11548.
[148]
LaTeX Warning: Citation `Nemesszeghy' on page 149 undefined on input line 11559
.
LaTeX Warning: Citation `Lejewski' on page 149 undefined on input line 11575.
LaTeX Warning: Citation `Goodstein' on page 149 undefined on input line 11653.
LaTeX Warning: Citation `Robinsont' on page 149 undefined on input line 11662.
[149]
LaTeX Warning: Citation `Quine' on page 150 undefined on input line 11683.
[150]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 11811--11819
[]\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
[151] [152]
Chapter 5.
[153] [154] [155] [156] [157]
Overfull \hbox (51.2085pt too wide) in paragraph at lines 12208--12213
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 write source \OT1/cmr/m/it/10 (-
20) file-name \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /rewrap\OT1/cmr/m/n/10 (-
20) ] [\OT1/cmtt/m/n/10 /split\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /keep[]
includes\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /no[]versioning\OT1/cmr/m/n/1
0 (-20) ] 
[158] [159] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169]
[170] [171] [172] [173] [174] [175] [176]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[177] [178] [179] [180]
Appendix B.
[181] [182]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 183 undefined on input line 13857.
LaTeX Warning: Citation `Munkres' on page 183 undefined on input line 13871.
LaTeX Warning: Citation `Tarski1965' on page 183 undefined on input line 13888.
[183] [184] [185]
LaTeX Warning: Citation `Nemeti' on page 186 undefined on input line 14075.
[186] [187] [188]
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14296.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14297.
[189] (/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 190 undefined on input line 14351.
[190] [191]
LaTeX Warning: Citation `Hamilton' on page 192 undefined on input line 14521.
LaTeX Warning: Citation `Tarski1965' on page 192 undefined on input line 14528.
[192]
LaTeX Warning: Citation `Kalish' on page 193 undefined on input line 14588.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14601.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14612.
[193] [194] [195]
LaTeX Warning: Citation `Takeuti' on page 196 undefined on input line 14851.
LaTeX Warning: Citation `Quine' on page 196 undefined on input line 14852.
[196] [197] [198] [199] [200]
Appendix D.
[201] [202]
LaTeX Warning: Citation `Hofstadter' on page 203 undefined on input line 15132.
[203] [204]
Appendix E.
Overfull \hbox (2.96838pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 /* File inclusion command.  The file is processed as a datab
ase.[] 
[205]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15231--15231
[]   \OT1/cmtt/m/n/10 If '?' is anywhere in a proof then it is an "incomplete" 
proof. */[] 
Overfull \hbox (0.8684pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 filename ::= MATH-SYMBOL /* Cannot include whitespace or '$'
 */[] 
[206]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 _PRINTABLE-CHARACTER ::= [#x21-#x7e] /* ASCII printable char
acters */[] 
Overfull \hbox (6.64334pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 /* Define whitespace between tokens. The -> SKIP means that 
when[] 
Overfull \hbox (11.3683pt too wide) in paragraph at lines 15291--15291
[]   \OT1/cmtt/m/n/10 whitespace is seen, it is skipped and we simply read agai
n. */[] 
[207] [208]
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)pdfTeX warning (dest): name
{htmlmkup} has been referenced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlmkup\040} has been referenced b
ut does not exist, replaced by a fixed one
</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/
texlive/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/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/
BUILDSTDERR: fonts/type1/public/amsfonts/cm+ bibtex metamath
+ makeindex metamath.idx
BUILDSTDERR: This is makeindex, version 2.15 [TeX Live 2018] (kpathsea + Thai support).
BUILDSTDERR: Scanning input file metamath.idx.....done (1589 entries accepted, 0 rejected).
BUILDSTDERR: Sorting entries................done (18491 comparisons).
BUILDSTDERR: Generating output file metamath.ind.....done (924 lines written, 0 warnings).
BUILDSTDERR: Output written in metamath.ind.
BUILDSTDERR: Transcript written in metamath.ilg.
+ pdflatex metamath
/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cmextra/cmex8.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
mi8.pfb></usr/share/texlive/texmf-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/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/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/cmsl8.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
msy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/symbols/msbm7.pfb>
Output written on metamath.pdf (226 pages, 1046911 bytes).
Transcript written on metamath.log.
This is BibTeX, Version 0.99d (TeX Live 2018)
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)
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2018-04-01> patch level 5
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 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex)
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te
xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] [4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 106.
[5] [6]) [7] [8] [9] [10]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on
 input line 1112.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i
nput line 1117.
[11] [12]
LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1214.
[13]
LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1239.
[14] [15] [16] [17] [18]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1414.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1507.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1574.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1611.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1617.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1649.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1769.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1988.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2062.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2070.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2079.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2101.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2129.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2145.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2152.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2157.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2205.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2239.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2241.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2243.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2260.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2273.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2273.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2287.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2307.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2402.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2427.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2461.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2473.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2507.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2514.
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2533.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2546.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2550.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2561.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2571.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2575.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2588.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2589.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2618.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
63.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2672.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2682.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2687.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2697.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2739.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2767.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2776.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2784.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2815.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2894.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2916.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3127.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3128.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3136.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3148.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3156.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3177.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3178.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3186.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3198.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3229.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3244.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3246.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3261.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3360.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3363.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3364.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3500.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3501.
[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 4489.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4701.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4712--4716
[]\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 4845--4850
\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 4896.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4909.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4950.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4978.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 4995.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5014.
[67] [68] [69] [70]
Overfull \hbox (18.1588pt too wide) in paragraph at lines 5297--5297
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with equal-ity - Tarski's
Overfull \hbox (2.30984pt too wide) in paragraph at lines 5377--5377
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equal-ity - Aux-
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5697.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5698.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5699.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5699.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5952.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5954.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5955.
[77] [78] [79] [80] [81] [82] [83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6909.
[86] [87] [88] [89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7596.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7736.
[94] [95]
Overfull \hbox (3.24176pt too wide) in paragraph at lines 7878--7883
\OT1/cmr/m/n/10 (-20) Today there is a pref-er-ence for writ-ing as-ser-tions i
n some-thing called``deduction
[96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8001.
LaTeX Warning: Citation `CarneiroND' on page 98 undefined on input line 8038.
[98]
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8054.
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Ration-
Underfull \hbox (badness 7379) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmtt/m/n/10 pm2.65da
[99] [100] [101]
LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8277.
[102] [103]
LaTeX Warning: Citation `Hamilton' on page 104 undefined on input line 8396.
[104] [105] [106] [107] [108]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 109 undefined on input line 8661.
[109]
LaTeX Warning: Citation `deMillo' on page 110 undefined on input line 8713.
[110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120] [121]
[122]
LaTeX Warning: Citation `Nemeti' on page 123 undefined on input line 9650.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9651.
LaTeX Warning: Citation `Megill' on page 123 undefined on input line 9658.
[123] [124] [125] [126] [127] [128] [129]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10136.
[130] [131] [132] [133] [134] [135] [136] [137] [138] [139] [140] [141]
[142] [143] [144] [145] [146] [147]
LaTeX Warning: Citation `Behnke' on page 148 undefined on input line 11548.
[148]
LaTeX Warning: Citation `Nemesszeghy' on page 149 undefined on input line 11559
.
LaTeX Warning: Citation `Lejewski' on page 149 undefined on input line 11575.
LaTeX Warning: Citation `Goodstein' on page 149 undefined on input line 11653.
LaTeX Warning: Citation `Robinsont' on page 149 undefined on input line 11662.
[149]
LaTeX Warning: Citation `Quine' on page 150 undefined on input line 11683.
[150]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 11811--11819
[]\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
[151] [152]
Chapter 5.
[153] [154] [155] [156] [157]
Overfull \hbox (51.2085pt too wide) in paragraph at lines 12208--12213
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 write source \OT1/cmr/m/it/10 (-
20) file-name \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /rewrap\OT1/cmr/m/n/10 (-
20) ] [\OT1/cmtt/m/n/10 /split\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /keep[]
includes\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /no[]versioning\OT1/cmr/m/n/1
0 (-20) ] 
[158] [159] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169]
[170] [171] [172] [173] [174] [175] [176]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[177] [178] [179] [180]
Appendix B.
[181] [182]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 183 undefined on input line 13857.
LaTeX Warning: Citation `Munkres' on page 183 undefined on input line 13871.
LaTeX Warning: Citation `Tarski1965' on page 183 undefined on input line 13888.
[183] [184] [185]
LaTeX Warning: Citation `Nemeti' on page 186 undefined on input line 14075.
[186] [187] [188]
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14296.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14297.
[189] (/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 190 undefined on input line 14351.
[190] [191]
LaTeX Warning: Citation `Hamilton' on page 192 undefined on input line 14521.
LaTeX Warning: Citation `Tarski1965' on page 192 undefined on input line 14528.
[192]
LaTeX Warning: Citation `Kalish' on page 193 undefined on input line 14588.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14601.
LaTeX Warning: Citation `Megill' on page 193 undefined on input line 14612.
[193] [194] [195]
LaTeX Warning: Citation `Takeuti' on page 196 undefined on input line 14851.
LaTeX Warning: Citation `Quine' on page 196 undefined on input line 14852.
[196] [197] [198] [199] [200]
Appendix D.
[201] [202]
LaTeX Warning: Citation `Hofstadter' on page 203 undefined on input line 15132.
[203] [204]
Appendix E.
Overfull \hbox (2.96838pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 /* File inclusion command.  The file is processed as a datab
ase.[] 
[205]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15231--15231
[]   \OT1/cmtt/m/n/10 If '?' is anywhere in a proof then it is an "incomplete" 
proof. */[] 
Overfull \hbox (0.8684pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 filename ::= MATH-SYMBOL /* Cannot include whitespace or '$'
 */[] 
[206]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 _PRINTABLE-CHARACTER ::= [#x21-#x7e] /* ASCII printable char
acters */[] 
Overfull \hbox (6.64334pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 /* Define whitespace between tokens. The -> SKIP means that 
when[] 
Overfull \hbox (11.3683pt too wide) in paragraph at lines 15291--15291
[]   \OT1/cmtt/m/n/10 whitespace is seen, it is skipped and we simply read agai
n. */[] 
[207] [208] (./metamath.bbl [209] [210] [211] [212] [213]) [214]
(./metamath.ind [215] [216] [217] [218] [219] [220] [221] [222] [223])
(./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
{htmlmkup} has been referenced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlmkup\040} has been referenced b
ut does not exist, replaced by a fixed one
</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/
texlive/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/fonts/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/cmextra/cmex8.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
mi8.pfb></usr/share/texlive/texmf-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/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/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/cmsl8.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
msy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/symbols/msbm7.pfb>
BUILDSTDERR: Output written on metamath.pdf (241 pages+ pdflatex metamath
, 1127493 bytes).
Transcript written on metamath.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2018-04-01> patch level 5
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 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex)
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te
xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] [4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 106.
[5] [6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18]
Chapter 1.
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17]
[18] [19] [20] [21] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
[22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36]
Chapter 2.
[37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51]
[52] [53] [54] [55] [56] [57] [58]
Chapter 3.
[59] [60] [61] [62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4712--4716
[]\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 4845--4850
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
[65] [66] [67] [68] [69] [70]
Overfull \hbox (18.1588pt too wide) in paragraph at lines 5297--5297
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with equal-ity - Tarski's
Overfull \hbox (2.30984pt too wide) in paragraph at lines 5377--5377
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equal-ity - Aux-
[71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82] [83] [84] [85]
[86] [87] [88] [89] [90] [91] [92] [93] [94] [95]
Overfull \hbox (3.24176pt too wide) in paragraph at lines 7878--7883
\OT1/cmr/m/n/10 (-20) Today there is a pref-er-ence for writ-ing as-ser-tions i
n some-thing called``deduction
[96] [97] [98]
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Ration-
Underfull \hbox (badness 7379) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmtt/m/n/10 pm2.65da
[99] [100] [101] [102] [103] [104] [105] [106] [107] [108]
Chapter 4.
[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]
[121] [122] [123] [124] [125] [126] [127] [128] [129]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10136.
[130] [131] [132] [133] [134] [135] [136] [137] [138] [139] [140] [141]
[142] [143] [144] [145] [146] [147] [148] [149] [150]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 11811--11819
[]\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
[151] [152]
Chapter 5.
[153] [154] [155] [156] [157]
Overfull \hbox (51.2085pt too wide) in paragraph at lines 12208--12213
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 write source \OT1/cmr/m/it/10 (-
20) file-name \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /rewrap\OT1/cmr/m/n/10 (-
20) ] [\OT1/cmtt/m/n/10 /split\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /keep[]
includes\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /no[]versioning\OT1/cmr/m/n/1
0 (-20) ] 
[158] [159] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169]
[170] [171] [172] [173] [174] [175] [176]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[177] [178] [179] [180]
Appendix B.
[181] [182]
Appendix C.
[183] [184] [185] [186] [187] [188] [189]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [190] [191]
[192] [193] [194] [195] [196] [197] [198] [199] [200]
Appendix D.
[201] [202] [203] [204]
Appendix E.
Overfull \hbox (2.96838pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 /* File inclusion command.  The file is processed as a datab
ase.[] 
[205]
BUILDSTDERR: Overfull \hbox (32.36812pt too wide) in parag+ pdflatex metamath
raph at lines 15231--15231
[]   \OT1/cmtt/m/n/10 If '?' is anywhere in a proof then it is an "incomplete" 
proof. */[] 
Overfull \hbox (0.8684pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 filename ::= MATH-SYMBOL /* Cannot include whitespace or '$'
 */[] 
[206]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 _PRINTABLE-CHARACTER ::= [#x21-#x7e] /* ASCII printable char
acters */[] 
Overfull \hbox (6.64334pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 /* Define whitespace between tokens. The -> SKIP means that 
when[] 
Overfull \hbox (11.3683pt too wide) in paragraph at lines 15291--15291
[]   \OT1/cmtt/m/n/10 whitespace is seen, it is skipped and we simply read agai
n. */[] 
[207] [208] (./metamath.bbl [209] [210] [211] [212] [213]) [214]
(./metamath.ind [215] [216] [217] [218] [219] [220] [221] [222] [223])
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
 )
(see the transcript file for additional information)pdfTeX warning (dest): name
{htmlmkup} has been referenced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlmkup\040} has been referenced b
ut does not exist, replaced by a fixed one
</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/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cmextra/cmex8.pfb></usr/share/texlive/texmf-dist/f
onts/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/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r10.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/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dis
t/fonts/type1/public/amsfonts/cm/cmsl8.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.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/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/symbols/msbm7.pfb>
Output written on metamath.pdf (241 pages, 1124857 bytes).
Transcript written on metamath.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2018-04-01> patch level 5
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 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3-code.tex)
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/l3pdfmode.def))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/usr/share/te
xlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] [4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 106.
[5] [6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18]
Chapter 1.
[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17]
[18] [19] [20] [21] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
[22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36]
Chapter 2.
[37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51]
[52] [53] [54] [55] [56] [57] [58]
Chapter 3.
[59] [60] [61] [62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4712--4716
[]\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 4845--4850
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
[65] [66] [67] [68] [69] [70]
Overfull \hbox (18.1588pt too wide) in paragraph at lines 5297--5297
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with equal-ity - Tarski's
Overfull \hbox (2.30984pt too wide) in paragraph at lines 5377--5377
[]\OT1/cmr/bx/n/12 Axioms of Pred-i-cate Cal-cu-lus with Equal-ity - Aux-
[71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82] [83] [84] [85]
[86] [87] [88] [89] [90] [91] [92] [93] [94] [95]
Overfull \hbox (3.24176pt too wide) in paragraph at lines 7878--7883
\OT1/cmr/m/n/10 (-20) Today there is a pref-er-ence for writ-ing as-ser-tions i
n some-thing called``deduction
[96] [97] [98]
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 ND
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
\OT1/cmr/bx/n/10 Ration-
Underfull \hbox (badness 7379) in paragraph at lines 8122--8122
[]\OT1/cmr/bx/n/10 MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8122--8122
[]\OT1/cmr/m/n/10 (+20) $e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8122--8122
[]\OT1/cmtt/m/n/10 pm2.65da
[99] [100] [101] [102] [103] [104] [105] [106] [107] [108]
Chapter 4.
[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]
[121] [122] [123] [124] [125] [126] [127] [128] [129]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10136.
[130] [131] [132] [133] [134] [135] [136] [137] [138] [139] [140] [141]
[142] [143] [144] [145] [146] [147] [148] [149] [150]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 11811--11819
[]\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
[151] [152]
Chapter 5.
[153] [154] [155] [156] [157]
Overfull \hbox (51.2085pt too wide) in paragraph at lines 12208--12213
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 write source \OT1/cmr/m/it/10 (-
20) file-name \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /rewrap\OT1/cmr/m/n/10 (-
20) ] [\OT1/cmtt/m/n/10 /split\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /keep[]
includes\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /no[]versioning\OT1/cmr/m/n/1
0 (-20) ] 
[158] [159] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169]
[170] [171] [172] [173] [174] [175] [176]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13590--13590
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[177] [178] [179] [180]
Appendix B.
[181] [182]
Appendix C.
[183] [184] [185] [186] [187] [188] [189]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [190] [191]
[192] [193] [194] [195] [196] [197] [198] [199] [200]
Appendix D.
[201] [202] [203] [204]
Appendix E.
Overfull \hbox (2.96838pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 /* File inclusion command.  The file is processed as a datab
ase.[] 
[205]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15231--15231
[]   \OT1/cmtt/m/n/10 If '?' is anywhere in a proof then it is an "incomplete" 
proof. */[] 
Overfull \hbox (0.8684pt too wide) in paragraph at lines 15231--15231
[]\OT1/cmtt/m/n/10 filename ::= MATH-SYMBOL /* Cannot include whitespace or '$'
 */[] 
[206]
Overfull \hbox (32.36812pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 _PRINTABLE-CHARACTER ::= [#x21-#x7e] /* ASCII printable char
acters */[] 
BUILDSTDERR: Overfull \hbox (6.643+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
34pt too wide) in paragraph at lines 15291--15291
[]\OT1/cmtt/m/n/10 /* Define whitespace between tokens. The -> SKIP means that 
when[] 
Overfull \hbox (11.3683pt too wide) in paragraph at lines 15291--15291
[]   \OT1/cmtt/m/n/10 whitespace is seen, it is skipped and we simply read agai
n. */[] 
[207] [208] (./metamath.bbl [209] [210] [211] [212] [213]) [214]
(./metamath.ind [215] [216] [217] [218] [219] [220] [221] [222] [223])
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
 )
(see the transcript file for additional information)pdfTeX warning (dest): name
{htmlmkup} has been referenced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlmkup\040} has been referenced b
ut does not exist, replaced by a fixed one
</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/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cmextra/cmex8.pfb></usr/share/texlive/texmf-dist/f
onts/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/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r10.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/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dis
t/fonts/type1/public/amsfonts/cm/cmsl8.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.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/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/symbols/msbm7.pfb>
Output written on metamath.pdf (241 pages, 1124857 bytes).
Transcript written on metamath.log.
Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.ko36p8
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64 '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64
BUILDSTDERR: ++ dirname /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64
+ cd metamath
+ /usr/bin/make install DESTDIR=/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64 'INSTALL=/usr/bin/install -p'
+ 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.177-2.fc31.riscv64/usr/share/metamath
+ mkdir -p /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/doc/metamath
+ cp -p metamath.pdf /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/doc/metamath
+ /usr/lib/rpm/find-debuginfo.sh -j4 --strict-build-id -m -i --build-id-seed 0.177-2.fc31 --unique-debug-suffix -0.177-2.fc31.riscv64 --unique-debug-src-base metamath-0.177-2.fc31.riscv64 --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 -S debugsourcefiles.list /builddir/build/BUILD/metamath
BUILDSTDERR: 3589 blocks
+ /usr/lib/rpm/check-buildroot
+ /usr/lib/rpm/redhat/brp-ldconfig
+ /usr/lib/rpm/brp-compress
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/redhat/brp-python-bytecompile /usr/bin/python 1 0
+ /usr/lib/rpm/brp-python-hardlink
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
make[1]: Entering directory '/builddir/build/BUILD/metamath'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/bin'
  /usr/bin/install -p metamath '/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/bin'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.177-2.fc31.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.177-2.fc31.riscv64/usr/share/metamath'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/man/man1'
 /usr/bin/install -p -m 644 metamath.1 '/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/man/man1'
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
explicitly decompress any DWARF compressed ELF sections in /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/bin/metamath
extracting debug info from /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/bin/metamath
original debug info size: 1360kB, size after compression: 1280kB
/usr/lib/rpm/sepdebugcrcfix: Updated 1 CRC32s, 0 CRC32s did match.
Processing files: metamath-0.177-2.fc31.riscv64
Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.M8Sj36
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ DOCDIR=/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/doc/metamath
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/doc/metamath
+ cp -pr README.TXT /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/doc/metamath
+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.bKV5e7
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath
+ cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath
+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
Provides: metamath = 0.177-2.fc31 metamath(riscv-64) = 0.177-2.fc31
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.177-2.fc31.noarch
Provides: metamath-theories = 0.177-2.fc31
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-doc-0.177-2.fc31.noarch
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.i6MNi6
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath-doc
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath-doc
+ cp -pr LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64/usr/share/licenses/metamath-doc
+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
Provides: metamath-doc = 0.177-2.fc31
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-debugsource-0.177-2.fc31.riscv64
Provides: metamath-debugsource = 0.177-2.fc31 metamath-debugsource(riscv-64) = 0.177-2.fc31
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-debuginfo-0.177-2.fc31.riscv64
Provides: debuginfo(build-id) = 11e7ee45ee35bf319abd207edfbdce5f39e54d80 metamath-debuginfo = 0.177-2.fc31 metamath-debuginfo(riscv-64) = 0.177-2.fc31
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.177-2.fc31
Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64
Wrote: /builddir/build/RPMS/metamath-doc-0.177-2.fc31.noarch.rpm
Wrote: /builddir/build/RPMS/metamath-0.177-2.fc31.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-debuginfo-0.177-2.fc31.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-debugsource-0.177-2.fc31.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-theories-0.177-2.fc31.noarch.rpm
Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.tr4g96
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ /usr/bin/rm -rf /builddir/build/BUILDROOT/metamath-0.177-2.fc31.riscv64
+ RPM_EC=0
BUILDSTDERR: ++ jobs -p
+ exit 0
Child return code was: 0