This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=latex 2012.5.21) 13 MAR 2015 11:08 entering extended mode %&-line parsing enabled. **fpt-from-s11.tex (./fpt-from-s11.tex LaTeX2e <2009/09/24> Babel and hyphenation patterns for english, usenglishmax, dumylang, noh yphenation, danish, french, basque, ngerman, german, german-x-2009-06-19, ngerm an-x-2009-06-19, ibycus, monogreek, greek, ancientgreek, ukenglish, loaded. (/usr/share/texmf-texlive/tex/latex/paper/paper.cls Document Class: paper 2008/05/30 1.0l LaTeX document class (wm). \hours=\count79 \minutes=\count80 (/usr/share/texmf-texlive/tex/latex/base/size10.clo File: size10.clo 2007/10/19 v1.4h Standard LaTeX file (size option) ) \beforetitlespace=\skip41 \c@part=\count81 \c@section=\count82 \c@subsection=\count83 \c@subsubsection=\count84 \c@paragraph=\count85 \c@subparagraph=\count86 \exampleindent=\skip42 \c@figure=\count87 \c@table=\count88 \abovecaptionskip=\skip43 \belowcaptionskip=\skip44 \bibindent=\dimen102 ) (/usr/share/texmf-texlive/tex/latex/base/latexsym.sty Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols) \symlasy=\mathgroup4 LaTeX Font Info: Overwriting symbol font `lasy' in version `bold' (Font) U/lasy/m/n --> U/lasy/b/n on input line 47. ) (/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty Package: amssymb 2009/06/22 v3.00 (/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty Package: amsfonts 2009/06/22 v3.00 Basic AMSFonts support \@emptytoks=\toks14 \symAMSa=\mathgroup5 \symAMSb=\mathgroup6 LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' (Font) U/euf/m/n --> U/euf/b/n on input line 96. )) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty Package: amsmath 2000/07/18 v2.13 AMS math features \@mathmargin=\skip45 For additional information on amsmath, use the `?' option. (/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty Package: amstext 2000/06/29 v2.01 (/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty File: amsgen.sty 1999/11/30 v2.0 \@emptytoks=\toks15 \ex@=\dimen103 )) (/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty Package: amsbsy 1999/11/29 v1.2d \pmbraise@=\dimen104 ) (/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty Package: amsopn 1999/12/14 v2.01 operator names ) \inf@bad=\count89 LaTeX Info: Redefining \frac on input line 211. \uproot@=\count90 \leftroot@=\count91 LaTeX Info: Redefining \overline on input line 307. \classnum@=\count92 \DOTSCASE@=\count93 LaTeX Info: Redefining \ldots on input line 379. LaTeX Info: Redefining \dots on input line 382. LaTeX Info: Redefining \cdots on input line 467. \Mathstrutbox@=\box26 \strutbox@=\box27 \big@size=\dimen105 LaTeX Font Info: Redeclaring font encoding OML on input line 567. LaTeX Font Info: Redeclaring font encoding OMS on input line 568. \macc@depth=\count94 \c@MaxMatrixCols=\count95 \dotsspace@=\muskip10 \c@parentequation=\count96 \dspbrk@lvl=\count97 \tag@help=\toks16 \row@=\count98 \column@=\count99 \maxfields@=\count100 \andhelp@=\toks17 \eqnshift@=\dimen106 \alignsep@=\dimen107 \tagshift@=\dimen108 \tagwidth@=\dimen109 \totwidth@=\dimen110 \lineht@=\dimen111 \@envbody=\toks18 \multlinegap=\skip46 \multlinetaggap=\skip47 \mathdisplay@stack=\toks19 LaTeX Info: Redefining \[ on input line 2666. LaTeX Info: Redefining \] on input line 2667. ) (/usr/share/texmf-texlive/tex/latex/ltxmisc/url.sty \Urlmuskip=\muskip11 Package: url 2006/04/12 ver 3.3 Verb mode for urls, etc. ) (/usr/share/texmf-texlive/tex/latex/bussproofs/bussproofs.sty Proof Tree (bussproofs) style macros. Version 1.0. \theLevel=\count101 \myMaxLevel=\count102 \myBoxA=\box28 \myBoxB=\box29 \myBoxC=\box30 \myBoxD=\box31 \myBoxLL=\box32 \myBoxRL=\box33 \thisAboveSkip=\dimen112 \thisBelowSkip=\dimen113 \newScoreStart=\dimen114 \newScoreEnd=\dimen115 \newCenter=\dimen116 \displace=\dimen117 \leftLowerAmt=\dimen118 \rightLowerAmt=\dimen119 \scoreHeight=\dimen120 \scoreDepth=\dimen121 \htLbox=\dimen122 \htRbox=\dimen123 \htAbox=\dimen124 \htCbox=\dimen125 ) (/usr/share/texmf-texlive/tex/latex/listings/listings.sty (/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty Package: keyval 1999/03/16 v1.13 key=value parser (DPC) \KV@toks@=\toks20 ) \lst@mode=\count103 \lst@gtempboxa=\box34 \lst@token=\toks21 \lst@length=\count104 \lst@currlwidth=\dimen126 \lst@column=\count105 \lst@pos=\count106 \lst@lostspace=\dimen127 \lst@width=\dimen128 \lst@newlines=\count107 \lst@lineno=\count108 \lst@maxwidth=\dimen129 (/usr/share/texmf-texlive/tex/latex/listings/lstmisc.sty File: lstmisc.sty 2007/02/22 1.4 (Carsten Heinz) \c@lstnumber=\count109 \lst@skipnumbers=\count110 \lst@framebox=\box35 ) (/usr/share/texmf-texlive/tex/latex/listings/listings.cfg File: listings.cfg 2007/02/22 1.4 listings configuration )) Package: listings 2007/02/22 1.4 (Carsten Heinz) \c@definition=\count111 \c@theorem=\count112 \c@lemma=\count113 \c@corollary=\count114 (./fpt-from-s11.aux) \openout1 = `fpt-from-s11.aux'. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 188. LaTeX Font Info: ... okay on input line 188. LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 188. LaTeX Font Info: ... okay on input line 188. LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 188. LaTeX Font Info: ... okay on input line 188. LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 188. LaTeX Font Info: ... okay on input line 188. LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 188. LaTeX Font Info: ... okay on input line 188. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 188. LaTeX Font Info: ... okay on input line 188. \c@lstlisting=\count115 LaTeX Font Info: Try loading font information for U+lasy on input line 207. (/usr/share/texmf-texlive/tex/latex/base/ulasy.fd File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions ) LaTeX Font Info: Try loading font information for U+msa on input line 207. (/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd File: umsa.fd 2009/06/22 v3.00 AMS symbols A ) LaTeX Font Info: Try loading font information for U+msb on input line 207. (/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd File: umsb.fd 2009/06/22 v3.00 AMS symbols B ) Overfull \hbox (8.02036pt too wide) in paragraph at lines 207--207 [][] [] [1 ] (./fpt-from-s11.toc) \tf@toc=\write3 \openout3 = `fpt-from-s11.toc'. [2] Overfull \hbox (38.24666pt too wide) in paragraph at lines 268--268 [] \OT1/cmtt/m/n/10 ((?Xl + (?Xr - {#?A#}) |- ?Yl - {#?A#} + ?Yr) : der rec ?rls {})"[] [] [3] Overfull \hbox (9.11272pt too wide) in paragraph at lines 337--340 []\OT1/cmr/m/n/10 if \OT1/cmtt/m/n/10 pscl \OT1/cmr/m/n/10 and \OT1/cmtt/m/n/10 pscr \OT1/cmr/m/n/10 are in \OT1/cmtt/m/n/10 rls\OT1/cmr/m/n/10 , then they sa t-isfy the step con-di-tion \OT1/cmtt/m/n/10 gen[]step2sr [] Overfull \hbox (27.74675pt too wide) in paragraph at lines 353--353 [] \OT1/cmtt/m/n/10 gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls (?pscl , ?pscr)) =[] [] Overfull \hbox (1.49698pt too wide) in paragraph at lines 353--353 [] \OT1/cmtt/m/n/10 (ALL dta dtb. botRule dta = ?pscl --> botRule dtb = ?ps cr -->[] [] LaTeX Warning: Citation `ohnishi1957' on page 4 undefined on input line 471. LaTeX Warning: Citation `Troelstra' on page 4 undefined on input line 471. LaTeX Warning: Citation `dawson14' on page 4 undefined on input line 472. [4] Underfull \hbox (badness 2351) in paragraph at lines 480--480 []\OT1/cmr/m/n/10 Jesse, is this [] \myBox1=\box36 \myScoreStart1=\dimen130 \myCenter1=\dimen131 \myScoreEnd1=\dimen132 LaTeX Warning: Citation `Goubault96' on page 5 undefined on input line 496. LaTeX Warning: Citation `bierman96' on page 5 undefined on input line 501. LaTeX Warning: Citation `Negri05' on page 5 undefined on input line 510. \myBox2=\box37 \myScoreStart2=\dimen133 \myCenter2=\dimen134 \myScoreEnd2=\dimen135 Overfull \hbox (32.9967pt too wide) in paragraph at lines 615--615 [] \OT1/cmtt/m/n/10 boxI : "(prem, conc) : lkbox ==> (prem, extend flr conc ) : gs4_rls"[] [] [5] [6] LaTeX Font Info: Try loading font information for OMS+cmr on input line 654. (/usr/share/texmf-texlive/tex/latex/base/omscmr.fd File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions ) LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available (Font) Font shape `OMS/cmsy/m/n' tried instead on input line 654. LaTeX Warning: Reference `s-ctr' on page 7 undefined on input line 654. LaTeX Warning: Reference `l-der-ind' on page 7 undefined on input line 681. [7] Overfull \hbox (4.91902pt too wide) in paragraph at lines 746--748 []\OT1/cmr/m/n/10 Use of the in-duc-tion hy-poth-e-sis stated above can then be en-coded in \OT1/cmtt/m/n/10 inv[]step\OT1/cmr/m/n/10 . [] [8] Overfull \hbox (17.24684pt too wide) in paragraph at lines 817--817 [] \OT1/cmtt/m/n/10 <= derrec ?drls (set ?ps Un UNION (set ?ps) (invs_of ?irls)))"[] [] Overfull \hbox (0.2198pt too wide) in paragraph at lines 851--858 []\OT1/cmtt/m/n/10 (ps, concl) \OT1/cmr/m/n/10 from []\OT1/cmtt/m/n/10 rls \OT1 /cmr/m/n/10 obeys []\OT1/cmtt/m/n/10 inv_step (derrec rls {}) irls (ps, concl)\ OT1/cmr/m/n/10 : [] [9] Overfull \hbox (11.99689pt too wide) in paragraph at lines 863--863 [] \OT1/cmtt/m/n/10 "[| Ball ?rls (inv_step (derrec ?rls {}) ?irls) ; ?psc : ?irls |][] [] LaTeX Font Info: Try loading font information for OMS+cmtt on input line 891 . LaTeX Font Info: No file OMScmtt.fd. on input line 891. LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined (Font) using `OMS/cmsy/m/n' instead (Font) for symbol `textbraceleft' on input line 891. Overfull \hbox (5.4972pt too wide) in paragraph at lines 909--909 []\OT1/cmtt/m/n/10 "?psc : extrs lkrefl ==> inv_stepm gs4_rls (extrs lksne) ?p sc"[] [] Overfull \hbox (0.24724pt too wide) in paragraph at lines 924--924 []\OT1/cmtt/m/n/10 "?psc : extrs lksne ==> inv_stepm gs4_rls (extrs lksne) ?ps c"[] [] [10] Overfull \hbox (31.74696pt too wide) in paragraph at lines 941--941 [] \OT1/cmtt/m/n/10 "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |][] [] Underfull \hbox (badness 10000) in paragraph at lines 962--962 []\OT1/cmr/m/n/10 Which of [] Underfull \hbox (badness 10000) in paragraph at lines 962--962 \OT1/cmr/m/n/10 the gen-step [] Underfull \hbox (badness 10000) in paragraph at lines 962--962 \OT1/cmr/m/n/10 lem-mas does [] Underfull \hbox (badness 10000) in paragraph at lines 962--962 \OT1/cmr/m/n/10 it ac-tu-ally [] Overfull \hbox (9.33931pt too wide) in paragraph at lines 962--962 \OT1/cmtt/m/n/10 gen[]inv[]by[]step [] [11] Overfull \hbox (2.31183pt too wide) in paragraph at lines 1045--1046 []\OT1/cmr/m/n/10 Contraction is ad-mis-si-ble for the cal-cu-lus \OT1/cmtt/m/n /10 gs4[]rls\OT1/cmr/m/n/10 . [] LaTeX Warning: Citation `Troelstra' on page 12 undefined on input line 1053. LaTeX Warning: Citation `Negri01' on page 12 undefined on input line 1053. LaTeX Warning: Reference `genstep:lem' on page 12 undefined on input line 1058. Underfull \hbox (badness 10000) in paragraph at lines 1082--1082 []\OT1/cmr/m/n/10 Was just $\OML/cmm/m/it/10 '$ [] Underfull \hbox (badness 10000) in paragraph at lines 1082--1082 \OT1/cmr/m/n/10 in succe-dent [] Underfull \hbox (badness 4156) in paragraph at lines 1082--1082 \OT1/cmr/m/n/10 of con-clusion. [] Underfull \hbox (badness 4279) in paragraph at lines 1082--1082 \OT1/cmr/m/n/10 (for Jesse to [] Underfull \hbox (badness 10000) in paragraph at lines 1096--1096 \OT1/cmr/m/n/10 succe-dent of [] [12] Underfull \hbox (badness 10000) in paragraph at lines 1108--1108 \OT1/cmr/m/n/10 succe-dent of [] LaTeX Warning: Reference `l-gs2-hs2-sumh' on page 13 undefined on input line 11 42. Overfull \hbox (43.49661pt too wide) in paragraph at lines 1152--1152 [] \OT1/cmtt/m/n/10 "gen_step2sr (prop2 car ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)[] [] Overfull \hbox (6.74693pt too wide) in paragraph at lines 1152--1152 [] \OT1/cmtt/m/n/10 ==> sumh_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"[] [] LaTeX Warning: Reference `l-sumh-step2-tr-lem' on page 13 undefined on input li ne 1162. Underfull \hbox (badness 5475) in paragraph at lines 1166--1166 []\OT1/cmr/m/n/10 which means, [] Underfull \hbox (badness 6316) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 ing, that so [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 far as rank [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 is con-cerned, [] Underfull \hbox (badness 6380) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 the in-duc-tion [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 as-sumes only [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 cut ad-mis- [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 si-bil-ity for [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 cut-formula [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 which are [] Underfull \hbox (badness 10000) in paragraph at lines 1166--1166 \OT1/cmr/m/n/10 im-me-di-ate [] [13] \myBox3=\box38 \myScoreStart3=\dimen136 \myCenter3=\dimen137 \myScoreEnd3=\dimen138 LaTeX Warning: Citation `Troelstra' on page 14 undefined on input line 1264. LaTeX Warning: Citation `Goubault96' on page 14 undefined on input line 1267. Overfull \hbox (8.8923pt too wide) in paragraph at lines 1296--1297 [] [] [14] LaTeX Warning: Reference `l-sumh-step2-tr-lem' on page 15 undefined on input li ne 1300. LaTeX Warning: Reference `thm-gen-step2sr-lem' on page 15 undefined on input li ne 1307. LaTeX Warning: Citation `Shimura91' on page 15 undefined on input line 1318. LaTeX Warning: Citation `gore94' on page 15 undefined on input line 1322. LaTeX Warning: Citation `indrzejczak12' on page 15 undefined on input line 1322 . LaTeX Warning: Citation `Negri05' on page 15 undefined on input line 1329. LaTeX Warning: Citation `castellini06' on page 15 undefined on input line 1330. LaTeX Warning: Citation `gore94' on page 15 undefined on input line 1340. Overfull \hbox (0.6117pt too wide) in paragraph at lines 1417--1426 []\OT1/cmr/m/n/10 From the per-spec-tive of back-ward proof search, the S4.3$\U /lasy/m/n/10 2$ \OT1/cmr/m/n/10 rule can be thought [] [15] [16] LaTeX Warning: Reference `genstep:lem' on page 17 undefined on input line 1514. [17] Overfull \hbox (1.26572pt too wide) in paragraph at lines 1539--1541 []\OT1/cmr/m/n/10 If \OT1/cmtt/m/n/10 wk[]adm[]single[]antec \OT1/cmr/m/n/10 an d \OT1/cmtt/m/n/10 wk[]adm[]single[]succ [] Overfull \hbox (2.81177pt too wide) in paragraph at lines 1547--1548 []\OT1/cmr/m/n/10 Weakening is ad-mis-si-ble for the cal-cu-lus \OT1/cmtt/m/n/1 0 gs43[]rls\OT1/cmr/m/n/10 . [] Underfull \hbox (badness 10000) in paragraph at lines 1559--1559 []\OT1/cmr/m/n/10 Was $[]$ in [] Underfull \hbox (badness 10000) in paragraph at lines 1559--1559 \OT1/cmr/m/n/10 succe-dent of [] [18] Overfull \hbox (5.48674pt too wide) in paragraph at lines 1657--1658 \OT1/cmr/m/n/10 then prov-ing in-vert-ibil-ity for G3cp re-quires show-ing the deriv-abil-ity of all premises [] [19] LaTeX Warning: Reference `l-der-ind' on page 20 undefined on input line 1724. Overfull \hbox (3.48659pt too wide) in paragraph at lines 1744--1748 []\OT1/cmr/m/n/10 No rules in G3cp op-er-ate on a boxed [] [20] LaTeX Warning: Reference `genstep:lem' on page 21 undefined on input line 1795. [21] LaTeX Warning: Reference `l-sumh-step2-tr-lem' on page 22 undefined on input li ne 1913. LaTeX Warning: Reference `thm-gen-step2sr-lem' on page 22 undefined on input li ne 1915. Overfull \hbox (27.78111pt too wide) in paragraph at lines 1948--1950 [] [] [22] Overfull \hbox (30.14484pt too wide) in paragraph at lines 1972--1973 [] [] LaTeX Warning: Reference `l-sumh-step2-tr-lem' on page 23 undefined on input li ne 1983. [23] Overfull \hbox (36.22787pt too wide) in paragraph at lines 2056--2057 [] [] LaTeX Warning: Citation `mints-jaegerfest' on page 24 undefined on input line 2 071. [24] Underfull \hbox (badness 10000) in paragraph at lines 2658--2658 []\OT1/cmr/m/n/10 JED please [] Underfull \hbox (badness 10000) in paragraph at lines 2658--2658 \OT1/cmr/m/n/10 check ver-ba- [] [25] Overfull \hbox (1.49698pt too wide) in paragraph at lines 2764--2764 [] \OT1/cmtt/m/n/10 "[| inv_stepm ?drls ?irlsa ?psc; inv_stepm ?drls ?irlsb ? psc |][] [] [26] Overfull \hbox (17.24684pt too wide) in paragraph at lines 2822--2822 [] \OT1/cmtt/m/n/10 "?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lks ne) ?psc"[] [] Overfull \hbox (27.74675pt too wide) in paragraph at lines 2822--2822 [] \OT1/cmtt/m/n/10 "[| seq_meet ?c ?ic = 0; extrs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>[] [] Overfull \hbox (22.4968pt too wide) in paragraph at lines 2822--2822 [] \OT1/cmtt/m/n/10 "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ? rls |] ==>[] [] Overfull \hbox (6.74693pt too wide) in paragraph at lines 2822--2822 [] \OT1/cmtt/m/n/10 "[| extrs {?srl} = ?rls; ?rl : ?rls; ?srl : scrls; ?irl : scrls;[] [] [27] Overfull \hbox (59.24648pt too wide) in paragraph at lines 2914--2914 [] \OT1/cmtt/m/n/10 ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Bo x B#}) : s4g prs"[] [] [28] Overfull \hbox (59.24648pt too wide) in paragraph at lines 3026--3026 []\OT1/cmtt/m/n/10 lcg_gen_step: "[| wk_adm ?erls; extrs {(?ps, ?U |- ?V)} <= ? erls; ~ ?A :# ?V;[] [] Overfull \hbox (11.99689pt too wide) in paragraph at lines 3026--3026 [] \OT1/cmtt/m/n/10 "[| wk_adm ?rls; extcs {(?ps, ?c)} <= ?rls; ~ ?A :# succ ? c |] ==>[] [] Overfull \hbox (69.74638pt too wide) in paragraph at lines 3026--3026 [] \OT1/cmtt/m/n/10 gen_step2sr (prop2 car ?rls) ?A ?sub ?rls ((?ps, extend ?f lr ?c), ?psr, ?cr)"[] [] [29] Overfull \hbox (6.74693pt too wide) in paragraph at lines 3080--3080 []\OT1/cmtt/m/n/10 gs2sr_alle: "[| wk_adm ?prls; c8_ercas_prop ?psubfml ?prls ? A ?rls;[] [] Overfull \hbox (48.74657pt too wide) in paragraph at lines 3080--3080 [] \OT1/cmtt/m/n/10 gen_step2sr (prop2 car ?prls) ?A ?psubfml ?prls ((?psa, ?c a), ?psb, ?cb)"[] [] Overfull \hbox (22.4968pt too wide) in paragraph at lines 3120--3120 [] \OT1/cmtt/m/n/10 "[| ALL A'. ctr_adm ?drls A' ; wk_adm ?drls; extrs lksne < = ?drls |][] [] Overfull \hbox (17.24684pt too wide) in paragraph at lines 3129--3129 []\OT1/cmtt/m/n/10 gtdns_lksne_c8: "c8_ercas_prop ipsubfml (lkssx (extcs GTD)) ?A lksne"[] [] Overfull \hbox (43.49661pt too wide) in paragraph at lines 3142--3142 [] \OT1/cmtt/m/n/10 "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (lkssx (e xtcs GTD)) ?A"[] [] LaTeX Warning: Citation `mints-jaegerfest' on page 30 undefined on input line 3 147. [30] LaTeX Warning: Citation `mints-jaegerfest' on page 31 undefined on input line 3 158. [31] Overfull \hbox (48.74657pt too wide) in paragraph at lines 3257--3257 [] \OT1/cmtt/m/n/10 extcsI : "(ps, c) : circ Un s4cbox ==> (ps, extend (U |- V) c) : s4cns"[] [] Overfull \hbox (22.4968pt too wide) in paragraph at lines 3257--3257 [] \OT1/cmtt/m/n/10 boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cbox"[] [] [32] LaTeX Warning: Reference `d-gen-step' on page 33 undefined on input line 3285. LaTeX Warning: Reference `genstep:lem' on page 33 undefined on input line 3285. Overfull \hbox (1.49698pt too wide) in paragraph at lines 3352--3352 [] \OT1/cmtt/m/n/10 "[| ?epsc : extrs ?lrls; ?lrls <= iscrls; extrs ?lrls <= ?drls;[] [] [33] Overfull \hbox (48.74657pt too wide) in paragraph at lines 3352--3352 [] \OT1/cmtt/m/n/10 (ALL fp. ms_mem fp p --> (EX fc. ms_mem fc ?c & (fp, fc) : ?sub)))"[] [] Overfull \hbox (22.4968pt too wide) in paragraph at lines 3370--3370 [] \OT1/cmtt/m/n/10 "[| ?psc = (?ps, ?c); ?psc : extcs s4cbox; extcs s4cbox < = ?drls |][] [] Overfull \hbox (1.49698pt too wide) in paragraph at lines 3370--3370 [] \OT1/cmtt/m/n/10 "[| ?psc = (?ps, ?c); ?psc : extcs circ; extcs circ <= ?d rls |][] [] [34] Overfull \hbox (43.49661pt too wide) in paragraph at lines 3429--3429 [] \OT1/cmtt/m/n/10 forget ((k = 0) = (botRule ?dt ~: extcs circ) & (k = 0) = (dtn = ?dt))"[] [] [35] Overfull \hbox (43.49661pt too wide) in paragraph at lines 3502--3502 [] \OT1/cmtt/m/n/10 "[| (?ps, ?cl |- ?cr) : s4cns; botRule ?dtn : extcs {(?ps, ?cl |- ?cr)};[] [] Overfull \hbox (43.49661pt too wide) in paragraph at lines 3502--3502 [] \OT1/cmtt/m/n/10 count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4c ns ?dtn |] ==>[] [] [36] Overfull \hbox (11.99689pt too wide) in paragraph at lines 3626--3626 [] \OT1/cmtt/m/n/10 count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4c ns ?dtn;[] [] Overfull \hbox (1.49698pt too wide) in paragraph at lines 3626--3626 [] \OT1/cmtt/m/n/10 (Der (seqmap (funpow Circ ?k) (conclDT ?dtn) + ?flr) ?list,[] [] Overfull \hbox (1.59523pt too wide) in paragraph at lines 3636--3651 [] [] Overfull \hbox (4.95148pt too wide) in paragraph at lines 3659--3677 [] [] [37] [38] LaTeX Warning: Citation `mints-jaegerfest' on page 39 undefined on input line 3 809. LaTeX Warning: Citation `pfenning-structural-cut-elimination' on page 39 undefi ned on input line 3826. [39] LaTeX Warning: Reference `s-ipedt' on page 40 undefined on input line 3844. LaTeX Warning: Reference `s-ipedt' on page 40 undefined on input line 3846. No file fpt-from-s11.bbl. [40] (./fpt-from-s11.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. LaTeX Warning: There were undefined references. ) Here is how much of TeX's memory you used: 2995 strings out of 494887 37567 string characters out of 1177128 100133 words of memory out of 3000000 6181 multiletter control sequences out of 15000+50000 16798 words of font info for 69 fonts, out of 3000000 for 9000 88 hyphenation exceptions out of 8191 27i,9n,32p,749b,319s stack positions out of 5000i,500n,10000p,200000b,50000s Output written on fpt-from-s11.dvi (40 pages, 151656 bytes).