This is TeX, Version 3.14159 (Web2C 7.4.5) (format=latex 2007.11.17)  6 FEB 2008 17:14
**marcelmanual
(./marcelmanual.tex
LaTeX2e <2001/06/01>
Babel <v3.7h> and hyphenation patterns for american, french, german, ngerman, n
ohyphenation, loaded.
(/usr/share/texmf/tex/latex/base/article.cls
Document Class: article 2001/04/21 v1.4e Standard LaTeX document class
(/usr/share/texmf/tex/latex/base/size12.clo
File: size12.clo 2001/04/21 v1.4e Standard LaTeX file (size option)
)
\c@part=\count79
\c@section=\count80
\c@subsection=\count81
\c@subsubsection=\count82
\c@paragraph=\count83
\c@subparagraph=\count84
\c@figure=\count85
\c@table=\count86
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen102
) (./bussproofs.sty
Proof Tree (bussproofs) style macros. Version 1.0.
\theLevel=\count87
\myMaxLevel=\count88
\myBoxA=\box26
\myBoxB=\box27
\myBoxC=\box28
\myBoxD=\box29
\myBoxLL=\box30
\myBoxRL=\box31
\thisAboveSkip=\dimen103
\thisBelowSkip=\dimen104
\newScoreStart=\dimen105
\newScoreEnd=\dimen106
\newCenter=\dimen107
\displace=\dimen108
\leftLowerAmt=\dimen109
\rightLowerAmt=\dimen110
\scoreHeight=\dimen111
\scoreDepth=\dimen112
\htLbox=\dimen113
\htRbox=\dimen114
\htAbox=\dimen115
\htCbox=\dimen116
) (/usr/share/texmf/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2002/01/22 v2.2d

(/usr/share/texmf/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2001/10/25 v2.2f
\@emptytoks=\toks14
\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 132.
))
(/usr/share/texmf/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup6
LaTeX Font Info:    Overwriting symbol font `lasy' in version `bold'
(Font)                  U/lasy/m/n --> U/lasy/b/n on input line 42.
) (./marcelmanual.aux)
\openout1 = `marcelmanual.aux'.

LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 10.
LaTeX Font Info:    ... okay on input line 10.
LaTeX Font Info:    Try loading font information for U+msa on input line 12.

(/usr/share/texmf/tex/latex/amsfonts/umsa.fd
File: umsa.fd 2002/01/19 v2.2g AMS font definitions
)
LaTeX Font Info:    Try loading font information for U+msb on input line 12.

(/usr/share/texmf/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2002/01/19 v2.2g AMS font definitions
)
LaTeX Font Info:    Try loading font information for U+lasy on input line 12.

(/usr/share/texmf/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
) (./marcelmanual.toc [1

])
\tf@toc=\write3
\openout3 = `marcelmanual.toc'.

 [2]

LaTeX Warning: Citation `nocuts' on page 3 undefined on input line 24.


LaTeX Warning: Citation `nfu' on page 3 undefined on input line 29.

[3]
Overfull \hbox (20.6537pt too wide) in paragraph at lines 71--86
\OT1/cmr/m/n/12 with \OT1/cmtt/m/n/12 *\OT1/cmr/m/n/12 . Pred-i-cates and func-
tions were al-ways pre-fix (as \OT1/cmtt/m/n/12 #predicate(arg1,arg2)\OT1/cmr/m
/n/12 ,
 []

LaTeX Font Info:    Try loading font information for OMS+cmtt on input line 98.

LaTeX Font Info:    No file OMScmtt.fd. on input line 98.

LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 98.

[4] [5] [6]
Overfull \hbox (26.091pt too wide) in paragraph at lines 225--229
[]\OT1/cmr/m/n/12 Function binders take propo-si-tion in-put and give ob-ject o
ut-put \OT1/cmtt/m/n/12 [B term.term]
 []

[7] [8] [9] [10] [11]
Overfull \hbox (14.95355pt too wide) in paragraph at lines 471--485
\OT1/cmr/m/n/12 fixed off-set may be added to all of the types. If a sen-tence 
\OT1/cmtt/m/n/12 predicate(t1,...tn)
 []


Overfull \hbox (20.24971pt too wide) in paragraph at lines 497--500
[]\OT1/cmr/m/n/12 The strat-i-fi-ca-tion al-go-rithm is in-voked when a sen-ten
ce \OT1/cmtt/m/n/12 t $\OMS/cmtt/m/n/12 2$ f\OT1/cmtt/m/n/12 x | ...x...\OMS/cm
tt/m/n/12 g\OT1/cmr/m/n/12 is
 []

[12] [13] [14] [15] [16]
\myBox1=\box32
\myScoreStart1=\dimen117
\myCenter1=\dimen118
\myScoreEnd1=\dimen119
\myBox2=\box33
\myScoreStart2=\dimen120
\myCenter2=\dimen121
\myScoreEnd2=\dimen122
 [17]
Overfull \hbox (6.34676pt too wide) in paragraph at lines 769--778
[]\OT1/cmr/m/n/12 Our ap-proach to bound and free vari-ables in the old ver-sio
n \OT1/cmtt/m/n/12 marcelsequent
 []

[18] [19] [20] [21] [22]
Overfull \hbox (10.99577pt too wide) in paragraph at lines 1054--1054
[]\OT1/cmr/bx/n/17.28 The The-o-rem List and Read-ing Saved Proofs 
 []


Overfull \hbox (8.72305pt too wide) in paragraph at lines 1074--1085
[]\OT1/cmr/m/n/12 The \OT1/cmtt/m/n/12 Constructive \OT1/cmr/m/n/12 com-mand im
-ple-ments con-struc-tive (in-tu-ition-is-tic) logic.
 []

[23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36]
Overfull \hbox (9.44934pt too wide) in paragraph at lines 1666--1676
[]\OT1/cmr/m/n/12 an in-te-ger ar-gu-ment fol-lowed by three
 []

[37] [38]
Overfull \hbox (3.1637pt too wide) in paragraph at lines 1715--1717
[]\OT1/cmr/m/n/12 One string ar-gu-ment \OT1/cmtt/m/n/12 name\OT1/cmr/m/n/12 . 
Load the the-ory saved in \OT1/cmtt/m/n/12 name.thy1
 []


Overfull \hbox (54.7525pt too wide) in paragraph at lines 1726--1728
[]\OT1/cmr/m/n/12 No ar-gu-ments. Turns off the mode in-tro-duced by \OT1/cmtt/
m/n/12 OneConclusion\OT1/cmr/m/n/12 . 
 []

[39] [40]
Overfull \hbox (3.2503pt too wide) in paragraph at lines 1829--1835
\OT1/cmr/m/n/12 propo-si-tions of the form \OT1/cmtt/m/n/12 Pn(t1,...,tn) \OT1/
cmr/m/n/12 with propo-si-tions \OT1/cmtt/m/n/12 [t1,...,tn]
 []

[41] [42]
Overfull \hbox (17.95296pt too wide) in paragraph at lines 1912--1914
[]\OT1/cmr/m/n/12 Two in-te-ger ar-gu-ments. \OT1/cmtt/m/n/12 Triv m n \OT1/cmr
/m/n/12 has the ef-fect of \OT1/cmtt/m/n/12 GetLeft m; GetRight
 []

[43]
Overfull \hbox (6.99411pt too wide) in paragraph at lines 1925--1930
[]\OT1/cmr/m/n/12 Integer ar-gu-ment fol-lowed by string ar-gu-ment. As \OT1/cm
tt/m/n/12 SetUnknown
 []


Overfull \hbox (54.7525pt too wide) in paragraph at lines 1944--1946
[]\OT1/cmr/m/n/12 No ar-gu-ments. Turns off the mode in-tro-duced by \OT1/cmtt/
m/n/12 OneConclusion\OT1/cmr/m/n/12 . 
 []

[44] [45]
Overfull \hbox (9.44934pt too wide) in paragraph at lines 2046--2056
[]\OT1/cmr/m/n/12 an in-te-ger ar-gu-ment fol-lowed by three
 []

[46]
Overfull \hbox (3.2503pt too wide) in paragraph at lines 2091--2097
\OT1/cmr/m/n/12 propo-si-tions of the form \OT1/cmtt/m/n/12 Pn(t1,...,tn) \OT1/
cmr/m/n/12 with propo-si-tions \OT1/cmtt/m/n/12 [t1,...,tn]
 []

[47]
Overfull \hbox (6.99411pt too wide) in paragraph at lines 2112--2117
[]\OT1/cmr/m/n/12 Integer ar-gu-ment fol-lowed by string ar-gu-ment. As \OT1/cm
tt/m/n/12 SetUnknown
 []

[48] [49] [50]
Overfull \hbox (17.95296pt too wide) in paragraph at lines 2255--2257
[]\OT1/cmr/m/n/12 Two in-te-ger ar-gu-ments. \OT1/cmtt/m/n/12 Triv m n \OT1/cmr
/m/n/12 has the ef-fect of \OT1/cmtt/m/n/12 GetLeft m; GetRight
 []

[51] [52]
Overfull \hbox (3.1637pt too wide) in paragraph at lines 2338--2340
[]\OT1/cmr/m/n/12 One string ar-gu-ment \OT1/cmtt/m/n/12 name\OT1/cmr/m/n/12 . 
Load the the-ory saved in \OT1/cmtt/m/n/12 name.thy1
 []

[53] (./marcelmanual.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:
 728 strings out of 95847
 8109 string characters out of 1195947
 54292 words of memory out of 1000001
 3690 multiletter control sequences out of 10000+50000
 14069 words of font info for 59 fonts, out of 500000 for 1000
 14 hyphenation exceptions out of 1000
 23i,6n,24p,439b,321s stack positions out of 1500i,500n,5000p,200000b,5000s

Output written on marcelmanual.dvi (53 pages, 126248 bytes).