diff options
Diffstat (limited to 'obsolete/macros/generic')
-rw-r--r-- | obsolete/macros/generic/diagrams/barr/diagdoc.tex | 422 | ||||
-rw-r--r-- | obsolete/macros/generic/diagrams/barr/diagram.tex | 1048 | ||||
-rw-r--r-- | obsolete/macros/generic/proofs/taylor/boxproof-old.tex | 142 | ||||
-rw-r--r-- | obsolete/macros/generic/proofs/taylor/boxproof.tex | 424 |
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 |