--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Journal/root.log Mon Nov 01 10:40:21 2021 +0000
@@ -0,0 +1,1995 @@
+This is LuaTeX, Version 1.07.0 (TeX Live 2018) (format=lualatex 2019.2.7) 1 NOV 2021 09:38
+ restricted system commands enabled.
+**root.tex
+(./root.tex
+LaTeX2e <2018-04-01> patch level 2
+Lua module: luaotfload-main 2017/01/29 2.80001 OpenType layout system.
+Lua module: lualibs 2017-02-01 2.5 ConTeXt Lua standard libraries.
+Lua module: lualibs-extended 2017-02-01 2.5 ConTeXt Lua libraries -- extended co
+llection.(using write cache: /Users/cstan/Library/texlive/2018/texmf-var/luatex-
+cache/generic)(using read cache: /usr/local/texlive/2018/texmf-var/luatex-cache/
+generic /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic)
+luaotfload | conf : Root cache directory is /Users/cstan/Library/texlive/2018/te
+xmf-var/luatex-cache/generic/names.
+luaotfload | init : Loading fontloader “fontloader-2017-02-11.lua” from kpse
+-resolved path “/usr/local/texlive/2018/texmf-dist/tex/luatex/luaotfload/fontl
+oader-2017-02-11.lua”.
+Lua-only attribute luaotfload@state = 1
+Lua-only attribute luaotfload@noligature = 2
+Lua-only attribute luaotfload@syllabe = 3
+luaotfload | init : Context OpenType loader version “3.027”
+Inserting `luaotfload.node_processor' at position 1 in `pre_linebreak_filter'.
+Inserting `luaotfload.node_processor' at position 1 in `hpack_filter'.
+Inserting `luaotfload.define_font' at position 1 in `define_font'.
+Lua-only attribute luaotfload_color_attribute = 4
+luaotfload | conf : Root cache directory is /Users/cstan/Library/texlive/2018/te
+xmf-var/luatex-cache/generic/names.
+Inserting `luaotfload.aux.set_sscale_dimens' at position 1 in `luaotfload.patch_
+font'.
+Inserting `luaotfload.aux.patch_cambria_domh' at position 2 in `luaotfload.patch
+_font'.
+Inserting `luaotfload.aux.fixup_fontdata' at position 1 in `luaotfload.patch_fon
+t_unsafe'.
+Inserting `luaotfload.aux.set_capheight' at position 3 in `luaotfload.patch_font
+'.
+Inserting `luaotfload.rewrite_fontname' at position 4 in `luaotfload.patch_font'
+.
+luaotfload | main : initialization completed in 0.091 seconds
+Babel <3.18> and hyphenation patterns for 1 language(s) loaded.
+(./llncs.cls
+Document Class: llncs 2002/01/28 v2.13
+ LaTeX document class for Lecture Notes in Computer Science
+(/usr/local/texlive/2018/texmf-dist/tex/latex/base/article.cls
+Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
+(/usr/local/texlive/2018/texmf-dist/tex/latex/base/size10.clo
+File: size10.clo 2014/09/29 v1.4h Standard LaTeX file (size option)
+luaotfload | db : Font names database loaded from /Users/cstan/Library/texlive/2
+018/texmf-var/luatex-cache/generic/names/luaotfload-names.luc(load luc: /Users/c
+stan/Library/texlive/2018/texmf-var/luatex-cache/generic/fonts/otl/lmroman10-reg
+ular.luc))
+\c@part=\count80
+\c@section=\count81
+\c@subsection=\count82
+\c@subsubsection=\count83
+\c@paragraph=\count84
+\c@subparagraph=\count85
+\c@figure=\count86
+\c@table=\count87
+\abovecaptionskip=\skip41
+\belowcaptionskip=\skip42
+\bibindent=\dimen102
+) (/usr/local/texlive/2018/texmf-dist/tex/latex/tools/multicol.sty
+Package: multicol 2018/04/01 v1.8r multicolumn formatting (FMi)
+\c@tracingmulticols=\count88
+\mult@box=\box26
+\multicol@leftmargin=\dimen103
+\c@unbalance=\count89
+\c@collectmore=\count90
+\doublecol@number=\count91
+\multicoltolerance=\count92
+\multicolpretolerance=\count93
+\full@width=\dimen104
+\page@free=\dimen105
+\premulticols=\dimen106
+\postmulticols=\dimen107
+\multicolsep=\skip43
+\multicolbaselineskip=\skip44
+\partial@page=\box27
+\last@line=\box28
+\maxbalancingoverflow=\dimen108
+\mult@rightbox=\box29
+\mult@grightbox=\box30
+\mult@gfirstbox=\box31
+\mult@firstbox=\box32
+\@tempa=\box33
+\@tempa=\box34
+\@tempa=\box35
+\@tempa=\box36
+\@tempa=\box37
+\@tempa=\box38
+\@tempa=\box39
+\@tempa=\box40
+\@tempa=\box41
+\@tempa=\box42
+\@tempa=\box43
+\@tempa=\box44
+\@tempa=\box45
+\@tempa=\box46
+\@tempa=\box47
+\@tempa=\box48
+\@tempa=\box49
+\c@columnbadness=\count94
+\c@finalcolumnbadness=\count95
+\last@try=\dimen109
+\multicolovershoot=\dimen110
+\multicolundershoot=\dimen111
+\mult@nat@firstbox=\box50
+\colbreak@box=\box51
+\mc@col@check@num=\count96
+)
+\c@chapter=\count97
+LaTeX Font Info: Redeclaring math symbol \Gamma on input line 360.
+LaTeX Font Info: Redeclaring math symbol \Delta on input line 361.
+LaTeX Font Info: Redeclaring math symbol \Theta on input line 362.
+LaTeX Font Info: Redeclaring math symbol \Lambda on input line 363.
+LaTeX Font Info: Redeclaring math symbol \Xi on input line 364.
+LaTeX Font Info: Redeclaring math symbol \Pi on input line 365.
+LaTeX Font Info: Redeclaring math symbol \Sigma on input line 366.
+LaTeX Font Info: Redeclaring math symbol \Upsilon on input line 367.
+LaTeX Font Info: Redeclaring math symbol \Phi on input line 368.
+LaTeX Font Info: Redeclaring math symbol \Psi on input line 369.
+LaTeX Font Info: Redeclaring math symbol \Omega on input line 370.
+\tocchpnum=\dimen112
+\tocsecnum=\dimen113
+\tocsectotal=\dimen114
+\tocsubsecnum=\dimen115
+\tocsubsectotal=\dimen116
+\tocsubsubsecnum=\dimen117
+\tocsubsubsectotal=\dimen118
+\tocparanum=\dimen119
+\tocparatotal=\dimen120
+\tocsubparanum=\dimen121
+\@tempcntc=\count98
+\fnindent=\dimen122
+\c@@inst=\count99
+\c@@auth=\count100
+\c@auco=\count101
+\instindent=\dimen123
+\authrun=\box52
+\authorrunning=\toks14
+\tocauthor=\toks15
+\titrun=\box53
+\titlerunning=\toks16
+\toctitle=\toks17
+\c@theorem=\count102
+\c@case=\count103
+\c@conjecture=\count104
+\c@corollary=\count105
+\c@definition=\count106
+\c@example=\count107
+\c@exercise=\count108
+\c@lemma=\count109
+\c@note=\count110
+\c@problem=\count111
+\c@property=\count112
+\c@proposition=\count113
+\c@question=\count114
+\c@solution=\count115
+\c@remark=\count116
+\headlineindent=\dimen124
+) (/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/times.sty
+Package: times 2005/04/12 PSNFSS-v9.2a (SPQR)
+)
+(./isabelle.sty
+\isa@parindent=\dimen125
+\isa@parskip=\dimen126
+ (/usr/local/texlive/2018/texmf-dist/tex/generic/ulem/ulem.sty
+\UL@box=\box54
+\UL@hyphenbox=\box55
+\UL@skip=\skip45
+\UL@hook=\toks18
+\UL@height=\dimen127
+\UL@pe=\count117
+\UL@pixel=\dimen128
+\ULC@box=\box56
+Package: ulem 2012/05/18
+\ULdepth=\dimen129
+)
+(./comment.sty
+\CommentStream=\write3
+ Excluding comment 'comment')
+Including comment 'isadelimdocument' Including comment 'isatagdocument'
+Including comment 'isadelimtheory' Including comment 'isatagtheory'
+Including comment 'isadelimproof' Including comment 'isatagproof'
+Including comment 'isadelimML' Including comment 'isatagML'
+Including comment 'isadelimvisible' Including comment 'isatagvisible'
+Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible'
+Including comment 'isadelimimportant' Including comment 'isatagimportant'
+Including comment 'isadelimunimportant' Including comment 'isatagunimportant')
+(./isabelletags.sty) (./isabellesym.sty)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsmath/amsmath.sty
+Package: amsmath 2017/09/02 v2.17a AMS math features
+\@mathmargin=\skip46
+
+For additional information on amsmath, use the `?' option.
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsmath/amstext.sty
+Package: amstext 2000/06/29 v2.01 AMS text
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsmath/amsgen.sty
+File: amsgen.sty 1999/11/30 v2.0 generic functions
+\@emptytoks=\toks19
+\ex@=\dimen130
+))
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsmath/amsbsy.sty
+Package: amsbsy 1999/11/29 v1.2d Bold Symbols
+\pmbraise@=\dimen131
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsmath/amsopn.sty
+Package: amsopn 2016/03/08 v2.02 operator names
+)
+\inf@bad=\count118
+LaTeX Info: Redefining \frac on input line 213.
+\uproot@=\count119
+\leftroot@=\count120
+LaTeX Info: Redefining \overline on input line 375.
+\classnum@=\count121
+\DOTSCASE@=\count122
+LaTeX Info: Redefining \ldots on input line 472.
+LaTeX Info: Redefining \dots on input line 475.
+LaTeX Info: Redefining \cdots on input line 596.
+\Mathstrutbox@=\box57
+\strutbox@=\box58
+\big@size=\dimen132
+LaTeX Font Info: Redeclaring font encoding OML on input line 712.
+LaTeX Font Info: Redeclaring font encoding OMS on input line 713.
+
+
+Package amsmath Warning: Unable to redefine math accent \vec.
+
+\macc@depth=\count123
+\c@MaxMatrixCols=\count124
+\dotsspace@=\muskip10
+\c@parentequation=\count125
+\dspbrk@lvl=\count126
+\tag@help=\toks20
+\row@=\count127
+\column@=\count128
+\maxfields@=\count129
+\andhelp@=\toks21
+\eqnshift@=\dimen133
+\alignsep@=\dimen134
+\tagshift@=\dimen135
+\tagwidth@=\dimen136
+\totwidth@=\dimen137
+\lineht@=\dimen138
+\@envbody=\toks22
+\multlinegap=\skip47
+\multlinetaggap=\skip48
+\mathdisplay@stack=\toks23
+LaTeX Info: Redefining \[ on input line 2817.
+LaTeX Info: Redefining \] on input line 2818.
+) (/usr/local/texlive/2018/texmf-dist/tex/latex/amsfonts/amssymb.sty
+Package: amssymb 2013/01/14 v3.01 AMS font symbols
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/amsfonts/amsfonts.sty
+Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
+\symAMSa=\mathgroup4
+\symAMSb=\mathgroup5
+LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
+(Font) U/euf/m/n --> U/euf/b/n on input line 106.
+))
+(/usr/local/texlive/2018/texmf-dist/tex/latex/mathpartir/mathpartir.sty
+Package: mathpartir 2016/02/24 version 1.3.2 Math Paragraph for Typesetting Infe
+rence Rules
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/keyval.sty
+Package: keyval 2014/10/28 v1.15 key=value parser (DPC)
+\KV@toks@=\toks24
+)
+\mpr@andskip=\skip49
+\mpr@lista=\toks25
+\mpr@listb=\toks26
+\mpr@hlist=\box59
+\mpr@vlist=\box60
+\mpr@right=\box61
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.te
+x
+\pgfutil@everybye=\toks27
+\pgfutil@tempdima=\dimen139
+\pgfutil@tempdimb=\dimen140
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-li
+sts.tex))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def
+\pgfutil@abb=\box62
+(/usr/local/texlive/2018/texmf-dist/tex/latex/ms/everyshi.sty
+Package: everyshi 2001/05/15 v3.00 EveryShipout Package (MS)
+))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex
+Package: pgfrcs 2015/08/07 v3.0.1a (rcs-revision 1.31)
+))
+Package: pgf 2015/08/07 v3.0.1a (rcs-revision 1.15)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/graphicx.sty
+Package: graphicx 2017/06/01 v1.1a Enhanced LaTeX Graphics (DPC,SPQR)
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/graphics.sty
+Package: graphics 2017/06/25 v1.2c Standard LaTeX Graphics (DPC,SPQR)
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/trig.sty
+Package: trig 2016/01/03 v1.10 sin cos tan (DPC)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
+File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
+)
+Package graphics Info: Driver file: luatex.def on input line 99.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics-def/luatex.def
+File: luatex.def 2018/01/08 v1.0l Graphics/color driver for luatex
+))
+\Gin@req@height=\dimen141
+\Gin@req@width=\dimen142
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex
+Package: pgfsys 2014/07/09 v3.0.1a (rcs-revision 1.48)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
+\pgfkeys@pathtoks=\toks28
+\pgfkeys@temptoks=\toks29
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.c
+ode.tex
+\pgfkeys@tmptoks=\toks30
+))
+\pgf@x=\dimen143
+\pgf@y=\dimen144
+\pgf@xa=\dimen145
+\pgf@ya=\dimen146
+\pgf@xb=\dimen147
+\pgf@yb=\dimen148
+\pgf@xc=\dimen149
+\pgf@yc=\dimen150
+\w@pgf@writea=\write4
+\r@pgf@reada=\read1
+\c@pgf@counta=\count130
+\c@pgf@countb=\count131
+\c@pgf@countc=\count132
+\c@pgf@countd=\count133
+\t@pgf@toka=\toks31
+\t@pgf@tokb=\toks32
+\t@pgf@tokc=\toks33
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg
+File: pgf.cfg 2008/05/14 (rcs-revision 1.7)
+)
+Driver file for pgf: pgfsys-luatex.def
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-luatex.d
+ef
+File: pgfsys-luatex.def 2014/10/11 (rcs-revision 1.35)
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-p
+df.def
+File: pgfsys-common-pdf.def 2013/10/10 (rcs-revision 1.13)
+)))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.
+code.tex
+File: pgfsyssoftpath.code.tex 2013/09/09 (rcs-revision 1.9)
+\pgfsyssoftpath@smallbuffer@items=\count134
+\pgfsyssoftpath@bigbuffer@items=\count135
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.
+code.tex
+File: pgfsysprotocol.code.tex 2006/10/16 (rcs-revision 1.4)
+)) (/usr/local/texlive/2018/texmf-dist/tex/latex/xcolor/xcolor.sty
+Package: xcolor 2016/05/11 v2.12 LaTeX color extensions (UK)
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics-cfg/color.cfg
+File: color.cfg 2016/01/02 v1.6 sample color configuration
+)
+Package xcolor Info: Driver file: luatex.def on input line 225.
+Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1348.
+Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1352.
+Package xcolor Info: Model `RGB' extended on input line 1364.
+Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1366.
+Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1367.
+Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1368.
+Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1369.
+Package xcolor Info: Model `Gray' substituted by `gray' on input line 1370.
+Package xcolor Info: Model `wave' substituted by `hsb' on input line 1371.
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex
+Package: pgfcore 2010/04/11 v3.0.1a (rcs-revision 1.7)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex
+\pgfmath@dimen=\dimen151
+\pgfmath@count=\count136
+\pgfmath@box=\box63
+\pgfmath@toks=\toks34
+\pgfmath@stack@operand=\toks35
+\pgfmath@stack@operation=\toks36
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.
+tex
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic
+.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigo
+nometric.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.rando
+m.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.compa
+rison.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.
+code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round
+.code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.
+code.tex)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integ
+erarithmetics.code.tex)))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex
+\c@pgfmathroundto@lastzeros=\count137
+))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.co
+de.tex
+File: pgfcorepoints.code.tex 2013/10/07 (rcs-revision 1.27)
+\pgf@picminx=\dimen152
+\pgf@picmaxx=\dimen153
+\pgf@picminy=\dimen154
+\pgf@picmaxy=\dimen155
+\pgf@pathminx=\dimen156
+\pgf@pathmaxx=\dimen157
+\pgf@pathminy=\dimen158
+\pgf@pathmaxy=\dimen159
+\pgf@xx=\dimen160
+\pgf@xy=\dimen161
+\pgf@yx=\dimen162
+\pgf@yy=\dimen163
+\pgf@zx=\dimen164
+\pgf@zy=\dimen165
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconst
+ruct.code.tex
+File: pgfcorepathconstruct.code.tex 2013/10/07 (rcs-revision 1.29)
+\pgf@path@lastx=\dimen166
+\pgf@path@lasty=\dimen167
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage
+.code.tex
+File: pgfcorepathusage.code.tex 2014/11/02 (rcs-revision 1.24)
+\pgf@shorten@end@additional=\dimen168
+\pgf@shorten@start@additional=\dimen169
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.co
+de.tex
+File: pgfcorescopes.code.tex 2015/05/08 (rcs-revision 1.46)
+\pgfpic=\box64
+\pgf@hbox=\box65
+\pgf@layerbox@main=\box66
+\pgf@picture@serial@count=\count138
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicst
+ate.code.tex
+File: pgfcoregraphicstate.code.tex 2014/11/02 (rcs-revision 1.12)
+\pgflinewidth=\dimen170
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransform
+ations.code.tex
+File: pgfcoretransformations.code.tex 2015/08/07 (rcs-revision 1.20)
+\pgf@pt@x=\dimen171
+\pgf@pt@y=\dimen172
+\pgf@pt@temp=\dimen173
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.cod
+e.tex
+File: pgfcorequick.code.tex 2008/10/09 (rcs-revision 1.3)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.c
+ode.tex
+File: pgfcoreobjects.code.tex 2006/10/11 (rcs-revision 1.2)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathproce
+ssing.code.tex
+File: pgfcorepathprocessing.code.tex 2013/09/09 (rcs-revision 1.9)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.co
+de.tex
+File: pgfcorearrows.code.tex 2015/05/14 (rcs-revision 1.43)
+\pgfarrowsep=\dimen174
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.cod
+e.tex
+File: pgfcoreshade.code.tex 2013/07/15 (rcs-revision 1.15)
+\pgf@max=\dimen175
+\pgf@sys@shading@range@num=\count139
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.cod
+e.tex
+File: pgfcoreimage.code.tex 2013/07/15 (rcs-revision 1.18)
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.
+code.tex
+File: pgfcoreexternal.code.tex 2014/07/09 (rcs-revision 1.21)
+\pgfexternal@startupbox=\box67
+))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.co
+de.tex
+File: pgfcorelayers.code.tex 2013/07/18 (rcs-revision 1.7)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretranspare
+ncy.code.tex
+File: pgfcoretransparency.code.tex 2013/09/30 (rcs-revision 1.5)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.
+code.tex
+File: pgfcorepatterns.code.tex 2013/11/07 (rcs-revision 1.5)
+)))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.cod
+e.tex
+File: pgfmoduleshapes.code.tex 2014/03/21 (rcs-revision 1.35)
+\pgfnodeparttextbox=\box68
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.
+tex
+File: pgfmoduleplot.code.tex 2015/08/03 (rcs-revision 1.13)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version
+-0-65.sty
+Package: pgfcomp-version-0-65 2007/07/03 v3.0.1a (rcs-revision 1.7)
+\pgf@nodesepstart=\dimen176
+\pgf@nodesepend=\dimen177
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version
+-1-18.sty
+Package: pgfcomp-version-1-18 2007/07/23 v3.0.1a (rcs-revision 1.1)
+))
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/utilities/pgffor.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex))
+ (/usr/local/texlive/2018/texmf-dist/tex/latex/pgf/math/pgfmath.sty
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex
+Package: pgffor 2013/12/13 v3.0.1a (rcs-revision 1.25)
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)
+\pgffor@iter=\dimen178
+\pgffor@skip=\dimen179
+\pgffor@stack=\toks37
+\pgffor@toks=\toks38
+))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.cod
+e.tex
+Package: tikz 2015/08/07 v3.0.1a (rcs-revision 1.151)
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothan
+dlers.code.tex
+File: pgflibraryplothandlers.code.tex 2013/08/31 v3.0.1a (rcs-revision 1.20)
+\pgf@plot@mark@count=\count140
+\pgfplotmarksize=\dimen180
+)
+\tikz@lastx=\dimen181
+\tikz@lasty=\dimen182
+\tikz@lastxsaved=\dimen183
+\tikz@lastysaved=\dimen184
+\tikzleveldistance=\dimen185
+\tikzsiblingdistance=\dimen186
+\tikz@figbox=\box69
+\tikz@figbox@bg=\box70
+\tikz@tempbox=\box71
+\tikz@tempbox@bg=\box72
+\tikztreelevel=\count141
+\tikznumberofchildren=\count142
+\tikznumberofcurrentchild=\count143
+\tikz@fig@count=\count144
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.cod
+e.tex
+File: pgfmodulematrix.code.tex 2013/09/17 (rcs-revision 1.8)
+\pgfmatrixcurrentrow=\count145
+\pgfmatrixcurrentcolumn=\count146
+\pgf@matrix@numberofcolumns=\count147
+)
+\tikz@expandcount=\count148
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/frontendlayer/tikz/librarie
+s/tikzlibrarytopaths.code.tex
+File: tikzlibrarytopaths.code.tex 2008/06/17 v3.0.1a (rcs-revision 1.2)
+)))
+(/usr/local/texlive/2018/texmf-dist/tex/generic/pgf/frontendlayer/tikz/librarie
+s/tikzlibrarypositioning.code.tex
+File: tikzlibrarypositioning.code.tex 2008/10/06 v3.0.1a (rcs-revision 1.7)
+) (./pdfsetup.sty)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/hyperref/hyperref.sty
+Package: hyperref 2018/02/06 v6.86b Hypertext links for LaTeX
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
+Package: hobsub-hyperref 2016/05/16 v1.14 Bundle oberdiek, subset hyperref (HO)
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty
+Package: hobsub-generic 2016/05/16 v1.14 Bundle oberdiek, subset generic (HO)
+Package: hobsub 2016/05/16 v1.14 Construct package bundles (HO)
+Package: infwarerr 2016/05/16 v1.4 Providing info/warning/error messages (HO)
+Package: ltxcmds 2016/05/16 v1.23 LaTeX kernel commands for general use (HO)
+Package: ifluatex 2016/05/16 v1.4 Provides the ifluatex switch (HO)
+Package ifluatex Info: LuaTeX detected.
+Package: ifvtex 2016/05/16 v1.6 Detect VTeX and its facilities (HO)
+Package ifvtex Info: VTeX not detected.
+Package: intcalc 2016/05/16 v1.2 Expandable calculations with integers (HO)
+Package: ifpdf 2017/03/15 v3.2 Provides the ifpdf switch
+Package: etexcmds 2016/05/16 v1.6 Avoid name clashes with e-TeX commands (HO)
+Package: kvsetkeys 2016/05/16 v1.17 Key value parser (HO)
+Package: kvdefinekeys 2016/05/16 v1.4 Define keys (HO)
+Package: luatex-loader 2016/05/16 v0.6 Lua module loader (HO)
+
+(/usr/local/texlive/2018/texmf-dist/scripts/oberdiek/oberdiek.luatex.lua)
+Package: pdftexcmds 2018/01/30 v0.27 Utility functions of pdfTeX for LuaTeX (HO)
+
+Package pdftexcmds Info: \pdf@primitive is available.
+Package pdftexcmds Info: \pdf@ifprimitive is available.
+Package pdftexcmds Info: \pdfdraftmode found.
+\pdftexcmds@toks=\toks39
+Package: pdfescape 2016/05/16 v1.14 Implements pdfTeX's escape features (HO)
+Package: bigintcalc 2016/05/16 v1.4 Expandable calculations on big integers (HO)
+
+Package: bitset 2016/05/16 v1.2 Handle bit-vector datatype (HO)
+Package: uniquecounter 2016/05/16 v1.3 Provide unlimited unique counter (HO)
+)
+Package hobsub Info: Skipping package `hobsub' (already loaded).
+Package: letltxmacro 2016/05/16 v1.5 Let assignment for LaTeX macros (HO)
+Package: hopatch 2016/05/16 v1.3 Wrapper for package hooks (HO)
+Package: xcolor-patch 2016/05/16 xcolor patch
+Package: atveryend 2016/05/16 v1.9 Hooks at the very end of document (HO)
+Package atveryend Info: \enddocument detected (standard20110627).
+Package: atbegshi 2016/06/09 v1.18 At begin shipout hook (HO)
+Package: refcount 2016/05/16 v3.5 Data extraction from label references (HO)
+Package: hycolor 2016/05/16 v1.8 Color options for hyperref/bookmark (HO)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/generic/ifxetex/ifxetex.sty
+Package: ifxetex 2010/09/12 v0.6 Provides ifxetex conditional
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/oberdiek/auxhook.sty
+Package: auxhook 2016/05/16 v1.4 Hooks for auxiliary files (HO)
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/oberdiek/kvoptions.sty
+Package: kvoptions 2016/05/16 v3.12 Key value format for package options (HO)
+)
+\@linkdim=\dimen187
+\Hy@linkcounter=\count149
+\Hy@pagecounter=\count150
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/hyperref/pd1enc.def
+File: pd1enc.def 2018/02/06 v6.86b Hyperref: PDFDocEncoding definition (HO)
+)
+\Hy@SavedSpaceFactor=\count151
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/latexconfig/hyperref.cfg
+File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive
+)
+Package hyperref Info: Option `colorlinks' set `true' on input line 4383.
+Package hyperref Info: Option `pdfpagelabels' set `true' on input line 4383.
+Package hyperref Info: Hyper figures OFF on input line 4509.
+Package hyperref Info: Link nesting OFF on input line 4514.
+Package hyperref Info: Hyper index ON on input line 4517.
+Package hyperref Info: Plain pages OFF on input line 4524.
+Package hyperref Info: Backreferencing OFF on input line 4529.
+Package hyperref Info: Implicit mode ON; LaTeX internals redefined.
+Package hyperref Info: Bookmarks ON on input line 4762.
+\c@Hy@tempcnt=\count152
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/url/url.sty
+\Urlmuskip=\muskip11
+Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc.
+)
+LaTeX Info: Redefining \url on input line 5115.
+\XeTeXLinkMargin=\dimen188
+\Fld@menulength=\count153
+\Field@Width=\dimen189
+\Fld@charsize=\dimen190
+Package hyperref Info: Hyper figures OFF on input line 6369.
+Package hyperref Info: Link nesting OFF on input line 6374.
+Package hyperref Info: Hyper index ON on input line 6377.
+Package hyperref Info: backreferencing OFF on input line 6384.
+Package hyperref Info: Link coloring ON on input line 6387.
+Package hyperref Info: Link coloring with OCG OFF on input line 6394.
+Package hyperref Info: PDF/A mode OFF on input line 6399.
+LaTeX Info: Redefining \ref on input line 6439.
+LaTeX Info: Redefining \pageref on input line 6443.
+\Hy@abspage=\count154
+\c@Item=\count155
+\c@Hfootnote=\count156
+)
+Package hyperref Info: Driver (autodetected): hluatex.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/hyperref/hluatex.def
+File: hluatex.def 2018/02/06 v6.86b Hyperref driver for luaTeX
+\Fld@listcount=\count157
+\c@bookmark@seq@number=\count158
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty
+Package: rerunfilecheck 2016/05/16 v1.8 Rerun checks for auxiliary files (HO)
+Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 28
+2.
+)
+\Hy@SectionHShift=\skip50
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty
+Package: stmaryrd 1994/03/03 St Mary's Road symbol package
+\symstmry=\mathgroup6
+LaTeX Font Info: Overwriting symbol font `stmry' in version `bold'
+(Font) U/stmry/m/n --> U/stmry/b/n on input line 89.
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/tipa/tipa.sty
+Package: tipa 2002/08/08 TIPA version 1.1
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/base/fontenc.sty
+Package: fontenc 2017/04/05 v2.0i Standard LaTeX package
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/tipa/t3enc.def
+File: t3enc.def 2001/12/31 T3 encoding
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmromanslant10-regular.luc)(load luc: /Users/cstan/Library/texlive/2018/te
+xmf-var/luatex-cache/generic/fonts/otl/lmroman10-italic.luc)(load luc: /Users/cs
+tan/Library/texlive/2018/texmf-var/luatex-cache/generic/fonts/otl/lmroman10-bold
+.luc)
+LaTeX Font Info: Try loading font information for TU+phv on input line 357.
+LaTeX Font Info: No file TUphv.fd. on input line 357.
+
+
+LaTeX Font Warning: Font shape `TU/phv/m/n' undefined
+(Font) using `TU/lmr/m/n' instead on input line 357.
+
+) (/usr/local/texlive/2018/texmf-dist/tex/latex/base/tuenc.def
+File: tuenc.def 2017/04/05 v2.0i Standard LaTeX file
+LaTeX Font Info: Redeclaring font encoding TU on input line 82.
+)))
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/mathpazo.sty
+Package: mathpazo 2005/04/12 PSNFSS-v9.2a Palatino w/ Pazo Math (D.Puga, WaS)
+\symupright=\mathgroup7
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/fontspec/fontspec.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
+(/usr/local/texlive/2018/texmf-dist/tex/latex/l3kernel/expl3.sty
+Package: expl3 2018/03/05 L3 programming layer (loader)
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/l3kernel/expl3-code.tex
+Package: expl3 2018/03/05 L3 programming layer (code)
+\ucharcat@table=\catcodetable5
+\c_max_int=\count159
+\l_tmpa_int=\count160
+\l_tmpb_int=\count161
+\g_tmpa_int=\count162
+\g_tmpb_int=\count163
+\g__intarray_font_int=\count164
+\g__prg_map_int=\count165
+\c_log_iow=\count166
+\l_iow_line_count_int=\count167
+\l__iow_line_target_int=\count168
+\l__iow_one_indent_int=\count169
+\l__iow_indent_int=\count170
+\c_zero_dim=\dimen191
+\c_max_dim=\dimen192
+\l_tmpa_dim=\dimen193
+\l_tmpb_dim=\dimen194
+\g_tmpa_dim=\dimen195
+\g_tmpb_dim=\dimen196
+\c_zero_skip=\skip51
+\c_max_skip=\skip52
+\l_tmpa_skip=\skip53
+\l_tmpb_skip=\skip54
+\g_tmpa_skip=\skip55
+\g_tmpb_skip=\skip56
+\c_zero_muskip=\muskip12
+\c_max_muskip=\muskip13
+\l_tmpa_muskip=\muskip14
+\l_tmpb_muskip=\muskip15
+\g_tmpa_muskip=\muskip16
+\g_tmpb_muskip=\muskip17
+\l_keys_choice_int=\count171
+\c__fp_leading_shift_int=\count172
+\c__fp_middle_shift_int=\count173
+\c__fp_trailing_shift_int=\count174
+\c__fp_big_leading_shift_int=\count175
+\c__fp_big_middle_shift_int=\count176
+\c__fp_big_trailing_shift_int=\count177
+\c__fp_Bigg_leading_shift_int=\count178
+\c__fp_Bigg_middle_shift_int=\count179
+\c__fp_Bigg_trailing_shift_int=\count180
+\c__fp_rand_size_int=\count181
+\c__fp_rand_four_int=\count182
+\c__fp_rand_eight_int=\count183
+\l__sort_length_int=\count184
+\l__sort_min_int=\count185
+\l__sort_top_int=\count186
+\l__sort_max_int=\count187
+\l__sort_true_max_int=\count188
+\l__sort_block_int=\count189
+\l__sort_begin_int=\count190
+\l__sort_end_int=\count191
+\l__sort_A_int=\count192
+\l__sort_B_int=\count193
+\l__sort_C_int=\count194
+\l__tl_build_start_index_int=\count195
+\l__tl_build_index_int=\count196
+\l__tl_analysis_normal_int=\count197
+\l__tl_analysis_index_int=\count198
+\l__tl_analysis_nesting_int=\count199
+\l__tl_analysis_type_int=\count266
+\l__regex_internal_a_int=\count267
+\l__regex_internal_b_int=\count268
+\l__regex_internal_c_int=\count269
+\l__regex_balance_int=\count270
+\l__regex_group_level_int=\count271
+\l__regex_mode_int=\count272
+\c__regex_cs_in_class_mode_int=\count273
+\c__regex_cs_mode_int=\count274
+\l__regex_catcodes_int=\count275
+\l__regex_default_catcodes_int=\count276
+\c__regex_catcode_L_int=\count277
+\c__regex_catcode_O_int=\count278
+\c__regex_catcode_A_int=\count279
+\c__regex_all_catcodes_int=\count280
+\l__regex_show_lines_int=\count281
+\l__regex_min_state_int=\count282
+\l__regex_max_state_int=\count283
+\l__regex_left_state_int=\count284
+\l__regex_right_state_int=\count285
+\l__regex_capturing_group_int=\count286
+\l__regex_min_pos_int=\count287
+\l__regex_max_pos_int=\count288
+\l__regex_curr_pos_int=\count289
+\l__regex_start_pos_int=\count290
+\l__regex_success_pos_int=\count291
+\l__regex_curr_char_int=\count292
+\l__regex_curr_catcode_int=\count293
+\l__regex_last_char_int=\count294
+\l__regex_case_changed_char_int=\count295
+\l__regex_curr_state_int=\count296
+\l__regex_step_int=\count297
+\l__regex_min_active_int=\count298
+\l__regex_max_active_int=\count299
+\l__regex_replacement_csnames_int=\count300
+\l__regex_match_count_int=\count301
+\l__regex_min_submatch_int=\count302
+\l__regex_submatch_int=\count303
+\l__regex_zeroth_submatch_int=\count304
+\g__regex_trace_regex_int=\count305
+\c_empty_box=\box73
+\l_tmpa_box=\box74
+\l_tmpb_box=\box75
+\g_tmpa_box=\box76
+\g_tmpb_box=\box77
+\l__box_top_dim=\dimen197
+\l__box_bottom_dim=\dimen198
+\l__box_left_dim=\dimen199
+\l__box_right_dim=\dimen256
+\l__box_top_new_dim=\dimen257
+\l__box_bottom_new_dim=\dimen258
+\l__box_left_new_dim=\dimen259
+\l__box_right_new_dim=\dimen260
+\l__box_internal_box=\box78
+\l__coffin_internal_box=\box79
+\l__coffin_internal_dim=\dimen261
+\l__coffin_offset_x_dim=\dimen262
+\l__coffin_offset_y_dim=\dimen263
+\l__coffin_x_dim=\dimen264
+\l__coffin_y_dim=\dimen265
+\l__coffin_x_prime_dim=\dimen266
+\l__coffin_y_prime_dim=\dimen267
+\c_empty_coffin=\box80
+\l__coffin_aligned_coffin=\box81
+\l__coffin_aligned_internal_coffin=\box82
+\l_tmpa_coffin=\box83
+\l_tmpb_coffin=\box84
+\l__coffin_display_coffin=\box85
+\l__coffin_display_coord_coffin=\box86
+\l__coffin_display_pole_coffin=\box87
+\l__coffin_display_offset_dim=\dimen268
+\l__coffin_display_x_dim=\dimen269
+\l__coffin_display_y_dim=\dimen270
+\l__coffin_bounding_shift_dim=\dimen271
+\l__coffin_left_corner_dim=\dimen272
+\l__coffin_right_corner_dim=\dimen273
+\l__coffin_bottom_corner_dim=\dimen274
+\l__coffin_top_corner_dim=\dimen275
+\l__coffin_scaled_total_height_dim=\dimen276
+\l__coffin_scaled_width_dim=\dimen277
+)
+(/usr/local/texlive/2018/texmf-dist/tex/latex/l3kernel/l3pdfmode.def
+File: l3pdfmode.def 2017/03/18 v L3 Experimental driver: PDF mode
+\l__driver_color_stack_int=\count306
+))
+Package: xparse 2018/02/21 L3 Experimental document command parser
+\l__xparse_current_arg_int=\count307
+\g__xparse_grabber_int=\count308
+\l__xparse_m_args_int=\count309
+\l__xparse_mandatory_args_int=\count310
+\l__xparse_v_nesting_int=\count311
+)
+Package: fontspec 2017/11/09 v2.6g Font selection for XeLaTeX and LuaLaTeX
+Lua module: fontspec 2017/11/09 2.6g Font selection for XeLaTeX and LuaLaTeX
+(/usr/local/texlive/2018/texmf-dist/tex/latex/fontspec/fontspec-luatex.sty
+Package: fontspec-luatex 2017/11/09 v2.6g Font selection for XeLaTeX and LuaLaTe
+X
+\l__fontspec_script_int=\count312
+\l__fontspec_language_int=\count313
+\l__fontspec_strnum_int=\count314
+\l__fontspec_tmp_int=\count315
+\l__fontspec_em_int=\count316
+\l__fontspec_emdef_int=\count317
+\l__fontspec_strong_int=\count318
+\l__fontspec_strongdef_int=\count319
+\l__fontspec_tmpa_dim=\dimen278
+\l__fontspec_tmpb_dim=\dimen279
+\l__fontspec_tmpc_dim=\dimen280
+\g__file_internal_ior=\read2
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/base/fontenc.sty
+Package: fontenc 2017/04/05 v2.0i Standard LaTeX package
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/base/tuenc.def
+File: tuenc.def 2017/04/05 v2.0i Standard LaTeX file
+LaTeX Font Info: Redeclaring font encoding TU on input line 82.
+))
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \fontspec with sig. 'O{}mO{}' on line 545.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setmainfont with sig. 'O{}mO{}' on line 549.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setsansfont with sig. 'O{}mO{}' on line 553.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setmonofont with sig. 'O{}mO{}' on line 557.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setmathrm with sig. 'O{}mO{}' on line 561.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setboldmathrm with sig. 'O{}mO{}' on line 565.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setmathsf with sig. 'O{}mO{}' on line 569.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setmathtt with sig. 'O{}mO{}' on line 573.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \setromanfont with sig. 'O{}mO{}' on line 577.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newfontfamily with sig. 'mO{}mO{}' on line 581.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newfontface with sig. 'mO{}mO{}' on line 585.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \defaultfontfeatures with sig. 't+om' on line 589.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \addfontfeatures with sig. 'm' on line 593.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \addfontfeature with sig. 'm' on line 597.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newfontfeature with sig. 'mm' on line 601.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newAATfeature with sig. 'mmmm' on line 605.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newopentypefeature with sig. 'mmm' on line 609.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newICUfeature with sig. 'mmm' on line 613.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \aliasfontfeature with sig. 'mm' on line 617.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \aliasfontfeatureoption with sig. 'mmm' on line 621.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newfontscript with sig. 'mm' on line 625.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \newfontlanguage with sig. 'mm' on line 629.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \DeclareFontsExtensions with sig. 'm' on line 633.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \IfFontFeatureActiveTF with sig. 'mmm' on line 637.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \EncodingCommand with sig. 'mO{}m' on line 3366.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \EncodingAccent with sig. 'mm' on line 3372.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \EncodingSymbol with sig. 'mm' on line 3378.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \EncodingComposite with sig. 'mmm' on line 3384.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \EncodingCompositeCommand with sig. 'mmm' on line 3390.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \DeclareUnicodeEncoding with sig. 'mm' on line 3415.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \UndeclareSymbol with sig. 'm' on line 3421.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \UndeclareAccent with sig. 'm' on line 3427.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \UndeclareCommand with sig. 'm' on line 3433.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \UndeclareComposite with sig. 'mm' on line 3440.
+.................................................
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/fontspec/fontspec.cfg)
+LaTeX Info: Redefining \itshape on input line 3625.
+LaTeX Info: Redefining \slshape on input line 3630.
+LaTeX Info: Redefining \scshape on input line 3635.
+LaTeX Info: Redefining \upshape on input line 3640.
+LaTeX Info: Redefining \em on input line 3670.
+LaTeX Info: Redefining \emph on input line 3695.
+LaTeX Info: Redefining \- on input line 3749.
+.................................................
+. LaTeX info: "xparse/redefine-command"
+.
+. Redefining command \oldstylenums with sig. 'm' on line 3844.
+.................................................
+.................................................
+. LaTeX info: "xparse/define-command"
+.
+. Defining command \liningnums with sig. 'm' on line 3848.
+.................................................
+))
+\c@falsehood=\count320
+\c@conject=\count321
+
+(./root.aux)
+\openout1 = root.aux
+
+LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for TU/lmr/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 42.
+LaTeX Font Info: ... okay on input line 42.
+LaTeX Font Info: Checking defaults for T3/cmr/m/n on input line 42.
+LaTeX Font Info: Try loading font information for T3+cmr on input line 42.
+ (/usr/local/texlive/2018/texmf-dist/tex/latex/tipa/t3cmr.fd
+File: t3cmr.fd 2001/12/31 TIPA font definitions
+)
+LaTeX Font Info: ... okay on input line 42.
+
+ABD: EveryShipout initializing macros
+(/usr/local/texlive/2018/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count322
+\scratchdimen=\dimen281
+\scratchbox=\box88
+\nofMPsegments=\count323
+\nofMParguments=\count324
+\everyMPshowfont=\toks40
+\MPscratchCnt=\count325
+\MPscratchDim=\dimen282
+\MPnumerator=\count326
+\makeMPintoPDFobject=\count327
+\everyMPtoPDFconversion=\toks41
+) (/usr/local/texlive/2018/texmf-dist/tex/latex/oberdiek/epstopdf-base.sty
+Package: epstopdf-base 2016/05/15 v2.6 Base part for package epstopdf
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/oberdiek/grfext.sty
+Package: grfext 2016/05/16 v1.2 Manage graphics extensions (HO)
+)
+Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 43
+8.
+Package grfext Info: Graphics extension search list:
+(grfext) [.pdf,.png,.jpg,.mps,.jpeg,.jbig2,.jb2,.PDF,.PNG,.JPG,.JPEG
+,.JBIG2,.JB2,.eps]
+(grfext) \AppendGraphicsExtensions on input line 456.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
+File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live
+
+))
+\AtBeginShipoutBox=\box89
+Package hyperref Info: Link coloring ON on input line 42.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/hyperref/nameref.sty
+Package: nameref 2016/05/21 v2.44 Cross-referencing by name of section
+
+(/usr/local/texlive/2018/texmf-dist/tex/generic/oberdiek/gettitlestring.sty
+Package: gettitlestring 2016/05/16 v1.5 Cleanup title references (HO)
+)
+\c@section@level=\count328
+)
+LaTeX Info: Redefining \ref on input line 42.
+LaTeX Info: Redefining \pageref on input line 42.
+LaTeX Info: Redefining \nameref on input line 42.
+
+(./root.out) (./root.out)
+\@outlinefile=\write5
+
+\openout5 = root.out
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman9-regular.luc)
+LaTeX Font Info: Try loading font information for OT1+pplx on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/ot1pplx.fd
+File: ot1pplx.fd 2004/09/06 font definitions for OT1/pplx.
+)
+LaTeX Font Info: Try loading font information for OML+zplm on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/omlzplm.fd
+File: omlzplm.fd 2002/09/08 Fontinst v1.914 font definitions for OML/zplm.
+)
+LaTeX Font Info: Try loading font information for OMS+zplm on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/omszplm.fd
+File: omszplm.fd 2002/09/08 Fontinst v1.914 font definitions for OMS/zplm.
+)
+LaTeX Font Info: Try loading font information for OMX+zplm on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/omxzplm.fd
+File: omxzplm.fd 2002/09/08 Fontinst v1.914 font definitions for OMX/zplm.
+)
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 9.37807pt on input line 57.
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 7.29405pt on input line 57.
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 5.21004pt on input line 57.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 9.37807pt on input line 57.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 7.29405pt on input line 57.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 5.21004pt on input line 57.
+LaTeX Font Info: Try loading font information for U+stmry on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
+LaTeX Font Info: Try loading font information for OT1+zplm on input line 57.
+
+(/usr/local/texlive/2018/texmf-dist/tex/latex/psnfss/ot1zplm.fd
+File: ot1zplm.fd 2002/09/08 Fontinst v1.914 font definitions for OT1/zplm.
+)(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/fon
+ts/otl/lmroman7-regular.luc)(load luc: /Users/cstan/Library/texlive/2018/texmf-v
+ar/luatex-cache/generic/fonts/otl/lmroman9-bold.luc)
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 1 undefined on input li
+ne 57.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 1 undefined on input line 57.
+
+
+LaTeX Warning: Citation `OkuiSuzukiTech' on page 1 undefined on input line 57.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 1 undefined on input line 57.
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman12-regular.luc)(load luc: /Users/cstan/Library/texlive/2018/texmf-v
+ar/luatex-cache/generic/fonts/otl/lmroman12-bold.luc)
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 10.42007pt on input line 69.
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 7.91925pt on input line 69.
+LaTeX Font Info: Font shape `U/msa/m/n' will be
+(Font) scaled to size 6.25204pt on input line 69.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 10.42007pt on input line 69.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 7.91925pt on input line 69.
+LaTeX Font Info: Font shape `U/msb/m/n' will be
+(Font) scaled to size 6.25204pt on input line 69.
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmmono9-regular.luc)(load luc: /Users/cstan/Library/texlive/2018/texmf-var
+/luatex-cache/generic/fonts/otl/lmroman9-italic.luc) (./session.tex (./RegLangs
+.tex) (./Spec.tex)
+(./Lexer.tex) (./Simplifying.tex) (./Sulzmann.tex) (./Positions.tex)
+(./SizeBound.tex [1
+
+{/usr/local/texlive/2018/texmf-var/fonts/map/pdftex/updmap/pdftex.map}](load luc
+: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/fonts/otl/lmr
+oman8-italic.luc)(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-c
+ache/generic/fonts/otl/lmroman7-italic.luc) [2] [3]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [4]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [5]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [6]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [7]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [8]
+Overfull \hbox (10.05669pt too wide) in paragraph at lines 776--778
+[][] \TU/lmr/bx/n/10 ap-ply$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 auto simp add
+$\OT1/zplm/m/n/10 :$ \TU/lmr/m/it/10 bnul-lable[]correctness mkeps[]nullable re
+-trieve[]fuse2$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Overfull \hbox (24.20656pt too wide) in paragraph at lines 780--782
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 smt bnul-lable
+$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 4$
+\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lable[]correctness erase$\OT1/pplx/m/n
+/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 5$\OT1/zplm/m/n/
+10 )$ \TU/lmr/m/it/10 erase$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/
+m/n/10 ($\TU/lmr/m/it/10 6$\OT1/zplm/m/n/10 )$
+ []
+
+
+Overfull \hbox (21.52992pt too wide) in paragraph at lines 786--788
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 smt ap-pend[]N
+il2 bnul-lable$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/
+lmr/m/it/10 4$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lable[]correctness erase
+$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 5$
+\OT1/zplm/m/n/10 )$
+ []
+
+
+Overfull \hbox (1.98334pt too wide) in paragraph at lines 814--816
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend[
+]Nil2 bnul-lable[]correctness erase$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\O
+T1/zplm/m/n/10 ($\TU/lmr/m/it/10 6$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 erase[]f
+use
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [9]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [10]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [11]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [12]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [13]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [14]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [15]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [16]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [17]
+Overfull \hbox (45.00008pt too wide) in paragraph at lines 1700--1713
+[][] \TU/lmr/bx/n/10 by $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis L[]bders[]si
+mp bnul-lable[]correctness lexer$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/
+zplm/m/n/10 ($\TU/lmr/m/it/10 1$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 lexer[]corr
+ect[]None
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [18]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [19]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [20]
+Overfull \hbox (72.57005pt too wide) in paragraph at lines 2035--2037
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend
+$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 assoc b2 bnul-lable[]correctness erase[]fus
+e bnul-lable[]Hdbmkeps[]Hd$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Overfull \hbox (10.72014pt too wide) in paragraph at lines 2120--2122
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis L[]erase
+[]AALTs L[]erase[]flts L[]flat[]Prf1 L[]flat[]Prf2
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [21]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [22]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [23]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [24]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [25]
+Overfull \hbox (6.40976pt too wide) in paragraph at lines 2633--2641
+[][] \TU/lmr/bx/n/10 ap-ply$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 induction ra$ [
+] $r1 rb$ [] $AZERO ar-bi-trary$\OT1/zplm/m/n/10 :$ \TU/lmr/m/it/10 bs1 r1 r2 r
+ule$\OT1/zplm/m/n/10 :$ \TU/lmr/m/it/10 rrewrites$\OT1/pplx/m/n/10 .$\TU/lmr/m/
+it/10 induct$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [26]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [27]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [28]
+Overfull \hbox (9.2633pt too wide) in paragraph at lines 2921--2923
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend[
+]Nil flts$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m
+/it/10 2$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 many[]steps[]later rrewrite$\OT1/p
+plx/m/n/10 .$\TU/lmr/m/it/10 intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 7$\OT1/z
+plm/m/n/10 )$$)$[]
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [29]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [30]
+Overfull \hbox (47.09676pt too wide) in paragraph at lines 3142--3144
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 smt $\OT1/zplm
+/m/n/10 ($\TU/lmr/m/it/10 verit$\OT1/pplx/m/n/10 ,$ \TU/lmr/m/it/10 ccfv[]thres
+hold$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 ap-pend[]Cons ap-pend[]assoc ap-pend[]
+self[]conv2
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [31]
+Overfull \hbox (6.43988pt too wide) in paragraph at lines 3238--3240
+[][] \TU/lmr/bx/n/10 ap-ply$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 subgoal[]tac AA
+LTs bs1 $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 flts $\OT1/zplm/m/n/10 ($\TU/lmr/m/
+it/10 map bsimp rs$\OT1/zplm/m/n/10 )$$)$ $\U/msa/m/n/10 $$\OMS/zplm/m/n/10 $
+ \TU/lmr/m/it/10 AALTs bs1 $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 distinctBy
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [32]
+Overfull \hbox (27.40672pt too wide) in paragraph at lines 3304--3311
+[][] \TU/lmr/bx/n/10 by $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 smt $\OT1/zplm/m/n
+/10 ($\TU/lmr/m/it/10 z3$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 Un[]iff bnul-lable
+[]correctness in-sert[]iff list$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 set$\OT1/zpl
+m/m/n/10 ($\TU/lmr/m/it/10 2$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 qq3 set[]appen
+d$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [33]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [34]
+Overfull \hbox (11.15656pt too wide) in paragraph at lines 3559--3561
+[][]\TU/lmr/bx/n/10 lemma \TU/lmr/m/it/10 third[]segment[]bnullable$\OT1/zplm/m
+/n/10 :$ $[]$\TU/lmr/m/it/10 bnul-lable $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 AAL
+Ts bs $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 rs1$\OT1/pplx/m/n/10 @$\TU/lmr/m/it/1
+0 rs2$\OT1/pplx/m/n/10 @$\TU/lmr/m/it/10 rs3$\OT1/zplm/m/n/10 )$$)$$\OT1/pplx/m
+/n/10 ;$ $\OMS/zplm/m/n/10 :$\TU/lmr/m/it/10 bnul-
+ []
+
+
+Overfull \hbox (30.67331pt too wide) in paragraph at lines 3565--3576
+[][] \TU/lmr/bx/n/10 by $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend$\OT1
+/pplx/m/n/10 .$\TU/lmr/m/it/10 left[]neutral ap-pend[]Cons bnul-lable$\OT1/pplx
+/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 1$\OT1/zplm/
+m/n/10 )$ \TU/lmr/m/it/10 bnul-lable[]segment
+ []
+
+
+Overfull \hbox (6.39323pt too wide) in paragraph at lines 3580--3582
+[][]\TU/lmr/bx/n/10 lemma \TU/lmr/m/it/10 third[]segment[]bmkeps$\OT1/zplm/m/n/
+10 :$ $[]$\TU/lmr/m/it/10 bnul-lable $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 AALTs
+ bs $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 rs1$\OT1/pplx/m/n/10 @$\TU/lmr/m/it/10
+rs2$\OT1/pplx/m/n/10 @$\TU/lmr/m/it/10 rs3$\OT1/zplm/m/n/10 )$$)$$\OT1/pplx/m/n
+/10 ;$ $\OMS/zplm/m/n/10 :$\TU/lmr/m/it/10 bnul-
+ []
+
+
+Overfull \hbox (25.44008pt too wide) in paragraph at lines 3601--3603
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend$
+\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 assoc in[]set[]conv[]decomp r2 third[]segmen
+t[]bnullable$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Overfull \hbox (31.5301pt too wide) in paragraph at lines 3643--3645
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 smt $\OT1/zplm
+/m/n/10 ($\TU/lmr/m/it/10 verit$\OT1/pplx/m/n/10 ,$ \TU/lmr/m/it/10 ccfv[]thres
+hold$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 ap-pend[]eq[]append[]conv2 list$\OT1/p
+plx/m/n/10 .$\TU/lmr/m/it/10 set[]intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 1$\
+OT1/zplm/m/n/10 )$
+ []
+
+
+Overfull \hbox (1.18669pt too wide) in paragraph at lines 3643--3645
+\TU/lmr/m/it/10 qq2 qq3 rewritenul-lable rrewrite$\OT1/pplx/m/n/10 .$\TU/lmr/m/
+it/10 intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 8$\OT1/zplm/m/n/10 )$ \TU/lmr/m
+/it/10 self[]append[]conv2 spillbmkep-slistr$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [35]
+Overfull \hbox (12.19328pt too wide) in paragraph at lines 3654--3656
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis ap-pend[
+]Cons ap-pend[]Nil bnul-lable$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zpl
+m/m/n/10 ($\TU/lmr/m/it/10 1$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lable[]se
+gment
+ []
+
+
+Overfull \hbox (94.37671pt too wide) in paragraph at lines 3657--3664
+[][] \TU/lmr/bx/n/10 by $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis bnul-lable$\
+OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 4$\O
+T1/zplm/m/n/10 )$ \TU/lmr/m/it/10 rewrite[]non[]nullable rrewrite$\OT1/pplx/m/n
+/10 .$\TU/lmr/m/it/10 intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 10$\OT1/zplm/m/
+n/10 )$ \TU/lmr/m/it/10 third[]segment[]bmkeps$\OT1/zplm/m/n/10 )$[]
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [36]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [37]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [38]
+Overfull \hbox (17.27003pt too wide) in paragraph at lines 4067--4069
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 meson con-tex-
+trewrites1 r[]in[]rstar rrewrite$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 intros$\OT1
+/zplm/m/n/10 ($\TU/lmr/m/it/10 11$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 rrewrite$
+\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 2$
+\OT1/zplm/m/n/10 )$
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [39]
+Overfull \hbox (52.87671pt too wide) in paragraph at lines 4155--4157
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis bder$\OT
+1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 4$\OT1
+/zplm/m/n/10 )$ \TU/lmr/m/it/10 bder[]fuse[]list map[]map r[]in[]rstar rrewrite
+$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 intros$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 9
+$\OT1/zplm/m/n/10 )$$)$[]
+ []
+
+
+Overfull \hbox (30.75671pt too wide) in paragraph at lines 4158--4160
+[][] \TU/lmr/bx/n/10 ap-ply $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis List$\OT
+1/pplx/m/n/10 .$\TU/lmr/m/it/10 map$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 composit
+ionality bder$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/l
+mr/m/it/10 4$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bder[]fuse[]list r[]in[]rstar
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [40]
+Overfull \hbox (31.29991pt too wide) in paragraph at lines 4223--4230
+[][] \TU/lmr/bx/n/10 by $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 metis bders$\OT1/p
+plx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 1$\OT1/zp
+lm/m/n/10 )$ \TU/lmr/m/it/10 bders$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT
+1/zplm/m/n/10 ($\TU/lmr/m/it/10 2$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bders[]si
+mp$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10
+1$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bders[]simp$\OT1/pplx/m/n/10 .$\TU/lmr/m/
+it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 2$\OT1/zplm/m/n/10 )$
+ []
+
+) (./Paper.tex
+
+LaTeX Warning: Citation `Brzozowski1964' on page 41 undefined on input line 82.
+
+
+LaTeX Warning: Citation `Owens2008' on page 41 undefined on input line 96.
+
+
+LaTeX Warning: Citation `Krauss2011' on page 41 undefined on input line 97.
+
+
+LaTeX Warning: Citation `Coquand2012' on page 41 undefined on input line 98.
+
+[41]
+
+LaTeX Warning: Citation `Frisch2004' on page 42 undefined on input line 103.
+
+
+LaTeX Warning: Citation `POSIX' on page 42 undefined on input line 104.
+
+
+LaTeX Warning: Citation `Kuklewicz' on page 42 undefined on input line 104.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 42 undefined on input line 104.
+
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 42 undefined on input line 104.
+
+
+LaTeX Warning: Citation `Vansummeren2006' on page 42 undefined on input line 104
+.
+
+
+LaTeX Warning: Citation `POSIX' on page 42 undefined on input line 121.
+
+[42]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 43 undefined on input line 160.
+
+
+LaTeX Warning: Citation `HosoyaVouillonPierce2005' on page 43 undefined on input
+ line 182.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 43 undefined on input line 204.
+
+
+LaTeX Warning: Citation `Frisch2004' on page 43 undefined on input line 208.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 43 undefined on input line 213.
+
+
+LaTeX Warning: Citation `Kuklewicz' on page 43 undefined on input line 221.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 43 undefined on input line 222.
+
+
+LaTeX Warning: Citation `CrashCourse2014' on page 43 undefined on input line 223
+.
+
+[43]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 44 undefined on input line 235.
+
+
+LaTeX Warning: Citation `Vansummeren2006' on page 44 undefined on input line 237
+.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 44 undefined on input line 238.
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman8-regular.luc)
+
+LaTeX Warning: Citation `Sulzmann2014' on page 44 undefined on input line 242.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 44 undefined on input line 246.
+
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman10-bolditalic.luc) [44]
+
+LaTeX Font Warning: Font shape `U/stmry/b/n' undefined
+(Font) using `U/stmry/m/n' instead on input line 325.
+
+
+LaTeX Warning: Citation `Krauss2011' on page 45 undefined on input line 330.
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman6-regular.luc)
+
+LaTeX Warning: Citation `Brzozowski1964' on page 45 undefined on input line 345.
+
+
+
+Overfull \hbox (1.4002pt too wide) in paragraph at lines 352--373
+ []
+ []
+
+[45]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 46 undefined on input line 408.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 46 undefined on input line 432.
+
+
+LaTeX Warning: Citation `Frisch2004' on page 46 undefined on input line 449.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 46 undefined on input line 450.
+
+
+LaTeX Warning: Citation `AusafDyckhoffUrban2016' on page 46 undefined on input l
+ine 482.
+
+[46]
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 47 undefined on input line 519.
+
+
+
+LaTeX Warning: Citation `Frisch2004' on page 47 undefined on input line 519.
+
+
+Underfull \hbox (badness 10000) in paragraph at lines 579--580
+
+ []
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 47 undefined on input line 590.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 47 undefined on input line 590.
+
+[47]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 48 undefined on input line 610.
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [48]
+[49]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 50 undefined on input line 718.
+
+
+LaTeX Warning: Citation `Vansummeren2006' on page 50 undefined on input line 725
+.
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman5-regular.luc) [50] [51] [52]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 53 undefined on input line 938.
+
+
+LaTeX Warning: Citation `Sulzmann2014' on page 53 undefined on input line 940.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 53 undefined on input line 947.
+
+
+
+LaTeX Warning: Citation `OkuiSuzukiTech' on page 53 undefined on input line 947.
+
+
+[53] [54]
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 55 undefined on input line 1069
+.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 55 undefined on input line 1090
+.
+
+
+LaTeX Warning: Citation `OkuiSuzuki2010' on page 55 undefined on input line 1130
+.
+
+[55]
+Overfull \hbox (47.18065pt too wide) in paragraph at lines 1154--1184
+[] []
+ []
+
+[56] [57]
+
+LaTeX Warning: Citation `Sulzmann2014' on page 58 undefined on input line 1351.
+
+(load luc: /Users/cstan/Library/texlive/2018/texmf-var/luatex-cache/generic/font
+s/otl/lmroman8-bold.luc)(load luc: /Users/cstan/Library/texlive/2018/texmf-var/l
+uatex-cache/generic/fonts/otl/lmroman5-bold.luc)
+
+LaTeX Warning: Citation `Sulzmann2014' on page 58 undefined on input line 1370.
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [58]
+Overfull \hbox (4.61574pt too wide) in paragraph at lines 1434--1435
+\OT1/zplm/m/n/10 $$$\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 dn$\OT1/zplm/m/n/10 $$ $
+\OT1/pplx/m/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/zplm/m/n/1
+0 ($\TU/lmr/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 in-tern$\OT1/pplx/m
+/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 5$\OT1/zplm/m/
+n/10 )$$[$\TU/lmr/m/it/10 of r$[][]$ r$[][]$$\OT1/zplm/m/n/10 ]$$\OMS/zplm/m/n/
+10 g$$n$$n$ $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/z
+plm/m/n/10 ($\TU/lmr/m/it/10 lhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 in-tern$\O
+T1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 6$\OT
+1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$
+ []
+
+
+Overfull \hbox (43.28516pt too wide) in paragraph at lines 1434--1435
+\OT1/pplx/m/n/10 &$ $\OT1/zplm/m/n/10 $$$\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 dn$
+\OT1/zplm/m/n/10 $$ $\OT1/pplx/m/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10
+ thm $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/1
+0 in-tern$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m
+/it/10 6$\OT1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$$n$$n$ $n$\TU/lmr/m/it/10 end$\
+OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 tabular$\OMS/zplm/m/n/10 g$ $n$\TU/lmr/m/it/1
+0 end$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 center$\OMS/zplm/m/n/10 g$ $n$\TU/lmr
+/m/it/10 begin$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 center$\OMS/zplm/m/n/10 g$
+ []
+
+
+Overfull \hbox (31.37523pt too wide) in paragraph at lines 1434--1435
+\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 end$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 tabul
+ar$\OMS/zplm/m/n/10 g$ $n$\TU/lmr/m/it/10 end$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/1
+0 center$\OMS/zplm/m/n/10 g$ \TU/lmr/m/it/10 Some sim-ple facts about erase $
+\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 begin$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 lem
+ma$\OMS/zplm/m/n/10 g$$n$\TU/lmr/m/it/10 mbox$\OMS/zplm/m/n/10 f$$g$$n$$n$
+ []
+
+
+Overfull \hbox (4.57928pt too wide) in paragraph at lines 1434--1435
+\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/zplm/m/n/10 ($
+\TU/lmr/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lable$\OT1/pplx/m/
+n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 4$\OT1/zplm/m/n
+/10 )$$[$\TU/lmr/m/it/10 of bs r$[][]$ r$[][]$$\OT1/zplm/m/n/10 ]$$\OMS/zplm/m/
+n/10 g$$n$$n$ $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1
+/zplm/m/n/10 ($\TU/lmr/m/it/10 lhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lab
+le$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10
+5$\OT1/zplm/m/n/10 )$$[$\TU/lmr/m/it/10 of
+ []
+
+
+Overfull \hbox (7.7924pt too wide) in paragraph at lines 1434--1435
+\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 lhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul
+-lable$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it
+/10 6$\OT1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$ $\OT1/pplx/m/n/10 &$ $\OT1/zplm/m
+/n/10 $$$\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 dn$\OT1/zplm/m/n/10 $$ $\OT1/pplx/m
+/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/zplm/m/n/10 ($\TU/lmr
+/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bnul-lable$\OT1/pplx/m/n/10 .$
+\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 6$\OT1/zplm/m/n/10 )$$
+\OMS/zplm/m/n/10 g$$n$\TU/lmr/m/it/10 medskip$\OMS/zplm/m/n/10 n$$n$
+ []
+
+
+Overfull \hbox (34.28575pt too wide) in paragraph at lines 1434--1435
+\TU/lmr/m/it/10 bder$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10
+($\TU/lmr/m/it/10 3$\OT1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$ $\OT1/pplx/m/n/10 &
+$ $\OT1/zplm/m/n/10 $$$\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 dn$\OT1/zplm/m/n/10 $
+$ $\OT1/pplx/m/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/zplm/m/
+n/10 ($\TU/lmr/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bder$\OT1/pplx/m
+/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 3$\OT1/zplm/m/
+n/10 )$$\OMS/zplm/m/n/10 g$$n$$n$ $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/l
+mr/m/it/10 thm $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 lhs$\OT1/zplm/m/n/10 )$ \TU/
+lmr/m/it/10 bder$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\T
+U/lmr/m/it/10 4$\OT1/zplm/m/n/10 )$$[$\TU/lmr/m/it/10 of
+ []
+
+
+Overfull \hbox (3.47198pt too wide) in paragraph at lines 1434--1435
+\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm $\OT1/zplm/m/n/10 ($
+\TU/lmr/m/it/10 rhs$\OT1/zplm/m/n/10 )$ \TU/lmr/m/it/10 bmkeps$\OT1/pplx/m/n/10
+ .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 4$\OT1/zplm/m/n/10
+)$$\OMS/zplm/m/n/10 g$$n$\TU/lmr/m/it/10 medskip$\OMS/zplm/m/n/10 n$$n$ $n$\TU/
+lmr/m/it/10 end$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 tabular$\OMS/zplm/m/n/10 g$
+$n$\TU/lmr/m/it/10 end$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 center$\OMS/zplm/m/n/
+10 g$ $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm
+ []
+
+
+Overfull \hbox (2.7528pt too wide) in paragraph at lines 1434--1435
+\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 noindent Def-i-ni-tion of the bit-coded lexe
+r $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm blexer[]def$\OMS
+/zplm/m/n/10 g$ $n$\TU/lmr/m/it/10 begin$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 t
+heorem$\OMS/zplm/m/n/10 g$
+ []
+
+[59]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [60]
+Overfull \hbox (2.67558pt too wide) in paragraph at lines 1438--1447
+\TU/lmr/m/it/10 ac-cord-ing to rules like $\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10
+begin$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 equation$\OMS/zplm/m/n/10 g$$n$\TU/lmr
+/m/it/10 label$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 Simpl$\OMS/zplm/m/n/10 g$ $n$
+\TU/lmr/m/it/10 begin$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 array$\OMS/zplm/m/n/10
+ g$$f$\TU/lmr/m/it/10 lcllcllcllcl$\OMS/zplm/m/n/10 g$
+ []
+
+
+Overfull \hbox (35.68385pt too wide) in paragraph at lines 1438--1447
+\TU/lmr/m/it/10 F[]SEQ1$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/
+10 ($\TU/lmr/m/it/10 1$\OT1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$ $\OT1/pplx/m/n/1
+0 &$ $\OT1/zplm/m/n/10 $$$\OMS/zplm/m/n/10 n$\TU/lmr/m/it/10 dn$\OT1/zplm/m/n/1
+0 $$ $\OT1/pplx/m/n/10 &$ []\TU/lmr/m/it/10 Seq $\OT1/zplm/m/n/10 ($\TU/lmr/m/i
+t/10 f$[][]$ $\OT1/zplm/m/n/10 ($$)$$)$ $($\TU/lmr/m/it/10 f$[][]$ v$\OT1/zplm/
+m/n/10 )$[]$\OMS/zplm/m/n/10 n$$n$ $\OT1/pplx/m/n/10 @$$\OMS/zplm/m/n/10 f$\TU/
+lmr/m/it/10 thm $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 lhs$\OT1/zplm/m/n/10 )$ \TU
+/lmr/m/it/10 F[]SEQ2$\OT1/pplx/m/n/10 .$\TU/lmr/m/it/10 simps$\OT1/zplm/m/n/10
+($\TU/lmr/m/it/10 1$\OT1/zplm/m/n/10 )$$\OMS/zplm/m/n/10 g$
+ []
+
+
+Overfull \hbox (18.66588pt too wide) in paragraph at lines 1438--1447
+\OT1/pplx/m/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm L[]fst[]simp$\OT
+1/zplm/m/n/10 [$\TU/lmr/m/it/10 symmetric$\OT1/zplm/m/n/10 ]$$\OMS/zplm/m/n/10
+g$$n$$n$ $\OT1/zplm/m/n/10 ($\TU/lmr/m/it/10 2$\OT1/zplm/m/n/10 )$ $\OT1/pplx/m
+/n/10 &$ $@$$\OMS/zplm/m/n/10 f$\TU/lmr/m/it/10 thm$\OT1/zplm/m/n/10 [$\TU/lmr/
+m/it/10 mode$\OT1/zplm/m/n/10 =$\TU/lmr/m/it/10 IfThen$\OT1/zplm/m/n/10 ]$ \TU/
+lmr/m/it/10 Posix[]simp$\OMS/zplm/m/n/10 g$
+ []
+
+
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [61]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [62]
+[63] [64]
+No file root.bbl.
+)) [65]
+Package atveryend Info: Empty hook `BeforeClearDocument' on input line 96.
+Package atveryend Info: Empty hook `AfterLastShipout' on input line 96.
+ (./root.aux)
+Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 96.
+Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 96.
+
+
+Package rerunfilecheck Warning: File `root.out' has changed.
+(rerunfilecheck) Rerun to get outlines right
+(rerunfilecheck) or use package `bookmark'.
+
+Package rerunfilecheck Info: Checksums for `root.out':
+(rerunfilecheck) Before: 40AB4FCF7DFB133886AD9117C6B3D022;396
+(rerunfilecheck) After: F68486A1B88421815EBCC3CB75200893;512.
+
+LaTeX Font Warning: Size substitutions with differences
+(Font) up to 2.26395pt have occurred.
+
+
+LaTeX Font Warning: Some font shapes were not available, defaults substituted.
+
+
+LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
+
+Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 96.
+)
+
+Here is how much of LuaTeX's memory you used:
+ 29104 strings out of 494413
+ 156265,794899 words of node,token memory allocated
+ 1590 words of node memory still in use:
+ 9 hlist, 2 vlist, 2 rule, 11 disc, 21 glue, 7 kern, 98 glyph, 33 attribute, 5
+7 glue_spec, 33 attribute_list, 1 write nodes
+ avail lists: 2:6992,3:290,4:52,5:2358,6:47,7:12582,8:52,9:593,10:23,11:398
+ 31952 multiletter control sequences out of 65536+600000
+ 282 fonts using 23215399 bytes
+ 55i,23n,68p,45885b,993s stack positions out of 5000i,500n,10000p,200000b,100000s
+
+warning (pdf backend): unreferenced destination with name 'equation.1.6.2'
+
+warning (pdf backend): unreferenced destination with name 'theorem.1.4.3'
+
+warning (pdf backend): unreferenced destination with name 'theorem.1.3.2'
+
+warning (pdf backend): unreferenced destination with name 'theorem.1.3.1'
+
+warning (pdf backend): unreferenced destination with name 'equation.1.2.1'
+</usr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman7-regular.ot
+f></usr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman8-regular.
+otf></usr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman7-italic
+.otf></usr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman10-ital
+ic.otf></usr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman10-bo
+ld.otf>{/usr/local/texlive/2018/texmf-dist/fonts/enc/dvips/base/8r.enc}</usr/loc
+al/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman9-italic.otf></usr/lo
+cal/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman9-bold.otf></usr/loc
+al/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmmono9-regular.otf></usr/lo
+cal/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman9-regular.otf></usr/
+local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman10-regular.otf></u
+sr/local/texlive/2018/texmf-dist/fonts/opentype/public/lm/lmroman12-bold.otf></u
+sr/local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></us
+r/local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/
+local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/lo
+cal/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local
+/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/t
+exlive/2018/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/loca
+l/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/l
+ocal/texlive/2018/texmf-dist/fonts/type1/public/stmaryrd/stmary10.pfb></usr/loca
+l/texlive/2018/texmf-dist/fonts/type1/urw/palatino/uplr8a.pfb></usr/local/texliv
+e/2018/texmf-dist/fonts/type1/urw/palatino/uplri8a.pfb>
+Output written on root.pdf (65 pages, 375818 bytes).
+
+PDF statistics: 526 PDF objects out of 1000 (max. 8388607)
+ 411 compressed objects within 5 object streams
+ 112 named destinations out of 1000 (max. 131072)
+ 72 words of extra memory for PDF output out of 10000 (max. 100000000)
+