summaryrefslogtreecommitdiff
path: root/obsolete/macros/generic
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /obsolete/macros/generic
Initial commit
Diffstat (limited to 'obsolete/macros/generic')
-rw-r--r--obsolete/macros/generic/diagrams/barr/diagdoc.tex422
-rw-r--r--obsolete/macros/generic/diagrams/barr/diagram.tex1048
-rw-r--r--obsolete/macros/generic/proofs/taylor/boxproof-old.tex142
-rw-r--r--obsolete/macros/generic/proofs/taylor/boxproof.tex424
4 files changed, 2036 insertions, 0 deletions
diff --git a/obsolete/macros/generic/diagrams/barr/diagdoc.tex b/obsolete/macros/generic/diagrams/barr/diagdoc.tex
new file mode 100644
index 0000000000..5dd69eb2c5
--- /dev/null
+++ b/obsolete/macros/generic/diagrams/barr/diagdoc.tex
@@ -0,0 +1,422 @@
+\documentstyle[12pt]{article}
+\input diagram
+\textheight=9in \topmargin=0pt\headheight=0pt\headsep=0pt
+\textwidth=6.5in \oddsidemargin=0pt
+\begin{document}
+{\catcode`\ =13\global\let =\ \catcode`\^^M=13
+\gdef^^M{\par\noindent}}
+\def\verbatim{\tt
+\catcode`\^^M=13
+\catcode`\ =13
+\catcode`\\=12
+\catcode`\{=12
+\catcode`\}=12
+\catcode`\_=12
+\catcode`\^=12
+\catcode`\&=12
+\catcode`\~=12
+\catcode`\#=12
+\catcode`\%=12
+\catcode`\$=12
+\catcode`|=0
+}
+
+All commercial rights reserved. May be freely distributed
+and used with the following exceptions:\\
+1. No commercial use without explicit permission.\\
+2. It may not be distributed without this notice.
+
+\def\\{{\tt \char 92}}
+
+\section*{The diagram macros}
+The file diagram includes a number of macros for drawing commutative
+diagrams in special shapes as well as more flexible macros to paste
+together more complicated diagrams.
+
+In general, there are two kinds of macros. The first kind has the
+following form
+{\tt \\shape\-name[shape\_\-parameters]} and is intended to be used in
+the following way:
+{\verbatim
+$$
+\shapename[shape_parameters]
+$$
+|egroup
+
+This will create a shape with the given parameters. It operates by
+building its own picture environment.
+
+The second kind of procedure must be used inside a picture environment
+and allows the user to put a diagram of a given size and shape at a
+given place. The usual way in which this is used is:
+
+{\verbatim
+$$
+\bfig
+\putshape1<optional parameters>(x1,y1)[shape_parameters1]
+|dots
+\putshape(xn,yn)<optional parameters>[shape_parametersn]
+\efig
+$$
+|egroup
+
+Here is an example of the first kind of macro. I will have to explain a
+few details before giving examples of the second. The code
+{\verbatim
+$$
+\square[A`B`C`D;f`g`h`k]
+$$
+|egroup
+produces the diagram
+$$
+\square[A`B`C`D;f`g`h`k]
+$$
+and the code
+{\verbatim
+$$
+\Atriangle[A`B`C;f`g`h]
+$$
+|egroup
+produces the diagram
+$$
+\Atriangle[A`B`C;f`g`h]
+$$
+The reason for the shape name will be explained later.
+
+If an arrow label extends especially high or low, the space
+automatically expands to match. For example,
+{\verbatim
+$$
+\square[A`B`C`D;\sum_{i=1}^{\infty}`g`h`\Psi^A_k]
+$$
+|egroup
+will get the diagram
+$$
+\square[A`B`C`D;\sum_{i=1}^{\infty}`g`h`\Psi^A_k]
+$$
+and so on.
+
+Before going on, I will explain about the parameters. Any shape will
+have one or two parameters for height and/or length as well as one
+parameter for each arrow in the diagram. These are in addition to the
+parameters used in the actual procedures. For example, the procedure
+{\verbatim
+$$
+\square<-1`0`2`-3;1000`700>[A`B`C`D;f`g`h`k]
+$$
+|egroup
+gives the square:
+$$
+\square<-1`0`2`-3;1000`700>[A`B`C`D;f`g`h`k]
+$$
+The meaning is as follows. The first four parameters refer to four
+arrows in linguistic order (top, left, right, bottom). A negative
+number gives a backward arrow, while a zero causes it to be omitted. A
+parameter with an absolute value of 1 is ordinary, while 2 gives an
+arrow with a tail (monomorphism) and 3 a double headed arrow
+(epimorphism). The last two parameters determine the width and height,
+respectively, in units of 0.01 em (an em is the width of an M, the
+widest letter in a font). It should be noted that it is not
+possible to give only some of the optional parameters; either all
+must be given or none is.
+
+Here are the shapes. We have already seen the shape {\tt \\square}.
+There are eight different triangles, all isoceles right triangles in
+different orientations. The names all have the form {\tt
+\\xtriangle}, where x is the letter that most closely resembles the
+actual shape of the triangle.
+
+Here are the names, followed by a sample of each one:
+\begin{list}{}{}
+\item{\tt \\btriangle}\samepage
+$$
+\btriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\dtriangle}\samepage
+$$
+\dtriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\ptriangle}\samepage
+$$
+\ptriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\qtriangle}\samepage
+$$
+\qtriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\Atriangle}\samepage
+$$
+\Atriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\Vtriangle}\samepage
+$$
+\Vtriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\Ctriangle}\samepage
+$$
+\Ctriangle[A`B`C;f`g`h]
+$$
+\pagebreak[0]
+\item{\tt \\Dtriangle}\samepage
+$$
+\Dtriangle[A`B`C;f`g`h]
+$$
+\end{list}
+
+In addition, there are two special diagrams that come up often enough to
+be worth having a special macros for.
+\begin{list}{}{}
+\item{\tt \\Atrianglepair}\samepage
+$$
+\Atrianglepair[A`B`C`D;f`g`h`k`l]
+$$
+\item{\tt \\Vtrianglepair}\samepage
+$$
+\Vtrianglepair[A`B`C`D;f`g`h`k`l]
+$$
+\end{list}
+Finally, there is one special shape that is probably not used by very
+many mathematicians. Still I have it and the user might as well share
+it.
+
+{\verbatim
+\recurse[A`B`R`C;s`f_0`f`t_0`t]
+|egroup
+$$
+\recurse[A`B`R`C;s`f_0`f`t_0`t]
+$$
+
+Notice what happens if the first parameter is empty:
+{\verbatim
+\recurse[`B`R`C;s`f_0`f`t_0`t]
+|egroup
+$$
+\recurse[`B`R`C;s`f_0`f`t_0`t]
+$$
+
+This takes care of the simple procedures. The remaining procedures are
+there as building blocks for more complicated diagrams.
+
+These take the form
+\vskip0pt\noindent
+{\tt \\putshape(xpos,ypos)[shape\_parameters]}
+\vskip0pt\noindent
+where
+shape is one of the 11 shapes (excluding {\tt \\recurse}) described
+above
+and the parms are as described there. The parameters {\tt xpos} and
+{\tt ypos} are the offsets from the lower left corner of the picture
+measured in umits of .01 em in the usual \LaTeX\ fashion.
+
+There is one
+more shape which is simply an arrow with an attached label. This is
+called {\tt \\putmorphism} and it is used with the syntax
+\vskip0pt\noindent
+{\tt
+\\putmorphism(xpos,ypos)(run,rise)[node1`node2`label]\{dist\}\{type\}\{loc\}}
+\vskip0pt\noindent
+Here the parameters {\tt xpos} and
+{\tt ypos} are as above. The slope is {\tt rise/run} where {\tt rise}
+and {\tt run} are two numbers that give the slope in accordance with the
+\LaTeX\ rules. That is rise and run must have no common divisor and
+must not exceed 4 in absolute value. In addition, these procedures are
+defined so that rise must not be positive and if it is zero, then run
+must be positive. In other words, all arrows must go in the linguistic
+direction, downwards or to the right. Arrows can be made to go in the
+reverse direction as explained below.
+
+The next three parameters are the node that appears first (in linguistic
+order), the one that appears second and the arrow label. The next
+paramater is the distance in the sense of \LaTeX\ between the centers of
+the nodes. This means it is the horizontal component of the distance,
+unless that is negative, in which case it is the vertical distance. The
+second parameter is the code for the arrowtype, an integer between -3
+and 3 with the same meaning as explained above. Using negative values
+of this parameter allows one to draw an arrow that goes upwards or left.
+Note, however, that node1 is always the node that is above or to the
+left of node2. The last parameter should have the value a,b,l,r or m.
+The values a and b are used only for horizontal arrows and direct the
+arrow label to be placed above or below the arrow. The values l and r
+are used for all other arrows and direct the label to be left or right
+of the arrow. Finally, a vertical arrow only can be given the parameter
+m, in which case the arrow will be gapped and the label placed in the
+middle of the gap.
+
+In general, the simple macros are designed to be used as indicated
+either in the display
+environment or in one of the others, usually
+{\verbatim
+\begin{equation}\begin{array}{c}
+|dots
+\end{array}\end{equation}|egroup
+
+The \\putshape macros must be used inside a picture environment that is
+normally placed inside a display or similar environment. The
+reference point for the positioning parameters is determined as the
+lower left corner of the smallest rectangle with sides parallel to the
+coordinate axes that includes the center points of all nodes on its
+border. This rectangle will be degenerate in the case of a horizontal
+or vertical morphism. The reference point may either be on or outside
+the actual figure. For example, in the case of the btriangle, it is the
+center of the lower left node, while for a qtriangle it is outside the
+triangle itself being the fourth corner of the enclosing square.
+
+The macros are made so that they fit together well. That is why all
+distances are from node centers to node centers. If a vertex is part of
+two shapes, it is probably best not to repeat it, since it is
+conceivable that round-off errors will cause its two appearances to be
+slightly offset. It can either be omitted or, since the width is used
+to determine the amount to shorten horizontal arrows, replaced by {\tt
+\\phantom} versions. Both methods are illustrated in the example given
+at the end.
+
+A somewhat baroque (but taken from an actual text) example illustrates
+most of these points.
+{\verbatim
+$$
+\bfig
+\putmorphism(0,2100)(0,-1)[``T\eta'T]{1400}1l
+\putmorphism(0,2100)(1,0)[TT`T`\mu]{700}1a
+\putmorphism(0,2100)(1,-1)[`TTT'`TT\eta']{700}1l
+\putmorphism(700,2100)(1,-1)[`TT'`T\eta]{700}1r
+\put(700,1750){\makebox(0,0){1}}
+\putmorphism(700,1420)(1,0)[\phantom{TTT'}`\phantom{TT'}`\mu
+ T']{700}1a
+\putmorphism(700,1380)(1,0)[\phantom{TTT'}`%
+ \phantom{TT'}`T\sigma]{700}1b
+\putsquare<0`1`1`1;700`700>(700,700)[TTT'`TT'`TT'TT'`TT'T';`T\eta'TT'``]
+\putmorphism(700,700)(1,0)[\phantom{TT'TT'}`%
+ \phantom{TT'T'}`TT'\sigma]{700}1a
+\put(300,1400){\makebox(0,0){2}}
+\put(950,1050){\makebox(0,0){3}}
+\putbtriangle<0`1`0;700>(1400,700)[``TT';T\eta'T'`id`]
+\putmorphism(1400,700)(1,0)[\phantom{TT'T'}`%
+ \phantom{TT'}`T\mu']{700}1a
+\put(1600,1050){\makebox(0,0){6}}
+\putsquare<1`1`0`1;700`700>(0,0)[TT'T`\phantom{TT'TT'}`T'T`T'TT';%
+ TT'T\eta'`\sigma T``T'T\eta']
+\putmorphism(700,0)(1,0)[\phantom{T'TT'}`%
+ \phantom{T'T'}`T'\sigma]{700}1b
+\putsquare<0`0`1`1;700`700>(1400,0)[``T'T'`T';``\sigma`\mu']
+\putmorphism(700,700)(0,-1)[``\sigma TT']{700}1m
+\putmorphism(1400,700)(0,-1)[``\sigma T']{700}1m
+\put(300,350){\makebox(0,0){4}}
+\put(1050,350){\makebox(0,0){5}}
+\put(1750,350){\makebox(0,0){7}}
+\efig
+$$
+|egroup
+which produces
+$$
+\bfig
+\putmorphism(0,2100)(0,-1)[``T\eta'T]{1400}1l
+\putmorphism(0,2100)(1,0)[TT`T`\mu]{700}1a
+\putmorphism(0,2100)(1,-1)[`TTT'`TT\eta']{700}1l
+\putmorphism(700,2100)(1,-1)[`TT'`T\eta]{700}1r
+\put(700,1750){\makebox(0,0){1}}
+\putmorphism(700,1420)(1,0)[\phantom{TTT'}`\phantom{TT'}`\mu
+ T']{700}1a
+\putmorphism(700,1380)(1,0)[\phantom{TTT'}`%
+ \phantom{TT'}`T\sigma]{700}1b
+\putsquare<0`1`1`1;700`700>(700,700)[TTT'`TT'`TT'TT'`TT'T';`T\eta'TT'``]
+\putmorphism(700,700)(1,0)[\phantom{TT'TT'}`%
+ \phantom{TT'T'}`TT'\sigma]{700}1a
+\put(300,1400){\makebox(0,0){2}}
+\put(950,1050){\makebox(0,0){3}}
+\putbtriangle<0`1`0;700>(1400,700)[``TT';T\eta'T'`id`]
+\putmorphism(1400,700)(1,0)[\phantom{TT'T'}`%
+ \phantom{TT'}`T\mu']{700}1a
+\put(1600,1050){\makebox(0,0){6}}
+\putsquare<1`1`0`1;700`700>(0,0)[TT'T`\phantom{TT'TT'}`T'T`T'TT';%
+ TT'T\eta'`\sigma T``T'T\eta']
+\putmorphism(700,0)(1,0)[\phantom{T'TT'}`%
+ \phantom{T'T'}`T'\sigma]{700}1b
+\putsquare<0`0`1`1;700`700>(1400,0)[``T'T'`T';``\sigma`\mu']
+\putmorphism(700,700)(0,-1)[``\sigma TT']{700}1m
+\putmorphism(1400,700)(0,-1)[``\sigma T']{700}1m
+\put(300,350){\makebox(0,0){4}}
+\put(1050,350){\makebox(0,0){5}}
+\put(1750,350){\makebox(0,0){7}}
+\efig
+$$
+
+Here is a page of samples of the results from the various
+{\tt\\putshapes}. The code
+{\verbatim
+$$
+\bfig
+\putsquare(0,0)[A`B`C`D;f`g`h`k]
+\putbtriangle(0,1500)[A`B`C;f`g`h]
+\putdtriangle(2200,1500)[A`B`C;f`g`h]
+\putptriangle(0,3000)[A`B`C;f`g`h]
+\putqtriangle(1000,500)[A`B`C;f`g`h]
+\putCtriangle(1500,750)[A`B`C;f`g`h]
+\putDtriangle(700,1000)[A`B`C;f`g`h]
+\putAtriangle(2000,2200)[A`B`C;f`g`h]
+\putAtrianglepair(0,2500)[A`B`C`D;f`g`h`k`l]
+\putVtriangle(2000,3000)[A`B`C;f`g`h]
+\putVtrianglepair(1000,2500)[A`B`C`D;f`g`h`k`l]
+\efig
+$$
+|egroup
+produces the diagram:
+$$
+\bfig
+\putsquare(0,0)[A`B`C`D;f`g`h`k]
+\putbtriangle(0,1500)[A`B`C;f`g`h]
+\putdtriangle(2200,1500)[A`B`C;f`g`h]
+\putptriangle(0,3000)[A`B`C;f`g`h]
+\putqtriangle(1000,500)[A`B`C;f`g`h]
+\putCtriangle(1500,750)[A`B`C;f`g`h]
+\putDtriangle(700,1000)[A`B`C;f`g`h]
+\putAtriangle(2000,2200)[A`B`C;f`g`h]
+\putAtrianglepair(0,2500)[A`B`C`D;f`g`h`k`l]
+\putVtriangle(2000,3000)[A`B`C;f`g`h]
+\putVtrianglepair(1000,2500)[A`B`C`D;f`g`h`k`l]
+\efig
+$$
+
+Added: For horizontal and vertical lines only, arrow parameters of
+$\pm4$, $\pm5$ and $\pm6$ will give dashed lines.
+
+Here is a double cube:
+{\verbatim
+$$
+\bfig
+\putsquare(0,750)[A`B`C`D;```]
+\putsquare(0,250)[\phantom{C}`\phantom{D}`E`F;```]
+\putsquare(250,500)[A'`B'`C'`D';```]
+\putsquare(250,0)[\phantom{C'}`\phantom{D'}`E'`F';```]
+\putmorphism(0,1250)(1,-1)[```]{250}1a
+\putmorphism(500,1250)(1,-1)[```]{250}1a
+\putmorphism(0,750)(1,-1)[```]{250}1a
+\putmorphism(500,750)(1,-1)[```]{250}1a
+\putmorphism(0,250)(1,-1)[```]{250}1a
+\putmorphism(500,250)(1,-1)[```]{250}1a
+\efig
+$$
+|egroup
+$$
+\bfig
+\putsquare(0,750)[A`B`C`D;```]
+\putsquare(0,250)[\phantom{C}`\phantom{D}`E`F;```]
+\putsquare(250,500)[A'`B'`C'`D';```]
+\putsquare(250,0)[\phantom{C'}`\phantom{D'}`E'`F';```]
+\putmorphism(0,1250)(1,-1)[```]{250}1a
+\putmorphism(500,1250)(1,-1)[```]{250}1a
+\putmorphism(0,750)(1,-1)[```]{250}1a
+\putmorphism(500,750)(1,-1)[```]{250}1a
+\putmorphism(0,250)(1,-1)[```]{250}1a
+\putmorphism(500,250)(1,-1)[```]{250}1a
+\efig
+$$
+
+
+
+\end{document}
diff --git a/obsolete/macros/generic/diagrams/barr/diagram.tex b/obsolete/macros/generic/diagrams/barr/diagram.tex
new file mode 100644
index 0000000000..2a322759d3
--- /dev/null
+++ b/obsolete/macros/generic/diagrams/barr/diagram.tex
@@ -0,0 +1,1048 @@
+% This should appear in a file named diagram.tex
+% Copyright 1988,1989 Michael Barr
+% Department of Mathematics and Statistics
+% McGill University
+% 805 Sherbrooke St., W
+% Montreal, Quebec, Canada
+% H3P 1S4
+%
+% barr@triples.math.mcgill.ca
+%
+% All commercial rights reserved. May be freely distributed
+% and used with the following exceptions:
+% 1. No commercial use without explicit permission.
+% 2. It may not be used by any employee of a telephone
+% company.
+% 3. It may not be distributed without this notice.
+%
+% Last revised 91-05-04
+
+% Ascii character test:
+% 32: 33: ! 34: " 35: # 36: $ 37: % 38: & 39: '
+% 40: ( 41: ) 42: * 43: + 44: , 45: - 46: . 47: /
+% 48: 0 49: 1 50: 2 51: 3 52: 4 53: 5 54: 6 55: 7
+% 56: 8 57: 9 58: : 59: ; 60: < 61: = 62: > 63: ?
+% 64: @ 65: A 66: B 67: C 68: D 69: E 70: F 71: G
+% 72: H 73: I 74: J 75: K 76: L 77: M 78: N 79: O
+% 80: P 81: Q 82: R 83: S 84: T 85: U 86: V 87: W
+% 88: X 89: Y 90: Z 91: [ 92: \ 93: ] 94: ^ 95: _
+% 96: ` 97: a 98: b 99: c 100: d 101: e 102: f 103: g
+% 104: h 105: i 106: j 107: k 108: l 109: m 110: n 111: o
+% 112: p 113: q 114: r 115: s 116: t 117: u 118: v 119: w
+% 120: x 121: y 122: z 123: { 124: | 125: } 126: ~
+
+
+\makeatletter
+
+\def\diagram{\m@th\leftwidth=\z@ \rightwidth=\z@ \topheight=\z@
+\botheight=\z@ \setbox\@picbox\hbox\bgroup}
+
+\def\enddiagram{\egroup\wd\@picbox\rightwidth\unitlength
+\ht\@picbox\topheight\unitlength \dp\@picbox\botheight\unitlength
+\hskip\leftwidth\unitlength\box\@picbox}
+
+\def\bfig{\begin{diagram}}
+\def\efig{\end{diagram}}
+\newcount\wideness \newcount\leftwidth \newcount\rightwidth
+\newcount\highness \newcount\topheight \newcount\botheight
+
+\def\ratchet#1#2{\ifnum#1<#2 \global #1=#2 \fi}
+
+\def\putbox(#1,#2)#3{%
+\horsize{\wideness}{#3} \divide\wideness by 2
+{\advance\wideness by #1 \ratchet{\rightwidth}{\wideness}}
+{\advance\wideness by -#1 \ratchet{\leftwidth}{\wideness}}
+\vertsize{\highness}{#3} \divide\highness by 2
+{\advance\highness by #2 \ratchet{\topheight}{\highness}}
+{\advance\highness by -#2 \ratchet{\botheight}{\highness}}
+\put(#1,#2){\makebox(0,0){$#3$}}}
+
+\def\putlbox(#1,#2)#3{%
+\horsize{\wideness}{#3}
+{\advance\wideness by #1 \ratchet{\rightwidth}{\wideness}}
+{\ratchet{\leftwidth}{-#1}}
+\vertsize{\highness}{#3} \divide\highness by 2
+{\advance\highness by #2 \ratchet{\topheight}{\highness}}
+{\advance\highness by -#2 \ratchet{\botheight}{\highness}}
+\put(#1,#2){\makebox(0,0)[l]{$#3$}}}
+
+\def\putrbox(#1,#2)#3{%
+\horsize{\wideness}{#3}
+{\ratchet{\rightwidth}{#1}}
+{\advance\wideness by -#1 \ratchet{\leftwidth}{\wideness}}
+\vertsize{\highness}{#3} \divide\highness by 2
+{\advance\highness by #2 \ratchet{\topheight}{\highness}}
+{\advance\highness by -#2 \ratchet{\botheight}{\highness}}
+\put(#1,#2){\makebox(0,0)[r]{$#3$}}}
+
+
+\def\adjust[#1]{} % For compatibility
+
+\newcount \coefa
+\newcount \coefb
+\newcount \coefc
+\newcount\tempcounta
+\newcount\tempcountb
+\newcount\tempcountc
+\newcount\tempcountd
+\newcount\xext
+\newcount\yext
+\newcount\xoff
+\newcount\yoff
+\newcount\gap%
+\newcount\arrowtypea
+\newcount\arrowtypeb
+\newcount\arrowtypec
+\newcount\arrowtyped
+\newcount\arrowtypee
+\newcount\height
+\newcount\width
+\newcount\xpos
+\newcount\ypos
+\newcount\run
+\newcount\rise
+\newcount\arrowlength
+\newcount\halflength
+\newcount\arrowtype
+\newdimen\tempdimen
+\newdimen\xlen
+\newdimen\ylen
+\newsavebox{\tempboxa}%
+\newsavebox{\tempboxb}%
+\newsavebox{\tempboxc}%
+
+\newdimen\w@dth
+
+\def\setw@dth#1#2{\setbox\z@\hbox{\m@th$#1$}\w@dth=\wd\z@
+\setbox\@ne\hbox{\m@th$#2$}\ifnum\w@dth<\wd\@ne \w@dth=\wd\@ne \fi
+\advance\w@dth by 1.2em}
+
+%The definitions below look more elaborate than they need to be.
+%The reason is that an empty asscript will still cause extra vertical
+%spacing and the only way to avoid ugly extra space seems to be using
+%some such method as this.
+
+\def\t@^#1_#2{\allowbreak\def\n@one{#1}\def\n@two{#2}\mathrel
+{\setw@dth{#1}{#2}
+\mathop{\hbox to \w@dth{\rightarrowfill}}\limits
+\ifx\n@one\empty\else ^{\box\z@}\fi
+\ifx\n@two\empty\else _{\box\@ne}\fi}}
+%\def\t@^#1_#2{\mathrel{\mathop{\hbox{\rightarrowfill}}\limits
+%^{\mkern12mu#1\mkern12mu}_{\mkern12mu#2\mkern12mu}}}
+\def\t@@^#1{\@ifnextchar_{\t@^{#1}}{\t@^{#1}_{}}}
+\def\to{\@ifnextchar^{\t@@}{\t@@^{}}}
+
+\def\t@left^#1_#2{\def\n@one{#1}\def\n@two{#2}\mathrel{\setw@dth{#1}{#2}
+\mathop{\hbox to \w@dth{\leftarrowfill}}\limits
+\ifx\n@one\empty\else ^{\box\z@}\fi
+\ifx\n@two\empty\else _{\box\@ne}\fi}}
+%\def\t@left^#1_#2{\mathrel{\mathop{\hbox{\leftarrowfill}}\limits
+%^{\mkern12mu#1\mkern12mu}_{\mkern12mu#2\mkern12mu}}}
+\def\t@@left^#1{\@ifnextchar_{\t@left^{#1}}{\t@left^{#1}_{}}}
+\def\toleft{\@ifnextchar^{\t@@left}{\t@@left^{}}}
+
+\def\two@^#1_#2{\allowbreak
+\def\n@one{#1}\def\n@two{#2}\mathrel{\setw@dth{#1}{#2}
+\mathop{\vcenter{\lineskip\z@\baselineskip\z@
+ \hbox to \w@dth{\rightarrowfill}%
+ \hbox to \w@dth{\rightarrowfill}}%
+ }\limits
+\ifx\n@one\empty\else ^{\box\z@}\fi
+\ifx\n@two\empty\else _{\box\@ne}\fi}}
+\def\tw@@^#1{\@ifnextchar _{\two@^{#1}}{\two@^{#1}_{}}}
+\def\two{\@ifnextchar ^{\tw@@}{\tw@@^{}}}
+
+\def\tofr@^#1_#2{\def\n@one{#1}\def\n@two{#2}\mathrel{\setw@dth{#1}{#2}
+\mathop{\vcenter{\hbox to \w@dth{\rightarrowfill}\kern-1.7ex
+ \hbox to \w@dth{\leftarrowfill}}%
+ }\limits
+\ifx\n@one\empty\else ^{\box\z@}\fi
+\ifx\n@two\empty\else _{\box\@ne}\fi}}
+\def\t@fr@^#1{\@ifnextchar_ {\tofr@^{#1}}{\tofr@^{#1}_{}}}
+\def\tofro{\@ifnextchar^ {\t@fr@}{\t@fr@^{}}}
+
+\def\epi{\mathop{\mathchar"221\mkern -12mu\mathchar"221}\limits}
+\def\leftepi{\mathop{\mathchar"220\mkern -12mu\mathchar"220}\limits}
+\def\mon{\mathop{\m@th\hbox to
+ 14.6\P@{\lasyb\char'51\hskip-2.1\P@$\arrext$\hss
+$\mathord\rightarrow$}}\limits} % width of \epi
+\def\leftmono{\mathrel{\m@th\hbox to
+14.6\P@{$\mathord\leftarrow$\hss$\arrext$\hskip-2.1\P@\lasyb\char'50%
+}}\limits} % width of \epi
+\mathchardef\arrext="0200 % amr minus for arrow extension (see \into)
+
+
+\setlength{\unitlength}{.01em}%
+\def\settypes(#1,#2,#3){\arrowtypea#1 \arrowtypeb#2 \arrowtypec#3}
+\def\settoheight#1#2{\setbox\@tempboxa\hbox{#2}#1\ht\@tempboxa\relax}%
+\def\settodepth#1#2{\setbox\@tempboxa\hbox{#2}#1\dp\@tempboxa\relax}%
+\def\settokens`#1`#2`#3`#4`{%
+ \def\tokena{#1}\def\tokenb{#2}\def\tokenc{#3}\def\tokend{#4}}
+\def\setsqparms[#1`#2`#3`#4;#5`#6]{%
+\arrowtypea #1
+\arrowtypeb #2
+\arrowtypec #3
+\arrowtyped #4
+\width #5
+\height #6
+}
+\def\setpos(#1,#2){\xpos=#1 \ypos#2}
+
+
+
+\def\settriparms[#1`#2`#3;#4]{\settripairparms[#1`#2`#3`1`1;#4]}%
+
+\def\settripairparms[#1`#2`#3`#4`#5;#6]{%
+\arrowtypea #1
+\arrowtypeb #2
+\arrowtypec #3
+\arrowtyped #4
+\arrowtypee #5
+\width #6
+\height #6
+}
+
+\def\resetparms{\settripairparms[1`1`1`1`1;500]\width 500}%default values%
+
+\resetparms
+
+\def\mvector(#1,#2)#3{%%
+\put(0,0){\vector(#1,#2){#3}}%
+\put(0,0){\vector(#1,#2){26}}%
+}
+\def\evector(#1,#2)#3{{%%
+\arrowlength #3
+\put(0,0){\vector(#1,#2){\arrowlength}}%
+\advance \arrowlength by-30
+\put(0,0){\vector(#1,#2){\arrowlength}}%
+}}
+
+\def\horsize#1#2{%
+\settowidth{\tempdimen}{$#2$}%
+#1=\tempdimen
+\divide #1 by\unitlength
+}
+
+\def\vertsize#1#2{%
+\settoheight{\tempdimen}{$#2$}%
+#1=\tempdimen
+\settodepth{\tempdimen}{$#2$}%
+\advance #1 by\tempdimen
+\divide #1 by\unitlength
+}
+
+\def\putvector(#1,#2)(#3,#4)#5#6{{%
+\ifnum3<\arrowtype
+\putdashvector(#1,#2)(#3,#4)#5\arrowtype
+\else
+\ifnum\arrowtype<-3
+\putdashvector(#1,#2)(#3,#4)#5\arrowtype
+\else
+\xpos=#1
+\ypos=#2
+\run=#3
+\rise=#4
+\arrowlength=#5
+\ifnum \arrowtype<0
+ \ifnum \run=0
+ \advance \ypos by-\arrowlength
+ \else
+ \tempcounta \arrowlength
+ \multiply \tempcounta by\rise
+ \divide \tempcounta by\run
+ \ifnum\run>0
+ \advance \xpos by\arrowlength
+ \advance \ypos by\tempcounta
+ \else
+ \advance \xpos by-\arrowlength
+ \advance \ypos by-\tempcounta
+ \fi
+ \fi
+ \multiply \arrowtype by-1
+ \multiply \rise by-1
+ \multiply \run by-1
+\fi
+\ifcase \arrowtype
+\or \put(\xpos,\ypos){\vector(\run,\rise){\arrowlength}}%
+\or \put(\xpos,\ypos){\mvector(\run,\rise)\arrowlength}%
+\or \put(\xpos,\ypos){\evector(\run,\rise){\arrowlength}}%
+\fi\fi\fi
+}}
+
+\def\putsplitvector(#1,#2)#3#4{%%
+\xpos #1
+\ypos #2
+\arrowtype #4
+\halflength #3
+\arrowlength #3
+\gap 140
+\advance \halflength by-\gap
+\divide \halflength by2
+\ifnum\arrowtype>0
+ \ifcase \arrowtype
+ \or \put(\xpos,\ypos){\line(0,-1){\halflength}}%
+ \advance\ypos by-\halflength
+ \advance\ypos by-\gap
+ \put(\xpos,\ypos){\vector(0,-1){\halflength}}%
+ \or \put(\xpos,\ypos){\line(0,-1)\halflength}%
+ \put(\xpos,\ypos){\vector(0,-1)3}%
+ \advance\ypos by-\halflength
+ \advance\ypos by-\gap
+ \put(\xpos,\ypos){\vector(0,-1){\halflength}}%
+ \or \put(\xpos,\ypos){\line(0,-1)\halflength}%
+ \advance\ypos by-\halflength
+ \advance\ypos by-\gap
+ \put(\xpos,\ypos){\evector(0,-1){\halflength}}%
+ \fi
+\else \arrowtype=-\arrowtype
+ \ifcase\arrowtype
+ \or \advance \ypos by-\arrowlength
+ \put(\xpos,\ypos){\line(0,1){\halflength}}%
+ \advance\ypos by\halflength
+ \advance\ypos by\gap
+ \put(\xpos,\ypos){\vector(0,1){\halflength}}%
+ \or \advance \ypos by-\arrowlength
+ \put(\xpos,\ypos){\line(0,1)\halflength}%
+ \put(\xpos,\ypos){\vector(0,1)3}%
+ \advance\ypos by\halflength
+ \advance\ypos by\gap
+ \put(\xpos,\ypos){\vector(0,1){\halflength}}%
+ \or \advance \ypos by-\arrowlength
+ \put(\xpos,\ypos){\line(0,1)\halflength}%
+ \advance\ypos by\halflength
+ \advance\ypos by\gap
+ \put(\xpos,\ypos){\evector(0,1){\halflength}}%
+ \fi
+\fi
+}
+
+\def\putmorphism(#1)(#2,#3)[#4`#5`#6]#7#8#9{{%
+\run #2
+\rise #3
+\ifnum\rise=0
+ \puthmorphism(#1)[#4`#5`#6]{#7}{#8}#9%
+\else\ifnum\run=0
+ \putvmorphism(#1)[#4`#5`#6]{#7}{#8}#9%
+\else
+\setpos(#1)%
+\arrowlength #7
+\arrowtype #8
+\ifnum\run=0
+\else\ifnum\rise=0
+\else
+\ifnum\run>0
+ \coefa=1
+\else
+ \coefa=-1
+\fi
+\ifnum\arrowtype>0
+ \coefb=0
+ \coefc=-1
+\else
+ \coefb=\coefa
+ \coefc=1
+ \arrowtype=-\arrowtype
+\fi
+\width=2
+\multiply \width by\run
+\divide \width by\rise
+\ifnum \width<0 \width=-\width\fi
+\advance\width by60
+\if l#9 \width=-\width\fi
+\putbox(\xpos,\ypos){#4}% %node 1
+{\multiply \coefa by\arrowlength% %node 2
+\advance\xpos by\coefa
+\multiply \coefa by\rise
+\divide \coefa by\run
+\advance \ypos by\coefa
+\putbox(\xpos,\ypos){#5} }%
+{\multiply \coefa by\arrowlength% %label
+\divide \coefa by2
+\advance \xpos by\coefa
+\advance \xpos by\width
+\multiply \coefa by\rise
+\divide \coefa by\run
+\advance \ypos by\coefa
+\if l#9%
+ \putrbox(\xpos,\ypos){#6}%
+\else\if r#9%
+ \putlbox(\xpos,\ypos){#6}%
+\fi\fi }%
+{\multiply \rise by-\coefc% %arrow
+\multiply \run by-\coefc
+\multiply \coefb by\arrowlength
+\advance \xpos by\coefb
+\multiply \coefb by\rise
+\divide \coefb by\run
+\advance \ypos by\coefb
+\multiply \coefc by70
+\advance \ypos by\coefc
+\multiply \coefc by\run
+\divide \coefc by\rise
+\advance \xpos by\coefc
+\multiply \coefa by140
+\multiply \coefa by\run
+\divide \coefa by\rise
+\advance \arrowlength by\coefa
+\ifcase\arrowtype
+\or \put(\xpos,\ypos){\vector(\run,\rise){\arrowlength}}%
+\or \put(\xpos,\ypos){\mvector(\run,\rise){\arrowlength}}%
+\or \put(\xpos,\ypos){\evector(\run,\rise){\arrowlength}}%
+\fi}\fi\fi\fi\fi}}
+
+
+\newcount\numbdashes \newcount\lengthdash \newcount\increment
+
+\def\howmanydashes{% Actually returns both number and length
+\numbdashes=\arrowlength \lengthdash=40
+\divide\numbdashes by \lengthdash
+\lengthdash=\arrowlength
+\divide\lengthdash by \numbdashes
+%This futzing around is to minimize round-off error.
+\increment=\lengthdash
+\multiply\lengthdash by 3
+\divide\lengthdash by 5
+}
+
+\def\putdashvector(#1)(#2,#3)#4#5{%
+\ifnum#3=0 \putdashhvector(#1){#4}#5
+\else
+\ifnum#2=0
+\putdashvvector(#1){#4}#5\fi\fi}
+
+\def\putdashhvector(#1,#2)#3#4{{%
+\arrowlength=#3 \howmanydashes
+\multiput(#1,#2)(\increment,0){\numbdashes}%
+{\vrule height .4pt width \lengthdash\unitlength}
+\arrowtype=#4 \xpos=#1
+\ifnum\arrowtype<0 \advance\arrowtype by 7 \fi
+\ifcase\arrowtype
+\or \advance\xpos by 10
+ \put(\xpos,#2){\vector(-1,0){\lengthdash}}
+ \advance\xpos by 40
+ \put(\xpos,#2){\vector(-1,0){\lengthdash}}
+\or \advance \xpos by 10
+ \put(\xpos,#2){\vector(-1,0){\lengthdash}}
+ \advance\xpos by \arrowlength
+ \advance\xpos by -50
+ \put(\xpos,#2){\vector(-1,0){\lengthdash}}
+\or \advance\xpos by 10
+ \put(\xpos,#2){\vector(-1,0){\lengthdash}}
+\or \advance\xpos by \arrowlength
+ \advance\xpos by -\lengthdash
+ \put(\xpos,#2){\vector(1,0){\lengthdash}}
+\or {\advance\xpos by 10
+ \put(\xpos,#2){\vector(1,0){\lengthdash}}}
+ \advance\xpos by \arrowlength
+ \advance\xpos by -\lengthdash
+ \put(\xpos,#2){\vector(1,0){\lengthdash}}
+\or \advance\xpos by \arrowlength
+ \advance\xpos by -\lengthdash
+ \put(\xpos,#2){\vector(1,0){\lengthdash}}
+ \advance\xpos by -40
+ \put(\xpos,#2){\vector(1,0){\lengthdash}}
+ \fi
+}}
+
+\def\putdashvvector(#1,#2)#3#4{{%
+\arrowlength=#3 \howmanydashes
+\ypos=#2 \advance\ypos by -\arrowlength
+\multiput(#1,#2)(0,\increment){\numbdashes}%
+ {\vrule width .4pt height \lengthdash\unitlength}
+\arrowtype=#4 \ypos=#2
+\ifnum\arrowtype<0 \advance\arrowtype by 7 \fi
+\ifcase\arrowtype
+\or \advance\ypos by \arrowlength \advance\ypos by -40
+ \put(#1,\ypos){\vector(0,1){\lengthdash}}
+ \advance\ypos by -40
+ \put(#1,\ypos){\vector(0,1){\lengthdash}}
+\or \advance\ypos by 10
+ \put(#1,\ypos){\vector(0,1){\lengthdash}}
+ \advance\ypos by \arrowlength \advance\ypos by -40
+ \put(#1,\ypos){\vector(0,1){\lengthdash}}
+\or \advance\ypos by \arrowlength \advance\ypos by -40
+ \put(#1,\ypos){\vector(0,1){\lengthdash}}
+\or \advance\ypos by 10
+ \put(#1,\ypos){\vector(0,-1){\lengthdash}}
+\or \advance\ypos by 10
+ \put(#1,\ypos){\vector(0,-1){\lengthdash}}
+ \advance\ypos by \arrowlength \advance\ypos by -40
+ \put(#1,\ypos){\vector(0,-1){\lengthdash}}
+\or \advance\ypos by 10
+ \put(#1,\ypos){\vector(0,-1){\lengthdash}}
+ \advance\ypos by 40
+ \put(#1,\ypos){\vector(0,-1){\lengthdash}}
+\fi
+}}
+
+\def\puthmorphism(#1,#2)[#3`#4`#5]#6#7#8{{%
+\xpos #1
+\ypos #2
+\width #6
+\arrowlength #6
+\arrowtype=#7
+\putbox(\xpos,\ypos){#3\vphantom{#4}}%
+{\advance \xpos by\arrowlength
+\putbox(\xpos,\ypos){\vphantom{#3}#4}}%
+\horsize{\tempcounta}{#3}%
+\horsize{\tempcountb}{#4}%
+\divide \tempcounta by2
+\divide \tempcountb by2
+\advance \tempcounta by30
+\advance \tempcountb by30
+\advance \xpos by\tempcounta
+\advance \arrowlength by-\tempcounta
+\advance \arrowlength by-\tempcountb
+\putvector(\xpos,\ypos)(1,0)\arrowlength\arrowtype
+\divide \arrowlength by2
+\advance \xpos by\arrowlength
+\vertsize{\tempcounta}{#5}%
+\divide\tempcounta by2
+\advance \tempcounta by20
+\if a#8 %
+ \advance \ypos by\tempcounta
+ \putbox(\xpos,\ypos){#5}%
+\else
+ \advance \ypos by-\tempcounta
+ \putbox(\xpos,\ypos){#5}%
+\fi}}
+
+\def\putvmorphism(#1,#2)[#3`#4`#5]#6#7#8{{%
+\xpos #1
+\ypos #2
+\arrowlength #6
+\arrowtype #7
+\settowidth{\xlen}{$#5$}%
+\putbox(\xpos,\ypos){#3}%
+{\advance \ypos by-\arrowlength
+\putbox(\xpos,\ypos){#4}}%
+{\advance\arrowlength by-140
+\advance \ypos by-70
+\ifdim\xlen>0pt
+ \if m#8%
+ \putsplitvector(\xpos,\ypos)\arrowlength\arrowtype
+ \else
+ \putvector(\xpos,\ypos)(0,-1)\arrowlength\arrowtype
+ \fi
+\else
+ \putvector(\xpos,\ypos)(0,-1)\arrowlength\arrowtype
+\fi}%
+\ifdim\xlen>0pt
+ \divide \arrowlength by2
+ \advance\ypos by-\arrowlength
+ \if l#8%
+ \advance \xpos by-40
+ \putrbox(\xpos,\ypos){#5}%
+ \else\if r#8%
+ \advance \xpos by40
+ \putlbox(\xpos,\ypos){#5}%
+ \else
+ \putbox(\xpos,\ypos){#5}%
+ \fi\fi
+\fi
+}}
+
+\def\putsquarep<#1>(#2)[#3;#4`#5`#6`#7]{{%
+\setsqparms[#1]%
+\setpos(#2)%
+\settokens`#3`%
+\puthmorphism(\xpos,\ypos)[\tokenc`\tokend`{#7}]{\width}{\arrowtyped}b%
+\advance\ypos by \height
+\puthmorphism(\xpos,\ypos)[\tokena`\tokenb`{#4}]{\width}{\arrowtypea}a%
+\putvmorphism(\xpos,\ypos)[``{#5}]{\height}{\arrowtypeb}l%
+\advance\xpos by \width
+\putvmorphism(\xpos,\ypos)[``{#6}]{\height}{\arrowtypec}r%
+}}
+
+\def\putsquare{\@ifnextchar <{\putsquarep}{\putsquarep%
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped;\width`\height>}}
+\def\square{\@ifnextchar< {\squarep}{\squarep
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped;\width`\height>}}
+ % #6
+\def\squarep<#1>[#2`#3`#4`#5;#6`#7`#8`#9]{{% % #2------>#3
+\setsqparms[#1]% % | |
+\diagram% % | |
+\putsquarep<\arrowtypea`\arrowtypeb`\arrowtypec`% % #7| |#8
+\arrowtyped;\width`\height>% % | |
+(0,0)[#2`#3`#4`{#5};#6`#7`#8`{#9}]% % | |
+\enddiagram% % v v
+}} % #4------>#5
+ % #9
+\def\putptrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\advance\ypos by \height
+\puthmorphism(\xpos,\ypos)[#4`#5`{#7}]{\height}{\arrowtypea}a%
+\putvmorphism(\xpos,\ypos)[`#6`{#8}]{\height}{\arrowtypeb}l%
+\advance\xpos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[``{#9}]{\height}{\arrowtypec}r%
+}}
+
+\def\putptriangle{\@ifnextchar <{\putptrianglep}{\putptrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\ptriangle{\@ifnextchar <{\ptrianglep}{\ptrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #5
+\def\ptrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % #2----->#3
+\settriparms[#1]% % | /
+\diagram% % | /
+\putptrianglep<\arrowtypea`\arrowtypeb`% % #6| /#7
+\arrowtypec;\height>% % | /
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % | /
+\enddiagram%% % v v
+}} % #4
+
+\def\putqtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\advance\ypos by\height
+\puthmorphism(\xpos,\ypos)[#4`#5`{#7}]{\height}{\arrowtypea}a%
+\putmorphism(\xpos,\ypos)(1,-1)[``{#8}]{\height}{\arrowtypeb}l%
+\advance\xpos by\height
+\putvmorphism(\xpos,\ypos)[`#6`{#9}]{\height}{\arrowtypec}r%
+}}
+
+\def\putqtriangle{\@ifnextchar <{\putqtrianglep}{\putqtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\qtriangle{\@ifnextchar <{\qtrianglep}{\qtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #5
+\def\qtrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % #2----->#3
+\settriparms[#1]% % \ |
+\width=\height % \ |
+\diagram% % #6\ |#7
+\putqtrianglep<\arrowtypea`\arrowtypeb`% % \ |
+\arrowtypec;\height>% % \ |
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % v v
+\enddiagram%% % #4
+}}
+
+\def\putdtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\puthmorphism(\xpos,\ypos)[#5`#6`{#9}]{\height}{\arrowtypec}b%
+\advance\xpos by \height \advance\ypos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[``{#7}]{\height}{\arrowtypea}l%
+\putvmorphism(\xpos,\ypos)[#4``{#8}]{\height}{\arrowtypeb}r%
+}}
+
+\def\putdtriangle{\@ifnextchar <{\putdtrianglep}{\putdtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\dtriangle{\@ifnextchar <{\dtrianglep}{\dtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #2
+\def\dtrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % / |
+\settriparms[#1]% % / |
+\width=\height % #5/ |#6
+\diagram% % / |
+\putdtrianglep<\arrowtypea`\arrowtypeb`% % / |
+\arrowtypec;\height>% % v v
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % #3----->#4
+\enddiagram%% % #7
+}}
+
+\def\putbtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\puthmorphism(\xpos,\ypos)[#5`#6`{#9}]{\height}{\arrowtypec}b%
+\advance\ypos by\height
+\putmorphism(\xpos,\ypos)(1,-1)[``{#8}]{\height}{\arrowtypeb}r%
+\putvmorphism(\xpos,\ypos)[#4``{#7}]{\height}{\arrowtypea}l%
+}}
+
+\def\putbtriangle{\@ifnextchar <{\putbtrianglep}{\putbtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\btriangle{\@ifnextchar <{\btrianglep}{\btrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #2
+\def\btrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % | \
+\settriparms[#1]% % | \
+\width=\height % #5| \#6
+\diagram% % | \
+\putbtrianglep<\arrowtypea`\arrowtypeb`% % | \
+\arrowtypec;\height>% % v v
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % #3----->#4
+\enddiagram%% % #7
+}}
+
+\def\putAtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+{\multiply \height by2
+\puthmorphism(\xpos,\ypos)[#5`#6`{#9}]{\height}{\arrowtypec}b}%
+\advance\xpos by\height \advance\ypos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[#4``{#7}]{\height}{\arrowtypea}l%
+\putmorphism(\xpos,\ypos)(1,-1)[``{#8}]{\height}{\arrowtypeb}r%
+}}
+
+\def\putAtriangle{\@ifnextchar <{\putAtrianglep}{\putAtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\Atriangle{\@ifnextchar <{\Atrianglep}{\Atrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #2
+\def\Atrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % / \
+\settriparms[#1]% % / \
+\width=\height % #5/ \#6
+\diagram% % / \
+\putAtrianglep<\arrowtypea`\arrowtypeb`% % / \
+\arrowtypec;\height>% % v v
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % #3------------>#4
+\enddiagram%% % #7
+}}
+
+\def\putAtrianglepairp<#1>(#2)[#3;#4`#5`#6`#7`#8]{{%
+\settripairparms[#1]%
+\setpos(#2)%
+\settokens`#3`%
+\puthmorphism(\xpos,\ypos)[\tokenb`\tokenc`{#7}]{\height}{\arrowtyped}b%
+\advance\xpos by\height
+\puthmorphism(\xpos,\ypos)[\phantom{\tokenc}`\tokend`{#8}]%
+{\height}{\arrowtypee}b%
+\advance\ypos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[\tokena``{#4}]{\height}{\arrowtypea}l%
+\putvmorphism(\xpos,\ypos)[``{#5}]{\height}{\arrowtypeb}m%
+\putmorphism(\xpos,\ypos)(1,-1)[``{#6}]{\height}{\arrowtypec}r%
+}}
+
+\def\putAtrianglepair{\@ifnextchar <{\putAtrianglepairp}{\putAtrianglepairp%
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped`\arrowtypee;\height>}}
+\def\Atrianglepair{\@ifnextchar <{\Atrianglepairp}{\Atrianglepairp%
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped`\arrowtypee;\height>}}
+
+\def\Atrianglepairp<#1>[#2;#3`#4`#5`#6`#7]{{% % #2a
+\settripairparms[#1]% % / | \
+\settokens`#2`% % / | \
+\width=\height % #3/ #4 \#5
+\diagram% % / | \
+\putAtrianglepairp % / | \
+<\arrowtypea`\arrowtypeb`\arrowtypec`% % v v v
+\arrowtyped`\arrowtypee;\height>% % #2b---->#2c---->#2d
+(0,0)[{#2};#3`#4`#5`#6`{#7}]% % #6 #7
+\enddiagram%%
+}}
+
+\def\putVtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\advance\ypos by\height
+{\multiply\height by2
+\puthmorphism(\xpos,\ypos)[#4`#5`{#7}]{\height}{\arrowtypea}a}%
+\putmorphism(\xpos,\ypos)(1,-1)[`#6`{#8}]{\height}{\arrowtypeb}l%
+\advance\xpos by\height
+\advance\xpos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[``{#9}]{\height}{\arrowtypec}r%
+}}
+
+\def\putVtriangle{\@ifnextchar <{\putVtrianglep}{\putVtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\Vtriangle{\@ifnextchar <{\Vtrianglep}{\Vtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #5
+\def\Vtrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % #2------------->#3
+\settriparms[#1]% % \ /
+\width=\height % \ /
+\diagram% % #6\ /#7
+\putVtrianglep<\arrowtypea`\arrowtypeb`% % \ /
+\arrowtypec;\height>% % \ /
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % v v
+\enddiagram%% % #4
+}}
+
+\def\putVtrianglepairp<#1>(#2)[#3;#4`#5`#6`#7`#8]{{
+\settripairparms[#1]%
+\setpos(#2)%
+\settokens`#3`%
+\advance\ypos by\height
+\putmorphism(\xpos,\ypos)(1,-1)[`\tokend`{#6}]{\height}{\arrowtypec}l%
+\puthmorphism(\xpos,\ypos)[\tokena`\tokenb`{#4}]{\height}{\arrowtypea}a%
+\advance\xpos by\height
+\puthmorphism(\xpos,\ypos)[\phantom{\tokenb}`\tokenc`{#5}]%
+{\height}{\arrowtypeb}a%
+\putvmorphism(\xpos,\ypos)[``{#7}]{\height}{\arrowtyped}m%
+\advance\xpos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[``{#8}]{\height}{\arrowtypee}r%
+}}
+
+\def\putVtrianglepair{\@ifnextchar <{\putVtrianglepairp}{\putVtrianglepairp%
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped`\arrowtypee;\height>}}
+\def\Vtrianglepair{\@ifnextchar <{\Vtrianglepairp}{\Vtrianglepairp%
+ <\arrowtypea`\arrowtypeb`\arrowtypec`\arrowtyped`\arrowtypee;\height>}}
+ % #3 #4
+\def\Vtrianglepairp<#1>[#2;#3`#4`#5`#6`#7]{{% % #2a---->#2b---->#2c
+\settripairparms[#1]% % \ | /
+\settokens`#2`% % \ | /
+\diagram% % #5\ #6 /#7
+\putVtrianglepairp % \ | /
+<\arrowtypea`\arrowtypeb`\arrowtypec`% % \ | /
+\arrowtyped`\arrowtypee;\height>% % v v v
+(0,0)[{#2};#3`#4`#5`#6`{#7}]% % #2d
+\enddiagram%%
+}}
+
+
+\def\putCtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\advance\ypos by\height
+\putmorphism(\xpos,\ypos)(1,-1)[``{#9}]{\height}{\arrowtypec}l%
+\advance\xpos by\height
+\advance\ypos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[#4`#5`{#7}]{\height}{\arrowtypea}l%
+{\multiply\height by 2
+\putvmorphism(\xpos,\ypos)[`#6`{#8}]{\height}{\arrowtypeb}r}%
+}}
+
+\def\putCtriangle{\@ifnextchar <{\putCtrianglep}{\putCtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\Ctriangle{\@ifnextchar <{\Ctrianglep}{\Ctrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #2
+\def\Ctrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % / |
+\settriparms[#1]% % #5/ |
+\width=\height % / |
+\diagram% % v |
+\putCtrianglep<\arrowtypea`\arrowtypeb`% % #3 |#6
+\arrowtypec;\height>% % \ |
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % #7\ |
+\enddiagram%% % \ |
+}} % v v
+ % #4
+\def\putDtrianglep<#1>(#2,#3)[#4`#5`#6;#7`#8`#9]{{%
+\settriparms[#1]%
+\xpos=#2 \ypos=#3
+\advance\xpos by\height \advance\ypos by\height
+\putmorphism(\xpos,\ypos)(-1,-1)[``{#9}]{\height}{\arrowtypec}r%
+\advance\xpos by-\height \advance\ypos by\height
+\putmorphism(\xpos,\ypos)(1,-1)[`#5`{#8}]{\height}{\arrowtypeb}r%
+{\multiply\height by 2
+\putvmorphism(\xpos,\ypos)[#4`#6`{#7}]{\height}{\arrowtypea}l}%
+}}
+
+\def\putDtriangle{\@ifnextchar <{\putDtrianglep}{\putDtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+\def\Dtriangle{\@ifnextchar <{\Dtrianglep}{\Dtrianglep
+ <\arrowtypea`\arrowtypeb`\arrowtypec;\height>}}
+ % #2
+\def\Dtrianglep<#1>[#2`#3`#4;#5`#6`#7]{{%% % | \
+\settriparms[#1]% % | \#6
+\width=\height % | \
+\diagram% % | v
+\putDtrianglep<\arrowtypea`\arrowtypeb`% % #5| #3
+\arrowtypec;\height>% % | /
+(0,0)[#2`#3`#4;#5`#6`{#7}]% % | /#7
+\enddiagram%% % | /
+}} % v v
+ % #4
+\def\setrecparms[#1`#2]{\width=#1 \height=#2}%
+% #4
+% #3b<-------#3a x #3b
+% ^ | |
+% / | |
+% #5/ | |
+% / | |
+% / | |
+% / | |
+% #3c |#6 |#3a x #5
+% \ | |
+% \ | |
+% #8\ | |
+% \ | |
+% \ | |
+% v v v
+% #3d<-------#3a x #3d
+% #8
+
+\def\recursep<#1`#2>[#3;#4`#5`#6`#7`#8]{{\m@th
+\width=#1 \height=#2
+\settokens`#3`
+\settowidth{\tempdimen}{$\tokena$}
+\ifdim\tempdimen=0pt
+ \savebox{\tempboxa}{\hbox{$\tokenb$}}%
+ \savebox{\tempboxb}{\hbox{$\tokend$}}%
+ \savebox{\tempboxc}{\hbox{$#6$}}%
+\else
+ \savebox{\tempboxa}{\hbox{$\hbox{$\tokena$}\times\hbox{$\tokenb$}$}}%
+ \savebox{\tempboxb}{\hbox{$\hbox{$\tokena$}\times\hbox{$\tokend$}$}}%
+ \savebox{\tempboxc}{\hbox{$\hbox{$\tokena$}\times\hbox{$#6$}$}}%
+\fi
+\ypos=\height
+\divide\ypos by 2
+\xpos=\ypos
+\advance\xpos by \width
+\bfig
+\putCtrianglep<-1`1`1;\ypos>(0,0)[`\tokenc`;#5`#6`{#7}]%
+\puthmorphism(\ypos,0)[\tokend`\usebox{\tempboxb}`{#8}]{\width}{-1}b%
+\puthmorphism(\ypos,\height)[\tokenb`\usebox{\tempboxa}`{#4}]{\width}{-1}a%
+\advance\ypos by \width
+\putvmorphism(\ypos,\height)[``\usebox{\tempboxc}]{\height}1r%
+\efig
+}}
+
+\def\recurse{\@ifnextchar <{\recursep}{\recursep<\width`\height>}}
+
+\def\puttwohmorphisms(#1,#2)[#3`#4;#5`#6]#7#8#9{{%
+% 1 and 2 are position, 3 and 4 are the nodes, 5 and 6 the labels,
+% 7 the distance between node centers and 8 & 9 are the arrow types.
+% #5
+% #3 ===========> #4
+% #6
+%
+\puthmorphism(#1,#2)[#3`#4`]{#7}0a
+\ypos=#2
+\advance\ypos by 20
+\puthmorphism(#1,\ypos)[\phantom{#3}`\phantom{#4}`#5]{#7}{#8}a
+\advance\ypos by -40
+\puthmorphism(#1,\ypos)[\phantom{#3}`\phantom{#4}`#6]{#7}{#9}b
+}}
+
+\def\puttwovmorphisms(#1,#2)[#3`#4;#5`#6]#7#8#9{{%
+% 1 and 2 are position, 3 and 4 are the nodes, 5 and 6 the labels,
+% 7 the distance between node centers and 8 & 9 are the arrow types.
+%
+% #3
+% ||
+% ||
+% #5 || #6
+% ||
+% ||
+% vv
+% #4
+%
+\putvmorphism(#1,#2)[#3`#4`]{#7}0a
+\xpos=#1
+\advance\xpos by -20
+\putvmorphism(\xpos,#2)[\phantom{#3}`\phantom{#4}`#5]{#7}{#8}l
+\advance\xpos by 40
+\putvmorphism(\xpos,#2)[\phantom{#3}`\phantom{#4}`#6]{#7}{#9}r
+}}
+
+\def\puthcoequalizer(#1)[#2`#3`#4;#5`#6`#7]#8#9{{%
+% #1 is (\xpos,\ypos), the next 6 are the nodes and arrow labels
+% #8 is the distance between each pair of nodes and #9 is the pos of #7
+% either a (above) or b (below)
+% #5 #7
+% #2 ===========> #3 --------> #4
+% #6
+%
+\setpos(#1)%
+\puttwohmorphisms(\xpos,\ypos)[#2`#3;#5`#6]{#8}11%
+\advance\xpos by #8
+\puthmorphism(\xpos,\ypos)[\phantom{#3}`#4`#7]{#8}1{#9}
+}}
+
+\def\putvcoequalizer(#1)[#2`#3`#4;#5`#6`#7]#8#9{{%
+% #1 is (\xpos,\ypos), the next 6 are the nodes and arrow labels
+% #8 is the distance between each pair of nodes and #9 is the pos of #7
+% either l (left) or r (right)
+%
+% #2
+% | |
+% | |
+% #5 | | #6
+% | |
+% | |
+% v v
+% #3
+% |
+% |
+% #7 |
+% |
+% v
+% #4
+%
+\setpos(#1)%
+\puttwovmorphisms(\xpos,\ypos)[#2`#3;#5`#6]{#8}11%
+\advance\ypos by -#8
+\putvmorphism(\xpos,\ypos)[\phantom{#3}`#4`#7]{#8}1{#9}
+}}
+
+\def\putthreehmorphisms(#1)[#2`#3;#4`#5`#6]#7(#8)#9{{%
+% Use: \putthreehmorphisms(xpos,ypos)[lnode`rnode;toplabel`midlabel%
+% botlabel]{distance}(toparrowtype,midarrowtype,botarrowtype){position}
+\setpos(#1) \settypes(#8)
+\if a#9 %
+ \vertsize{\tempcounta}{#5}%
+ \vertsize{\tempcountb}{#6}%
+ \ifnum \tempcounta<\tempcountb \tempcounta=\tempcountb \fi
+\else
+ \vertsize{\tempcounta}{#4}%
+ \vertsize{\tempcountb}{#5}%
+ \ifnum \tempcounta<\tempcountb \tempcounta=\tempcountb \fi
+\fi
+\advance \tempcounta by 60
+\puthmorphism(\xpos,\ypos)[#2`#3`#5]{#7}{\arrowtypeb}{#9}
+\advance\ypos by \tempcounta
+\puthmorphism(\xpos,\ypos)[\phantom{#2}`\phantom{#3}`#4]{#7}{\arrowtypea}{#9}
+\advance\ypos by -\tempcounta \advance\ypos by -\tempcounta
+\puthmorphism(\xpos,\ypos)[\phantom{#2}`\phantom{#3}`#6]{#7}{\arrowtypec}{#9}
+}}
+
+\def\setarrowtoks[#1`#2`#3`#4`#5`#6]{%
+\def\toka{#1}
+\def\tokb{#2}
+\def\tokc{#3}
+\def\tokd{#4}
+\def\toke{#5}
+\def\tokf{#6}
+}
+\def\hex{\@ifnextchar <{\hexp}{\hexp<1000`400>}}
+\def\hexp<#1`#2>[#3`#4`#5`#6`#7`#8;#9]{%
+\setarrowtoks[#9]
+\yext=#2 \advance \yext by #2
+\xext=#1 \advance\xext by \yext
+\bfig
+\putCtriangle<-1`0`1;#2>(0,0)[`#5`;\tokb``\tokd]
+\xext=#1 \yext=#2 \advance \yext by #2
+\putsquare<1`0`0`1;\xext`\yext>(#2,0)[#3`#4`#7`#8;\toka```\tokf]
+\advance \xext by #2
+\putDtriangle<0`1`-1;#2>(\xext,0)[`#6`;`\tokc`\toke]
+\efig
+}
+%\def\doublecomplex[#1`#2`#3`#4`#5`#6`#7`#8`#9]{%
+%\bfig
+%\putsquare<0`0`1`1;500`500>(0,1700)[`\vdots`\cdots`{#1};```]
+%\puthmorphism(500,1700)[\ph{#1}`\cdots`]{500}1a
+%\puthmorphism(1000,1700)[\ph{\cdots}`\ph{#2}`]{500}1a
+%\putsquare<0`1`1`1;700`500>(1500,1700)[\vdots`\vdots`{#2}`{#3};```]
+%\puthmorphism(2200,1700)[\ph{#3}`0`]{500}1a
+%\putvmorphism(500,1700)[`\vdots`]{400}1a \putvmorphism(500,1300)[``]{400}1a
+%\putvmorphism(1500,1700)[`\vdots`]{400}1a \putvmorphism(1500,1300)[``]{400}1a
+%\putvmorphism(2200,1700)[`\vdots`]{400}1a \putvmorphism(2200,1300)[``]{400}1a
+%\putsquare<1`0`1`1;500`500>(0,400)[\cdots`{#4}`\cdots`{#7};```]
+%\puthmorphism(500,900)[\ph{#1}`\cdots`]{500}1a
+%\puthmorphism(1000,900)[\ph{\cdots}`\ph{#2}`]{500}1a
+%\puthmorphism(500,400)[\ph{#1}`\cdots`]{500}1a
+%\puthmorphism(1000,400)[\ph{\cdots}`\ph{#2}`]{500}1a
+%\putsquare<1`1`1`1;700`500>(1500,400)[{#5}`{#6}`{#8}`{#9};```]
+%\puthmorphism(2200,900)[\ph{#6}`0`]{500}1a
+%\puthmorphism(2200,400)[\ph{#9}`0`]{500}1a
+%\putvmorphism(500,400)[`0`]{400}1a
+%\putvmorphism(1500,400)[`0`]{400}1a
+%\putvmorphism(2200,400)[`0`]{400}1a
+%\efig
+%}
+%
+%\def\doublecocomplex[#1`#2`#3`#4`#5`#6`#7`#8`#9]{%
+%\bfig
+%\putsquare<0`0`-1`-1;500`500>(0,1700)[`\vdots`\cdots`{#1};```]
+%\puthmorphism(500,1700)[\ph{#1}`\cdots`]{500}{-1}a
+%\puthmorphism(1000,1700)[\ph{\cdots}`\ph{#2}`]{500}{-1}a
+%\putsquare<0`-1`-1`-1;500`500>(1500,1700)[\vdots`\vdots`{#2}`{#3};```]
+%\puthmorphism(2000,1700)[\ph{#3}`0`]{500}{-1}a
+%\putvmorphism(500,1700)[`\vdots`]{400}{-1}a \putvmorphism(500,1300)[``]{400}{-1}a
+%\putvmorphism(1500,1700)[`\vdots`]{400}{-1}a \putvmorphism(1500,1300)[``]{400}{-1}a
+%\putvmorphism(2000,1700)[`\vdots`]{400}{-1}a \putvmorphism(2000,1300)[``]{400}{-1}a
+%\putsquare<-1`0`-1`-1;500`500>(0,400)[\cdots`{#4}`\cdots`{#7};```]
+%\puthmorphism(500,900)[\ph{#1}`\cdots`]{500}{-1}a
+%\puthmorphism(1000,900)[\ph{\cdots}`\ph{#2}`]{500}{-1}a
+%\puthmorphism(500,400)[\ph{#1}`\cdots`]{500}{-1}a
+%\puthmorphism(1000,400)[\ph{\cdots}`\ph{#2}`]{500}{-1}a
+%\putsquare<-1`-1`-1`-1;500`500>(1500,400)[{#5}`{#6}`{#8}`{#9};```]
+%\puthmorphism(2000,900)[\ph{#6}`0`]{500}{-1}a
+%\puthmorphism(2000,400)[\ph{#9}`0`]{500}{-1}a
+%\putvmorphism(500,400)[`0`]{400}{-1}a
+%\putvmorphism(1500,400)[`0`]{400}{-1}a
+%\putvmorphism(2000,400)[`0`]{400}{-1}a
+%\efig
+%}
+\makeatother
diff --git a/obsolete/macros/generic/proofs/taylor/boxproof-old.tex b/obsolete/macros/generic/proofs/taylor/boxproof-old.tex
new file mode 100644
index 0000000000..e42924bb08
--- /dev/null
+++ b/obsolete/macros/generic/proofs/taylor/boxproof-old.tex
@@ -0,0 +1,142 @@
+% mangletex (11 May 1992) run at 19:39 BST Monday 29 June 1992
+\message{<Paul Taylor's Proof Boxes, 29 June 1992>}%%
+%%=======================================================
+%% There is now a PROTOTYPE proof-box macro mackage for TRIAL only.
+%% The syntax and implementation may change.
+%% It is "boxproof.tex" in the TeX system (so just "\input boxproof").
+%% There are some examples in ~pt/utilities/misctex/proofboxeg.tex and
+%% proofboxeg1.tex.
+%%
+%% Syntax as follows:
+%% each line is of the form
+%% <all/exists_variables> <latex_label> \: <formula> \= <reason> \\
+%% where
+%% <all/exists_variables> is something like "x,y" - its for variables
+%% declared at the beginning of all-intro and exists-elim boxes
+%% <latex_label> is a command "\label{fred}" which defines "fred" to
+%% be the label text, which may be used anywhere as "\ref{fred}"
+%% - see LaTeX book.
+%% <formula> is the proposition being asserted
+%% <reason> is "\intro\land(\ref{john},\ref{mary})"
+%%% note that the parts are separated by "\:", "\=" and "\\"; these correspond
+%% to "let identifier = expression : type" in a declarative language.
+%%
+%% Proof boxes are "wrapped up" as follows:
+%% the whole proof in "\begin{proofbox}...\end{proofbox}"
+%% single-column boxes (all-intro, implies-intro, exists-elim) in "\[...\]"
+%% double-column boxes are of two kinds:
+%% separate (and-intro) "\(...\*...\)"
+%% stuck together (or-elim) "\(...\+...\)"
+%%
+%%% At the moment you may only have pairs of parallel boxes, and the width is
+%%% split in two; later there will be options for mutiple boxes and adjustable
+%% widths.
+%%
+%% Comments please.
+%%
+%% WARNING: this is for temporary use only at the moment.
+%%=======================================================
+\catcode`\@=11 \let\plaint@bplus\+\let\+\relax\newcount\prooflineinbox
+\newcount\prooflineinnextbox\newcount\prooflinetotal\newcount\pr@@flinetotal
+\newcount\pr@@flinemax\newcount\proofboxesacross\newdimen\prooflinenowidth
+\newdimen\proofboxformulawidth\newdimen\proofboxrulebreadth\newdimen
+\proofboxrulespace\newdimen\proofboxsurround\newdimen\proofboxmargin\newdimen
+\pr@@fboxhadjust\newdimen\proofboxintercol\newif\ifinproofbox\newif
+\ifleftmostproofbox\newif\ifparallelisand\newskip\proofboxlefttabskip\newskip
+\proofboxrighttabskip\newskip\proofboxbaselineskip\def\runningproofline{%
+\number\prooflinetotal}\def\nestedproofline{\ifinproofbox\enclosingproofline.%
+\fi\number\prooflineinbox}\def\enclosingproofline{}\prooflinenowidth=1em
+\proofboxformulawidth=15em \proofboxrulebreadth=.03em \proofboxrulespace=.2em
+\proofboxsurround=.5em \proofboxlefttabskip=1em \proofboxrighttabskip=1em plus
+1 fil \proofboxbaselineskip=1.8em \proofboxmargin=5em \proofboxintercol=3em
+\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}%
+\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@
+\hfill}\let\theproofline\runningproofline\def\proofboxmakelabel#1{{%
+\ifleftmostproofbox\setbox0=\hbox{\hss\the\scriptfont1 #1}\ifdim\wd0<%
+\prooflinenowidth\setbox0=\hbox to\prooflinenowidth{\unhbox0}\fi\box0 \fi}}%
+\def\proofboxnonumbers{\def\proofboxmakelabel##1{}} \def\proofbox{\global
+\prooflinetotal=0 \ifvmode\else\vtop\fi\bgroup\let\[\intofullpr@@fbox\let\(%
+\intohalfpr@@fbox\let\:\pr@@fboxcolon\let\=\pr@@fboxequals\let\proofbox
+\intofullpr@@fbox\proofboxesacross=1 \pr@@fb@x}\let\pr@@fb@x\csname\let
+\endpr@@fb@x\endcsname\def\endproofbox{\endpr@@fb@x\proofboxmargin\z@\vskip1%
+ex \unvbox9 \vskip1ex \egroup}\def\intofullpr@@fbox{\pr@@ffirst\pr@@fb@x}\def
+\+#1{<"7C#1}\def\outofpr@@fbox{\endpr@@fb@x\z@\z@\endpr@@ffirst
+\proofboxleftside\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f
+\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\intohalfpr@@fbox{%
+\pr@@ffirst\advance\proofboxformulawidth-\proofboxintercol\advance
+\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \pr@@fb@x
+}\def\pr@@fvalign{m}\def\orpr@@ffirst{\endpr@@fb@x\z@{.5\proofboxintercol}%
+\endpr@@ffirst\proofboxleftside\advance\proofboxformulawidth-%
+\proofboxintercol\advance\proofboxformulawidth-\proofboxsurround\divide
+\proofboxformulawidth2 \let\*\orpr@@fmore\let\+\orpr@@fmore\let\]\orpr@@flast
+\let\)\orpr@@flast\let\endproof\orpr@@flast\pr@@fvalign\putpr@@fedge
+\proofboxleftside\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def
+\putpr@@forsep{o}\def\orpr@@fmore{\endpr@@fb@x{.5\proofboxintercol}{.5%
+\proofboxintercol}\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def
+\putpr@@fedge{n}\def\orpr@@flast{\endpr@@fb@x{.5\proofboxintercol}\z@
+\putpr@@f\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\putpr@@f{t}\def
+\endpr@@fvalign{h}\def\andpr@@ffirst{\endpr@@fb@x\z@\z@\endpr@@ffirst
+\proofboxleftside\advance\proofboxformulawidth-\proofboxintercol\advance
+\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \let\*%
+\andpr@@fmore\let\+\andpr@@fmore\let\]\andpr@@flast\let\)\andpr@@flast\let
+\endproof\andpr@@flast\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f
+\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=\proofboxintercol\advance
+\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2\dimen2 \pr@@fb@x}\def
+\la@math{a}\def\andpr@@fmore{\endpr@@fb@x\z@\z@\hadjustandpr@@f\putpr@@fedge
+\proofboxleftside\putpr@@f\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=%
+\proofboxintercol\advance\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2%
+\dimen2 \pr@@fb@x}\def\la@ket{r}\def\andpr@@flast{\endpr@@fb@x\z@\z@
+\hadjustandpr@@f\putpr@@fedge\proofboxleftside\putpr@@f\putpr@@fedge
+\proofboxrightside\endpr@@fvalign}\def\hadjustandpr@@f{\advance
+\pr@@fboxhadjust-\dimen6 \ifdim\pr@@fboxhadjust<\proofboxsurround
+\pr@@fboxhadjust=\proofboxsurround\fi\hrule width\pr@@fboxhadjust height\z@
+depth\z@\cr}\def\pr@@fboxcr{\cr}\def\pr@@fboxequals{&}\def\pr@@fboxcolon{&}%
+\ifnum\pr@@fb@x\pr@@fvalign\putpr@@forsep\putpr@@fedge\putpr@@f
+\endpr@@fvalign\endpr@@fb@x<13\let\pr@@fmtb\relax\else\def\pr@@fmtb#1{}\fi
+\def\pr@@ffirst{\omit\prooflineinnextbox=\prooflineinbox\edef
+\enclosingproofline{\theproofline}%% its line label
+\pr@@flinetotal=\prooflinetotal\let\endproofbox\outofpr@@fbox
+\proofboxesacross=1 \let\+\orpr@@ffirst\let\*\andpr@@ffirst\let\)%
+\outofpr@@fbox\let\]\outofpr@@fbox\inproofboxtrue}\def\la@bra{y}\def
+\endpr@@ffirst#1{\setbox0=\vbox{#1}\global\advance\dimen6\wd0 \advance\dimen6%
+\proofboxsurround\hskip\dimen6 plus 1fil \global\count@=\pr@@flinetotal&\omit
+\setbox8=\hbox\bgroup\pr@@flinetotal=\count@\hskip-\dimen6 \pr@@flinemax=%
+\prooflinetotal\global\prooflinetotal=\pr@@flinetotal\leftmostproofboxfalse
+\inproofboxtrue}\def\pr@@fvalign{\valign\bgroup\vfil##&##&##\vfil&##&##\vfil
+\cr}\def\endpr@@fvalign{\vfil&\vfil&\vfil&\vfil&\vfil\cr\egroup\setbox0=%
+\lastbox\setbox0=\vbox{\unvbox0\unskip\setbox5=\lastbox\unskip\setbox4=%
+\lastbox\unskip\setbox3=\lastbox\unskip\setbox2=\lastbox\unskip\setbox1=%
+\lastbox\global\dimen9=\ht5 \global\advance\dimen9\dp5\global\advance\dimen9%
+\ht4\global\advance\dimen9\dp4\global\dimen4=\ht1 \global\advance\dimen4\dp1%
+\global\advance\dimen4\ht2\global\advance\dimen4\dp1}\global\advance\dimen8%
+\dimen2\kern-\dimen8 \global\prooflinetotal=\pr@@flinemax\egroup\dimen0=\dp8
+\advance\dimen0-\dimen4 \vtop{\setbox0=\null\ht0=\dimen4 \dp0=-\dimen4 \box0%
+\nointerlineskip\box8}\ifdim\dimen0<\z@\dimen0\z@\fi\advance\dimen0-\dimen9
+\vadjust{\vskip-\dimen0}&\omit\global\advance\dimen8\proofboxsurround\hskip
+\dimen8 plus 1 fil \cr}\def\putpr@@fedge#1{\span\omit\span\omit\span\omit
+\span\omit\setbox0=\vbox{#1}\global\dimen2=\wd0 \unvbox0\vfil\cr}\def
+\la@displ{e}\def\putpr@@forsep#1{&\multispan3 \setbox0=\vbox{#1}\global\dimen
+2=\wd0 \unvbox0 &\vfil\cr\noalign{\kern-\dimen2}}\def\putpr@@f{\hbox to\dimen
+5{\proofboxtopside}&\advance\dimen4\proofboxrulespace\vskip\dimen4 plus 1fil&%
+\vskip-\dimen4 \unvbox9 \vskip-\dimen9&\advance\dimen9\proofboxrulespace
+\vskip\dimen9 plus 1 fil&\hbox to\dimen5{\proofboxbottomside}\cr}\ifnum
+\pr@@fb@x\la@bra\la@displ\la@math\la@ket\endpr@@fb@x\+A\let\pr@@fytb\relax
+\else\def\pr@@fytb#1{}\fi\def\pr@@fb@x{\global\setbox9=\vtop\bgroup
+\nointerlineskip\global\prooflineinbox=0 \baselineskip=\proofboxbaselineskip
+\tabskip=\z@\let\\\pr@@fboxcr\halign\bgroup\hskip\proofboxrulespace plus 1fil%
+\let\(\la@math\let\[\la@displ\global\advance\prooflineinbox1 \global\advance
+\prooflinetotal1 \edef\@currentlabel{\theproofline}$##\proofboxmakelabel
+\@currentlabel$&\hskip\proofboxlefttabskip\let\(\la@math\let\[\la@displ$%
+\displaystyle##$\hskip\proofboxrighttabskip&\let\(\la@math\let\[\la@displ$##$%
+\hskip\proofboxrulespace plus1fil \cr}\def\endpr@@fb@x#1#2{\crcr\omit\hskip#1
+plus 1 fil&\omit\hskip\proofboxformulawidth plus 1fil&\omit\hskip#2 plus 1fil%
+\cr\egroup\setbox0=\lastbox\unskip\global\dimen5=\wd0 \setbox0=\hbox{\unhbox0%
+\unskip\setbox0=\lastbox\global\dimen8=\wd0\unskip\setbox0=\lastbox\global
+\dimen7=\wd0\unskip\setbox0=\lastbox\global\dimen6=\wd0\unskip}\setbox0=%
+\lastbox\global\dimen9=\dp0 \nointerlineskip\pr@@fytb{\box0}\egroup\global
+\dimen4=\ht9 }\inproofboxfalse\leftmostproofboxtrue\let\la@bra\(\let\la@ket\)%
+\def\la@math{\la@bra\let\)\la@ket}\def\la@displ{\la@bra\displaystyle\let\]%
+\la@ket}\let\+\plaint@bplus\catcode`\@=12 \ No newline at end of file
diff --git a/obsolete/macros/generic/proofs/taylor/boxproof.tex b/obsolete/macros/generic/proofs/taylor/boxproof.tex
new file mode 100644
index 0000000000..d95d0a58c1
--- /dev/null
+++ b/obsolete/macros/generic/proofs/taylor/boxproof.tex
@@ -0,0 +1,424 @@
+% mangletex (11 May 1992) run at 22:09 GMT Monday 08 November 1993
+%%\title {\TeX\ macros for proof boxes}
+%%\author {Paul Taylor\\
+%% Department of Computing,\\
+%% Imperial College,\\
+%% London SW7 2BZ\\
+%% +44 71 589 5111 {\em ext.} 5057\\
+%% {\tt<pt@doc.ic.ac.uk>}}
+%%\date{8 November 1993}
+%% % to get the provisional user documentation do
+%% % grep ^%% boxproof.tex | sed 's/^%*//' > boxproof-manual.tex
+%%\documentstyle{article}
+%%\input boxproof.tex
+%%\def\meta#1{\mbox{$\langle\hbox{#1}\rangle$}}
+%%\def\macrowitharg#1#2{{\tt\string#1\bra\meta{#2}\ket}}
+%%{\escapechar-1 \xdef\bra{\string\{}\xdef\ket{\string\}}}
+%%\let\subsection\section
+%%\begin{document}
+%%\maketitle
+%%
+%% \subsection{Introduction}
+%% The proof
+%%\begin{proofbox}
+%% \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\=\\
+%% \:\Some\beta.\psi(x,\beta)\=\mathsf{total}\\
+%% \[\exists\beta\kern-1em\:\psi(x,\beta)\\
+%% \(\:\beta\=\\
+%% \:\beta=\top\=(*)\\
+%% \:\psi(x,\!\top)\=\mathsf{subs}\\
+%% \:\alpha\=\elim\leftrightarrow(\ref{1})\\
+%% \*\:\alpha\=\\
+%% \:\psi(x,\!\top)\=\elim\leftrightarrow(\ref{1})\\
+%% \:\beta=\top\=\mathsf{func}\\
+%% \:\beta\=(*)\\
+%% \)\:\alpha=\beta\=\intro\leftrightarrow\\
+%% \:\psi(x,\alpha)\=\mathsf{subs}\\
+%% \] \:\psi(x,\alpha)\=\elim\exists\\
+%% \* \:\psi(x,\alpha)\=\\
+%% \(\:\alpha\=\\
+%% \:\alpha=\top\=(*)\\
+%% \:\phi(x,\!\top)\=\mathsf{subs}\\
+%% \*\:\psi(x,\!\top)\=\\
+%% \:\alpha=\top\=\mathsf{func}\\
+%% \:\alpha\=(*)\\
+%% \)\:\alpha\leftrightarrow\psi(x,\!\top)\=\intro\leftrightarrow\\
+%%% \) \:\psi(x,\alpha)\leftrightarrow(\alpha\leftrightarrow\psi(x,\!\top))
+%% \=\intro\leftrightarrow\\
+%%\end{proofbox}
+%% is produced by
+%%\begin{verbatim}
+%%\begin{proofbox}
+%% \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\\
+%% \:\Some\beta.\psi(x,\beta) \=\mathsf{total}\\
+%% \[\exists\beta\kern-1em\:\psi(x,\beta)\\
+%% \(\:\beta\\
+%% \:\beta=\top \=(*)\\
+%% \:\psi(x,\!\top) \=\mathsf{subs}\\
+%% \:\alpha \=\elim\leftrightarrow(\ref{1})\\
+%% \*\:\alpha\\
+%% \:\psi(x,\!\top) \=\elim\leftrightarrow(\ref{1})\\
+%% \:\beta=\top \=\mathsf{func}\\
+%% \:\beta\=(*)\\
+%% \)\:\alpha=\beta \=\intro\leftrightarrow\\
+%% \:\psi(x,\alpha) \=\mathsf{subs}\\
+%% \] \:\psi(x,\alpha) \=\elim\exists\\
+%% \* \:\psi(x,\alpha)\\
+%% \(\:\alpha\\
+%% \:\alpha=\top \=(*)\\
+%% \:\phi(x,\!\top) \=\mathsf{subs}\\
+%% \*\:\psi(x,\!\top)\\
+%% \:\alpha=\top \=\mathsf{func}\\
+%% \:\alpha \=(*)\\
+%% \)\:\alpha\leftrightarrow\psi(x,\!\top) \=\intro\leftrightarrow\\
+%% \) \:\psi(x,\alpha)\leftrightarrow
+%% (\alpha\leftrightarrow\psi(x,\!\top)) \=\intro\leftrightarrow\\
+%%\end{proofbox}
+%%\end{verbatim}
+%%
+%% Syntax as follows:
+%% each line is of the form
+%% \begin{center}
+%% \meta{variables}
+%% \meta{name}
+%% \verb/\:/ \meta{formula}
+%% \verb/\=/ \meta{reason}
+%% \verb/\-/ \meta{use}
+%% \verb/\\/
+%% \end{center}
+%% where
+%% \begin{itemize}
+%% \item \meta{variables} is something like ``$x,y$'' ---
+%% it's for variables declared at the beginning of $\intro\forall$- and
+%% $\elim\exists$-boxes.
+%% \item \meta{name} is a command \verb/\label{fred}/ which
+%% defines \verb/fred/ to be the label text, which may be used anywhere
+%% as \verb/\ref{fred}/ --- see {\em The \LaTeX book.}
+%% Local labels are also available, using \macrowitharg\lbl{name}
+%% or \verb/\"/\meta{name}\verb/"/; these obey the scoping rules of
+%% the boxes.
+%% You may also refer to the previous line as \verb/\ref{-}/.
+%% \item \meta{formula} is the proposition being asserted.
+%% \item \meta{reason} is \verb/\intro\land(\ref{john},\ref{mary})/
+%% or \verb/\elim\forall(\ref{jim})/.
+%% \item \meta{use} is provided for linear logic, to record the step
+%%% which uses this one. How this accords with theory I don't yet know.
+%% \end{itemize}
+%% Note that the parts are separated by \verb/\:/, \verb/\=/ and \verb/\\/;
+%% these correspond to
+%% \begin{center}
+%% {\bf let } \meta{name} = \meta{expression} : \meta{type}
+%% \end{center}
+%% in a declarative language.
+%% The \verb/\:/, \verb/\=/ and \verb/\-/ fields are optional and may occur
+%% in any order. If any of them is repeated the last is taken.
+%% If none of them is present the \meta{variables} field is also ignored.
+%%
+%% Proof {\em boxes\/} are ``wrapped up'' as follows:
+%% \begin{itemize}
+%%% \item the whole proof in \verb/\begin{proofbox}/...\verb/\end{proofbox}/;
+%%% \item single-column boxes ($\intro\forall$, $\intro\imp$, $\elim\exists$),
+%% in \verb/\[/...\verb/\]/.
+%% \item multiple-column boxes are of two kinds:
+%% \begin{itemize}
+%%% \item separate ($\intro\land$) boxes: \verb/\(/...\verb/\*/...\verb/\)/.
+%% \item stuck together ($\elim\lor$) boxes:
+%% \verb/\(/...\verb/\+/...\verb/\)/.
+%% \end{itemize}
+%% \end{itemize}
+%% You may put more than two columns in \verb/\(/...\verb/\)/ and even mix
+%% the \verb/\+/ and \verb/\*/ separators.
+%%
+%% The whole proof is enclosed in \verb/\proofbox/...\verb/\endproofbox/
+%% or \verb/\begin{proofbox}/...\verb/\end{proofbox}/, but the \LaTeX\
+%% environment form {\em must not\/} be used for nested boxes.
+%%
+%% If the proof occurs in paragraph mode (ie in vertical or
+%% unrestricted horizontal mode) then it is set as a display, using the
+%% full width of the page. Otherwise it uses only the required width.
+%%
+%% A lot of the internals are potentially configurable, but there is not
+%% yet a user interface suitable for doing this. This will be provided
+%% in the next version.
+%%
+%% This is a {\em prototype\/} proof-box macro package;
+%% the syntax and implementation may change.
+%% It is {\tt boxproof.tex} in the \TeX\ system
+%% (so just \verb/\input boxproof/).
+%%
+%% There are some examples in
+%% \verb+~pt/utilities/proofs/proofboxeg.tex+ and
+%% \verb+proofboxeg1.tex+.
+%%
+%% The prototype version was begun on 2 August 1991, the new one on
+%% 4 June 1993.
+%%
+%%
+\message{<Paul Taylor's Proof Boxes, 8 November 1993>}\edef\proofboxrestoreat
+{\noexpand\catcode`\noexpand\@\the\catcode`\@}\catcode`\@=11
+\let\pb@A\+\let\+\relax\let\pb@B\(\let\pb@C\)\def\pb@D{\pb@B
+\let\)\pb@C}\def\pb@E{\pb@B\displaystyle\let\]\pb@C}%%
+%% The following are user-settable dimensions.
+%%
+\newdimen\prooflinenowidth\prooflinenowidth1em \newdimen\proofboxfullwidth
+\newdimen\proofboxleftmargin\proofboxleftmargin3em \newdimen
+\proofboxrightmargin\newdimen\proofboxrulebreadth\proofboxrulebreadth.4pt
+\newdimen\proofboxseparation\proofboxseparation.2em \newdimen
+\proofboxbaselineskip\proofboxbaselineskip4ex %%
+%%
+%% The following are user-accessible numbers.
+%%
+\newcount\proofcolumns\newcount\prooflinetotal\newcount\prooflineinbox%%
+%%
+%% These boxes receive the fields of the proof steps.
+%% They are used in \verb/\proofboxmakeleftcolumn/ {\em etc}.
+%%
+\newbox\proofboxproposition\newbox\proofboxreason\newbox\proofboxuse\newbox
+\proofboxvariables%%
+%% The left-most switch is used by
+%%% \verb/\proofboxmakelabel/ to suppress the label in all but the first column.
+%% On the outside it is true.
+\newif\ifleftmostproofbox\leftmostproofboxtrue%%
+%%
+%% The following are obsolete: they are only included for reverse
+%% compatibility with the prototype version.
+\newdimen\proofboxintercol\newdimen\proofboxsurround\newdimen
+\proofboxformulawidth\newdimen\proofboxmargin\newskip\proofboxlefttabskip
+\newskip\proofboxrighttabskip%%
+%%
+%% \subsection{Redefinable macros}
+%% WARNING: most of these commands will be hidden and replaced with
+%% optional arguments to \verb/\proofbox/ in a future version.
+%% Do not rely on them.
+%%
+%% We provide three different ways of numbering the lines of the proof:
+%% \begin{itemize}
+%% \item \verb/\runningproofline/: a global running sequence (default),
+%%
+\def\runningproofline{\number\prooflinetotal}%%
+%% \item \verb/\nestedproofline/: a hierarchical system with dots,
+%%
+\def\nestedproofline{\relax\ifx\enclosingproofline\empty\else
+\enclosingproofline{.}\fi\number\prooflineinbox}\def\enclosingproofline{}%%
+%% \item \verb/\nestedproofline/: a fully hierarchical system which
+%% also includes the column number
+%% (\verb/\proof@columns/) as a letter (ASCII quote plus number).
+%%
+\def\proofboxcolumn{\ifnum\proofcolumns>\z@{\count@96\advance\count@
+\proofcolumns\char\count@}\fi}\def\fullynestedproofline{\relax\ifx
+\enclosingproofline\empty\enclosingproofline\proofboxcolumn.\else
+\proofboxcolumn\fi\number\prooflineinbox}%%
+%% \end{itemize}
+%% \verb/\theproofline/ is the default.
+%%
+\let\theproofline\runningproofline%%
+%% The macro \verb/\proofboxmakelabel#1/ is used to print the line label.
+%% We only put it in the leftmost box.
+%% It is printed in small non-ranging Arabic numerals
+%% ({\the\scriptfont1 0123456789}).
+%% Right-justify it in \verb/\prooflinenowidth/ if it will fit,
+%% otherwise let it stick out on the right, {\em i.e.}~left-justify it.
+%%
+\def\proofboxmakelabel#1{{\relax\ifleftmostproofbox\setbox\z@\hbox{\hss\the
+\scriptfont\@ne#1}\ifdim\wd\z@<\prooflinenowidth\setbox\z@\hbox to%
+\prooflinenowidth{\unhbox\z@}\fi\box\z@\quad\fi}}%%
+%% Kill the numbers altogether with \verb/\proofboxnonumbers/.
+%%
+\def\proofboxnonumbers{\def\proofboxmakelabel##1{}}%%
+%% How to make the left column of the proof box:
+%% use the variables field, a space if necessary and the line label.
+%%
+\def\proofboxmakeleftcolumn{\kern\proofboxseparation\hfil\dimen@\wd
+\proofboxvariables\unhbox\proofboxvariables\ifdim\dimen@>\z@\quad\fi
+\proofboxmakelabel\@currentlabel}%%
+%% How to make the middle column of the proof box:
+%% left justify the formula field.
+%%
+\def\proofboxmakemiddlecolumn{\unhbox\proofboxproposition\hfil\quad}%%
+%% How to make the right column of the proof box:
+%% use the reason and use fields.
+%%
+\def\proofboxmakerightcolumn{\box\proofboxreason\box\proofboxuse\hfil\kern
+\proofboxseparation}%%
+%%
+%% Make the four edges of a rectangular box and the separator
+%% between \verb/\+/ columns.
+%%
+\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def
+\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}%
+\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@
+\hfill}%%
+%%
+%% Use dotted lines: \verb/\dottedproofbox/.
+%%
+\def\dottedproofbox{\def\proofboxleftside{\leaders\pb@F\vfill} \def
+\proofboxrightside{\leaders\pb@F\vfill} \def\proofboxorseparator{\leaders
+\pb@F\vfill} \def\proofboxtopside{\leaders\pb@F\hfill}\def\proofboxbottomside
+{\leaders\pb@F\hfill}%%
+}\def\pb@F{\vbox to 5pt{\vss\hbox to 5pt{\hss.\hss}\vss}}%%
+%% Leave the boxes open at the bottom: \verb/\openproofbox/
+%%
+\def\openproofbox{\def\proofboxbottomside{\hfill}} %%
+%% \subsection{Miscellaneous logical notations}
+%%
+%% Print the names of the introduction and elimination rules, for example:
+%% \begin{quote}
+%% \verb/\elim\forall/ $\elim\forall$ \qquad
+%% \verb/\intro\land/ $\intro\land$ \qquad
+%% \end{quote}
+\def\intro#1{{{#1}{\cal I}}}\def\elim#1{{{#1}{\cal E}}}%%
+%% Recall that in \TeX\ the logical connectives and quantifiers are called
+%% \begin{center}
+%% \verb/\lor/ $\lor$\quad
+%% \verb/\land/ $\land$\quad
+%% \verb/\lnot/ $\lnot$\quad
+%% \verb/\forall/ $\forall$\quad
+%% \verb/\exists/ $\exists$
+%% \end{center}
+%% The following provide macros for the \verb/\implies/ {\em relation\/}
+%% and for the binary {\em operation\/} which yields the abstract
+%% \verb/\implic/ation between formulae.
+%% The point is that \TeX\ spaces them and breaks the lines differently:
+%% \begin{center}
+%% \verb/A\implies B/ $A\implies B$\quad{\em versus\/}\quad
+%% \verb/A\implic B/ $A\implic B$
+%% \end{center}
+%% There are forward and reverse, single and Double versions.
+%%
+\mathchardef\implies="3221 \mathchardef\impliedby="3220 \mathchardef\Implies=%
+"3229 \mathchardef\Impliedby="3228 \mathchardef\implic="2221 \mathchardef
+\implicby="2220 \mathchardef\Implic="2229 \mathchardef\Implicby="2228 \let
+\imp\to%%
+%% Handle the spacing after a variable (and optionally its type)
+%% bound by a quantifier symbol. For example
+%% \begin{quote}
+%% \verb/\All x:X. \phi(x)/\quad prints as\quad $\All x:X.\phi(x)$\quad
+%% instead of\quad $\forall x:X.\phi(x)$
+%% \end{quote}
+\def\Quantifier#1#2.{\pb@G{#1}#2::.}\def\pb@G#1#2:#3:#4.{{{#1}{#2}\def\next{#%
+3}\ifx\next\empty{.}\mkern1mu \else\mkern1mu{\colon}\mkern1mu{#3}\mkern.5mu{.%
+}\mkern3mu \fi}}%
+%% We provide some commonly used forms; \verb/\iota/ ($\iota$) is Russell's
+%% description operator and should really be inverted.
+\def\All{\Quantifier\forall}\def\Some{\Quantifier\exists}\def\Function{%
+\Quantifier\lambda}\def\Product{\Quantifier\Pi}\def\Sum{\Quantifier\Sigma}%
+\def\TheOne{\Quantifier\iota}\def\Least{\Quantifier\mu}\def\Greatest{%
+\Quantifier\nu}%%
+%% There are several notations for substitution.
+%% After writing $a[x:=b]$ throughout my book I~thought I~might change to
+%% $[b/x]^*a$.
+%% This macro reads the source in the first form and prints in the second.
+%% If you use it you can, like me, defer the decision about
+%% which notation to use until the final stages, doing
+%% \begin{quote}
+%% \verb/\renewcommand{\Subst}{\plainsubstitution}/
+%% \end{quote}
+%% if you finally decide on making substitution act on the right.
+%% This is already an improvement on the literal text, because it
+%% automatically enlarges the brackets according to the text inside.
+%% \verb/\Subst/ itself is (following my book)
+%% defined in terms of the action of a context morphism (\verb/\CtxtMor/)
+%% on a term. Again you can do
+%% \begin{quote}
+%% \verb/\renewcommand{\CtxtMor}{\plaincontextmorphism}/
+%% \end{quote}
+%% for something simpler.
+%% This macro interprets its argument as a comma-separated list
+%% of items in the form $x:=b$, which it switches to $b/x$.
+\def\swappingsubstitution#1[#2]{{\CtxtMor[#2]^*{#1}}}\def
+\swappingcontextmorphism[#1]{{\let\pb@J\empty\left[\pb@H#1,[],\/\right]}}\def
+\pb@H#1,{\def\next{#1}\ifx\next\pb@K\else\pb@J\let\pb@J,\pb@I#1:=:=,%
+\expandafter\pb@H\fi}\def\pb@I#1:=#2:=#3,{{\def\next{#2}\ifx\next\empty\else{%
+#2}/\fi{#1} }}\def\pb@K{[]}\def\Subst{\swappingsubstitution}\def\CtxtMor{%
+\swappingcontextmorphism}%%
+%% The simple versions.
+\def\plainsubstitution#1#2{{#1}{\left[{#2}\right]}}\def\plaincontextmorphism#%
+1{{\left[#1\right]}}\newbox\pb@L\newdimen\pb@T\newdimen\pb@U\newdimen\pb@M
+\newdimen\pb@N\newdimen\pb@O\newdimen\pb@P\newdimen\pb@Q\newdimen\pb@R
+\newdimen\pb@S\def\pb@V#1#2{\relax\ifdim#1<#2\relax#1=#2\relax\fi}\count@
+\year\multiply\count@12 \advance\count@\month\ifnum\count@> 23966 \message{%
+because this one has expired and will no longer work!}\endinput\fi%%
+\def\proofbox{\relax\ifmmode\let\next\pb@a\else\let\next\pb@b\ifhmode\ifinner
+\let\next\pb@a\fi\fi\fi\next\global\prooflinetotal\@ne\boxmaxdepth\maxdimen
+\def\[{\pb@w\pb@f\pb@W}\def\({\pb@w\pb@f\pb@X}\def\proofbox{\[}\let\lbl\pb@y
+\def\"##1"{\pb@y{##1}}\def\:{\pb@v\proofboxproposition\displaystyle}\def\={%
+\pb@v\proofboxreason}\def\-{\pb@v\proofboxuse}\def\\{\pb@w\pb@u}\let\+\pb@c
+\let\*\pb@c\let\]\pb@c\pb@p\pb@s}\def\endproofbox{\pb@q\pb@IA\box\pb@L\egroup
+}\def\pb@W{\let\+\pb@d\let\*\pb@d\def\){\pb@e\[\)}\let\]\pb@Y\proofcolumns\z@
+}\def\pb@X{\proofcolumns\@ne\def\+{\pb@j\pb@l}\def\*{\pb@j\pb@m}\def\]{\pb@e
+\(\]}\let\)\pb@Y}\def\pb@Y{\pb@o\pb@u}\def\pb@a{\hbox\bgroup}\def\pb@b{$$%
+\kern-\displayindent\hbox to\hsize\bgroup\proofboxfullwidth\hsize\aftergroup$%
+\aftergroup$}\def\pb@c{\errmessage{Box proofs: \string\+, \string\*, \string
+\) and \string\] may not be used at the top level}}\def\pb@d{\errmessage{Box
+proofs: enclose \string\+ and \string\* in \string\(\string\), not \string\[%
+\string\]}}\def\pb@e#1#2{\errmessage{Box proofs: \string#1 closed by \string#%
+2}\pb@Y}\def\pb@f#1{\setbox\pb@L\hbox\bgroup#1\let\pb@g\pb@n\let
+\enclosingproofline\@currentlabel\edef\pb@h{\the\prooflinetotal}\let\pb@i
+\pb@h\pb@O\z@\pb@M\z@\pb@N-\maxdimen\pb@P\z@\pb@p\pb@t}\def\pb@j#1{\pb@q\pb@k
+\let\pb@g#1\advance\proofcolumns\@ne\global\prooflinetotal\pb@h
+\leftmostproofboxfalse\pb@p\pb@t}\def\pb@k{\pb@g\pb@V\pb@M{\wd\pb@L}\advance
+\pb@O\wd\pb@L\ifnum\pb@i<\prooflinetotal\edef\pb@i{\the\prooflinetotal}\fi
+\ifdim\pb@N<\dp\pb@L\pb@N\dp\pb@L\pb@P\pb@Q\fi\setbox\z@\hbox{%
+\proofboxtopside}\wd\z@\z@\box\z@\setbox\z@\hbox{\proofboxbottomside}\wd\z@
+\z@\box\z@\kern\pb@R\box\pb@L\kern\pb@S}\def\pb@l{\vtop{\proofboxorseparator}%
+\penalty\thr@@}\def\pb@m{\vtop{\proofboxrightside}\kern\proofboxseparation
+\vtop{\proofboxleftside}\penalty\tw@}\def\pb@n{\pb@T\pb@R\setbox\z@\vtop{%
+\proofboxleftside}\dimen@\wd\z@\advance\pb@T\dimen@\advance\pb@T
+\proofboxseparation\kern-\pb@T\kern\proofboxseparation\box\z@\penalty\@ne}%
+\def\pb@o{\pb@q\pb@k\setbox\z@\vtop{\proofboxrightside}\global\advance\pb@S
+\wd\z@\box\z@\global\advance\pb@S\proofboxseparation\kern\proofboxseparation
+\global\prooflinetotal\pb@i\global\pb@R\pb@T\global\pb@Q\pb@P\ifnum
+\proofcolumns<\@ne\proofcolumns\@ne\fi\penalty\proofcolumns\kern-\pb@M\kern
+\pb@M\kern-\pb@O\kern\pb@O\kern-\pb@S\penalty\@ne\egroup\pb@r}\def\pb@p#1{%
+\setbox\pb@L\vtop\bgroup\baselineskip\proofboxbaselineskip\prooflineinbox\@ne
+\pb@T\z@\pb@U\z@#1\pb@u}\def\pb@q{\pb@w\global\pb@R\pb@T\global\pb@S\pb@U
+\egroup}\def\pb@r{\pb@V\pb@T\pb@R\pb@V\pb@U\pb@S\box\pb@L\prevdepth\pb@Q}\def
+\pb@s{}\def\pb@t{}\def\pb@u{\edef\@currentlabel{\theproofline}\let\label@name
+\@currentlabel\setbox\proofboxproposition\box\voidb@x\setbox\proofboxreason
+\box\voidb@x\setbox\proofboxuse\box\voidb@x\setbox\proofboxvariables\hbox
+\bgroup\let\pb@z\pb@AA\let\pb@w\pb@x$}\def\pb@v#1{$\egroup\setbox#1\hbox
+\bgroup\let\pb@z\pb@AA$}\def\pb@w{$\egroup\global\advance\prooflinetotal\@ne
+\advance\prooflineinbox\@ne\setbox\pb@L\hbox{\setbox\z@\hbox{%
+\proofboxmakeleftcolumn}\global\pb@R\wd\z@\kern-\pb@R\box\z@\hbox{%
+\proofboxmakemiddlecolumn}\setbox\z@\hbox{\proofboxmakerightcolumn}\global
+\pb@S\wd\z@\box\z@\kern-\pb@S\penalty\tw@}\global\pb@Q\dp\pb@L\pb@r}\def\pb@x
+{$\egroup}\def\pb@y#1{\aftergroup\pb@z\expandafter\aftergroup\csname r@#1%
+\endcsname}\def\pb@z#1{\edef#1{{\@currentlabel}{}}\expandafter\pb@@A\string#1%
+\\}\expandafter\def\expandafter\pb@@A\string\r@#1\\{\def\label@name{#1}}\def
+\pb@AA#1{\aftergroup\pb@z\aftergroup#1}\expandafter\def\csname r@-\endcsname{%
+{\previous@label}{}}\dimendef\pb@BA=\@ne\dimendef\pb@CA=\tw@\dimendef\pb@DA=%
+\thr@@\dimendef\pb@EA=4 \dimendef\pb@FA=5 \dimendef\pb@GA=6 \chardef\pb@HA=9
+\def\pb@IA{\pb@GA\proofboxfullwidth\pb@T\proofboxleftmargin\pb@V\pb@T\pb@R
+\advance\pb@GA-\pb@T\pb@U\proofboxrightmargin\pb@V\pb@U\pb@S\advance\pb@GA-%
+\pb@U\pb@V\pb@GA{\wd\pb@L}\pb@JA}\def\pb@JA{\setbox\pb@L\vtop{\unvbox\pb@L
+\loop\skip@\lastskip\unskip\setbox\pb@HA\lastbox\ifhbox\pb@HA\pb@KA\repeat
+\unvbox\pb@L\unskip}}\def\pb@KA{\pb@DA\dp\pb@HA\pb@EA\ht\pb@HA\pb@CA\wd\pb@HA
+\setbox\pb@HA\hbox{\unhbox\pb@HA\count@\lastpenalty\unpenalty\unkern\ifodd
+\count@\pb@LA\else\setbox\thr@@\lastbox\setbox\tw@\lastbox\setbox\@ne\lastbox
+\unkern\hbox to\pb@T{\unhbox\@ne}\hbox to\pb@GA{\unhbox\tw@}\hbox to\pb@U{%
+\unhbox\thr@@}\fi}\dp\pb@HA\pb@DA\ht\pb@HA\pb@EA\setbox\pb@L\vtop{\box\pb@HA
+\nointerlineskip\vskip\skip@\unvbox\pb@L}}\def\pb@LA{\pb@O\lastkern\unkern
+\unkern\pb@M\lastkern\unkern\unkern\proofcolumns\lastpenalty\unpenalty\pb@FA
+\pb@T\ifnum\@ne=\proofcolumns\let\pb@MA\pb@NA\else\advance\pb@GA-\pb@CA\pb@BA
+\pb@GA\advance\pb@GA\pb@O\ifdim\pb@GA<\proofcolumns\pb@M\divide\pb@BA
+\proofcolumns\let\pb@MA\pb@PA\else\divide\pb@GA\proofcolumns\let\pb@MA\pb@OA
+\fi\fi\dimen@\lastkern\unkern\setbox\@ne\lastbox\pb@RA\setbox\pb@HA\hbox{\box
+\@ne\kern\dimen@}\advance\pb@U-\wd\pb@HA\unkern\loop\setbox\pb@L\lastbox\pb@T
+\lastkern\unkern\setbox\tw@\lastbox\setbox\thr@@\lastbox\count@\lastpenalty
+\unpenalty\pb@MA\pb@JA\setbox\@ne\vbox{\offinterlineskip\pb@QA\thr@@\vfil
+\pb@QA\tw@}\pb@RA\pb@TA{\box\@ne\box\pb@L}\ifnum\count@>\@ne\pb@SA\pb@U
+\lastkern\unkern\repeat\unhbox\pb@HA}\def\pb@NA{\pb@T\pb@FA\setbox\@ne
+\lastbox\advance\pb@T-\wd\@ne\dimen@\lastkern\unkern\unkern\kern\dimen@\pb@RA
+\box\@ne\advance\pb@T-\dimen@}\def\pb@OA{\ifnum\@ne=\count@\pb@NA\fi}\def
+\pb@PA{\pb@GA\wd\pb@L\advance\pb@GA\pb@BA\pb@OA}\def\pb@QA#1{\setbox#1\hbox to%
+\wd\pb@L{\unhbox#1}\wd#1\z@\box#1\relax}\def\pb@RA{\setbox\@ne\vbox to\pb@EA{%
+\offinterlineskip\vskip-\proofboxseparation\unvbox\@ne\vskip-%
+\proofboxseparation\setbox\z@\null\ht\z@-\pb@DA\dp\z@\pb@DA\box\z@}}\def
+\pb@SA{\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne}\ifodd\count@\else\dimen@
+\lastkern\unkern\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne\kern\dimen@}\fi}\def
+\pb@TA#1{\setbox\pb@HA\hbox{#1\unhbox\pb@HA}}\let\+\pb@A\proofboxrestoreat
+\endinput\def\x{}%%
+%% \end{document}
+% \fi