]> matita.cs.unibo.it Git - helm.git/blob - helm/nuprl_stylesheets/nuprl_mmlextension.xsl
mathql_db_map.txt now retrieved by Helm_registry.
[helm.git] / helm / nuprl_stylesheets / nuprl_mmlextension.xsl
1 <?xml version="1.0"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--***********************************************************************--> 
28 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
29 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
30 <!-- Revised: March 3 2000, Irene Schena                                   -->
31 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
32 <!-- Revised: March 21 2000, Irene Schena                                  -->
33 <!--***********************************************************************--> 
34
35 <!-- NOTE: the namespace declaration has to be done in the stylesheets 
36 which generates the toplevel element (see for instance xlink) -->
37 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
38                               xmlns:m="http://www.w3.org/1998/Math/MathML"
39                               xmlns:helm="http://www.cs.unibo.it/helm"
40                               xmlns:xlink="http://www.w3.org/1999/xlink">
41
42 <!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
43
44 <xsl:import href="mmlnotation.xsl"/>
45
46 <xsl:import href="mmltheoryextension.xsl"/>
47
48 <xsl:key name="sequent_number" use="@id" match="Sequent"/>
49
50 <xsl:param name="explodeall" select="false()"/>
51
52 <!--***********************************************************************-->
53 <!-- Parameter affecting line-breaking                                     -->
54 <!--***********************************************************************-->
55
56 <xsl:variable name="framewidth" select="35"/> 
57
58 <!--***********************************************************************-->
59 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
60 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
61 <!-- sono i termini: la presentation per un termine e' generata come primo -->
62 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
63 <!-- nel secondo figlio di semantics, annotation-xml                       -->
64 <!--***********************************************************************-->
65
66 <!--**********************-->
67 <!--        OBJECTS       -->
68 <!--**********************-->
69
70
71 <!--<xsl:key name="variable" use="@name" match="Decl"/> -->
72
73 <xsl:param name="type" select="'standalone'"/>
74
75 <xsl:template match="/">
76  <xsl:choose>
77   <xsl:when test="$type = 'standalone'">
78    <xsl:apply-templates select="*"/>
79   </xsl:when>
80   <xsl:otherwise>
81    <to_be_embedded>
82     <xsl:apply-templates select="*"/>
83    </to_be_embedded>
84   </xsl:otherwise> 
85  </xsl:choose>
86 </xsl:template>
87
88
89 <!-- NODE -->
90
91  <xsl:template match="Node">
92      <xsl:choose>
93       <xsl:when test="count(Node)=0">    <!-- E' una foglia -->
94        <m:mtable align="baseline 1" equalrows="false" columnalign="left" stretchy="false">
95         <m:mtr>
96          <m:mtd>
97           <m:mrow>
98            <m:mtext mathcolor="red">Sequent <xsl:apply-templates select="Sequent/@id"/>
99            </m:mtext>
100           </m:mrow>
101          </m:mtd>
102         </m:mtr>
103         <m:mtr>
104         <xsl:if test="*[Decl]">
105          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
106           <xsl:for-each select="Sequent/Decl">
107            <m:mtr columnalign="left">
108             <m:mtd columnalign="left">
109              <m:mrow>
110               <xsl:variable name="num" select="position()"/>
111               <m:mtext>
112                <xsl:value-of select="$num"/>)
113               </m:mtext>
114               <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
115               <xsl:if test="@name">
116                <m:mo mathcolor="green"><xsl:value-of select="@name"/></m:mo>
117                <m:mo mathcolor="green" stretchy="false">:</m:mo>
118               </xsl:if>
119               <xsl:apply-templates select="."/>
120              </m:mrow>
121             </m:mtd>
122            </m:mtr>
123           </xsl:for-each>
124          </m:mtable>
125         </xsl:if>
126         </m:mtr>
127         <m:mtr>
128          <m:mrow>
129           <m:mtext mathcolor="red" mathvariant="bold">|-</m:mtext>
130          </m:mrow>
131         </m:mtr>
132         <m:mtr>
133          <m:mtd>
134           <xsl:apply-templates select="Sequent/Goal"/>
135          </m:mtd>
136         </m:mtr>
137         <m:mtr>
138          <m:mtd>
139           <m:mrow>
140            <m:mo mathcolor="red">Rule: </m:mo>
141            <xsl:choose>
142            <xsl:when test="Rule[m:apply]">
143             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:apply/m:ci"/></m:mo>
144            </xsl:when>
145            <xsl:when test="count(Rule)=0">
146             <m:mi>NESSUNA REGOLA</m:mi>
147            </xsl:when>
148            <xsl:otherwise>
149             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:ci"/></m:mo>
150            </xsl:otherwise>
151            </xsl:choose>
152           </m:mrow>
153          </m:mtd>
154         </m:mtr>
155         <m:mspace height="1ex"/>
156        </m:mtable>
157       </xsl:when>
158      
159      <xsl:otherwise>   <!--E' un nodo -->
160      <m:mtable equalrows="false" columnalign="left">
161       <m:mtr>
162        <m:mtable align="baseline 1" equalrows="false" columnalign="left" stretchy="false">
163         <m:mtr>
164          <m:mtd>
165           <m:mrow>
166            <m:mtext mathcolor="red">Sequent <xsl:apply-templates select="Sequent/@id"/>
167            </m:mtext>
168           </m:mrow>
169          </m:mtd>
170         </m:mtr>
171         <m:mtr>
172         <xsl:if test="*[Decl]">
173          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
174           <xsl:for-each select="Sequent/Decl">
175            <m:mtr columnalign="left">
176             <m:mtd columnalign="left">
177              <m:mrow>
178               <xsl:variable name="num" select="position()"/>
179               <m:mtext>
180                <xsl:value-of select="$num"/>)
181               </m:mtext>
182               <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
183               <xsl:if test="@name">
184                <m:mo mathcolor="green"><xsl:value-of select="@name"/></m:mo>
185                <m:mo mathcolor="green" stretchy="false">:</m:mo>
186               </xsl:if>
187               <xsl:apply-templates select="."/>
188              </m:mrow>
189             </m:mtd>
190            </m:mtr>
191           </xsl:for-each>
192          </m:mtable>
193         </xsl:if>
194         </m:mtr>
195         <m:mtr>
196          <m:mrow>
197           <m:mtext mathcolor="red" mathvariant="bold">|-</m:mtext>
198          </m:mrow>
199         </m:mtr>
200         <m:mtr>
201          <m:mtd>
202           <xsl:apply-templates select="Sequent/Goal"/>
203          </m:mtd>
204         </m:mtr>
205         <m:mtr>
206          <m:mtd>
207           <m:mrow>
208            <m:mo mathcolor="red">Rule: </m:mo>
209            <xsl:choose>
210            <xsl:when test="Rule[m:apply]">
211             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:apply/m:ci"/></m:mo>
212            </xsl:when>
213            <xsl:when test="count(Rule)=0">
214             <m:mi>NESSUNA REGOLA</m:mi>
215            </xsl:when>
216            <xsl:otherwise>
217             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:ci"/></m:mo>
218            </xsl:otherwise>
219            </xsl:choose>
220           </m:mrow>
221          </m:mtd>
222         </m:mtr>
223        </m:mtable>
224       </m:mtr>
225       <m:mtr>
226        <m:maction>
227         <xsl:choose>
228         <xsl:when test="count(Node)=1">
229          <m:mi mathcolor="blue" mathvariant="script">Subgoal</m:mi>
230         </xsl:when>
231         <xsl:otherwise>
232          <m:mi mathcolor="blue" mathvariant="script">Subgoals</m:mi>
233         </xsl:otherwise>
234         </xsl:choose>
235         <m:mrow>
236          <m:mspace width="1em"/>
237          <m:mtable equalrows="false" columnalign="left">
238           <xsl:for-each select="Node">
239            <m:mtr>
240             <xsl:apply-templates select="."/>
241            </m:mtr>
242            <m:mspace height="1ex"/>
243           </xsl:for-each>
244          </m:mtable>
245         </m:mrow>
246        </m:maction>
247       </m:mtr>
248      </m:mtable>
249      </xsl:otherwise>
250      </xsl:choose>
251 </xsl:template>
252
253
254 <!-- NuPRLDefinition -->
255
256 <xsl:template match="NuPrlDefinition">
257  <m:math>
258   <m:mrow>
259    <xsl:apply-templates select="*[1]"/>
260    <m:mo> := </m:mo>
261    <xsl:apply-templates select="*[2]"/>
262   </m:mrow>
263  </m:math>
264 </xsl:template>
265
266 <!-- DEFINITION -->
267
268 <xsl:template match="Definition">
269     <m:math>
270      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
271       <m:mtr>
272        <m:mtd>
273         <m:mrow>
274          <m:mtext>DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
275         </m:mrow>
276        </m:mtd>
277       </m:mtr>
278       <m:mtr>
279        <m:mtd>
280         <m:mrow>
281          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
282          <xsl:apply-templates select="type/*[1]"/>
283         </m:mrow>
284        </m:mtd>
285       </m:mtr>
286       <m:mtr>
287        <m:mtd>
288         <m:mrow>
289          <m:mtext>AS</m:mtext>
290         </m:mrow>
291        </m:mtd>
292       </m:mtr>
293       <m:mtr>
294        <m:mtd>
295         <m:mrow>
296          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
297          <xsl:apply-templates select="body/Node"/>   <!-- body/*[1]"/>-->
298         </m:mrow>
299        </m:mtd>
300       </m:mtr>
301      </m:mtable>
302     </m:math>
303 </xsl:template>
304
305 <!-- AXIOM -->
306
307 <xsl:template match="Axiom">
308     <m:math>
309      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
310       <m:mtr>
311        <m:mtd>
312         <m:mrow>
313          <m:mtext>AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
314         </m:mrow>
315        </m:mtd>
316       </m:mtr>
317       <m:mtr>
318        <m:mtd>
319         <m:mrow>
320          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
321          <xsl:apply-templates select="type/*[1]"/>
322         </m:mrow>
323        </m:mtd>
324       </m:mtr>
325      </m:mtable>
326     </m:math>
327 </xsl:template>
328
329 <!-- UNFINISHED PROOF -->
330
331 <xsl:template match="CurrentProof">
332     <m:math>
333      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
334       <m:mtr>
335        <m:mtd>
336         <m:mrow>
337          <m:mtext>UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)</m:mtext>
338         </m:mrow>
339        </m:mtd>
340       </m:mtr>
341       <m:mtr>
342        <m:mtd>
343         <m:mrow>
344          <m:mtext>THESIS:</m:mtext>
345         </m:mrow>
346        </m:mtd>
347       </m:mtr>
348       <m:mtr>
349        <m:mtd>
350         <m:mrow>
351          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
352          <xsl:apply-templates select="type/*[1]"/>
353         </m:mrow>
354        </m:mtd>
355       </m:mtr>
356       <m:mtr>
357        <m:mtd>
358         <m:mrow>
359          <m:mtext>CONJECTURES:</m:mtext>
360         </m:mrow>
361        </m:mtd>
362       </m:mtr>
363       <xsl:for-each select="Conjecture">
364       <m:mtr>
365        <m:mtd>
366         <m:mrow helm:xref="{@helm:xref}">
367          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
368          <xsl:for-each select="Decl|Def|Hidden">
369           <xsl:choose>
370            <xsl:when test="name(.)='Decl'">
371             <m:mrow helm:xref="{@helm:xref}">
372              <xsl:choose>
373               <xsl:when test="@name">
374                <m:mi><xsl:value-of select="@name"/></m:mi>
375               </xsl:when>
376               <xsl:otherwise>
377                <m:mi>_</m:mi>
378               </xsl:otherwise>
379              </xsl:choose>
380              <m:mo>:</m:mo>
381              <xsl:apply-templates select="./*[1]"/>
382             </m:mrow>
383            </xsl:when>
384            <xsl:when test="name(.)='Def'">
385             <m:mrow helm:xref="{@helm:xref}">
386              <xsl:choose>
387               <xsl:when test="@name">
388                <m:mi><xsl:value-of select="@name"/></m:mi>
389               </xsl:when>
390               <xsl:otherwise>
391                <m:mi>_</m:mi>
392               </xsl:otherwise>
393              </xsl:choose>
394              <m:mo>:=</m:mo>
395              <xsl:apply-templates select="./*[1]"/>
396             </m:mrow>
397            </xsl:when>
398            <xsl:otherwise>
399             <m:mrow helm:xref="{@helm:xref}">
400              <m:mi>_</m:mi>
401              <m:mo>:?</m:mo>
402              <m:mi>_</m:mi>
403             </m:mrow>
404            </xsl:otherwise>
405           </xsl:choose>
406           <xsl:if test="not (position() = last())">
407            <m:mo>;</m:mo>
408           </xsl:if>
409          </xsl:for-each>
410          <m:mo>|-</m:mo>
411          <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
412          <m:mo>:</m:mo>
413          <xsl:apply-templates select="./Goal/*[1]"/>
414         </m:mrow>
415        </m:mtd>
416       </m:mtr>
417       </xsl:for-each>
418       <m:mtr>
419        <m:mtd>
420         <m:mrow>
421          <m:mtext>PROOF:</m:mtext>
422         </m:mrow>
423        </m:mtd>
424       </m:mtr>
425       <m:mtr>
426        <m:mtd>
427         <m:mrow>
428          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
429          <xsl:apply-templates select="body/*[1]"/>
430         </m:mrow>
431        </m:mtd>
432       </m:mtr>
433      </m:mtable>
434     </m:math>
435 </xsl:template>
436
437 <!-- MUTUAL INDUCTIVE DEFINITION -->
438
439 <xsl:template match="InductiveDefinition">
440     <m:math>
441      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
442      <xsl:for-each select="InductiveType">
443       <m:mtr>
444        <m:mtd>
445         <m:mrow>
446          <xsl:choose>
447          <xsl:when test="position() = 1">
448           <xsl:choose>
449           <xsl:when test="string(./@inductive) = &quot;true&quot;">
450            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
451           </xsl:when>
452           <xsl:otherwise>
453            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
454           </xsl:otherwise>
455           </xsl:choose>  
456          </xsl:when>
457          <xsl:otherwise>
458           <m:mtext>AND</m:mtext>
459          </xsl:otherwise>
460          </xsl:choose>
461          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
462          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
463         </m:mrow>
464        </m:mtd>
465       </m:mtr>
466       <m:mtr>
467        <m:mtd>
468         <m:mrow> 
469          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
470          <m:mtext>[</m:mtext>
471          <xsl:choose>
472          <xsl:when test="string(../Param) != &quot;&quot;">         
473           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
474            <xsl:for-each select="../Param">
475             <m:mtr>
476              <m:mtd>
477               <m:mrow>   
478                <m:mi><xsl:value-of select="./@name"/></m:mi>
479                <m:mo>:</m:mo>
480                <xsl:apply-templates select="*"/>
481               </m:mrow>
482              </m:mtd>
483             </m:mtr>
484            </xsl:for-each>
485             <m:mtr>
486              <m:mtd>
487               <m:mrow>
488                <m:mtext>]</m:mtext>
489               </m:mrow>
490              </m:mtd>
491             </m:mtr>
492           </m:mtable>
493          </xsl:when>
494          <xsl:otherwise>
495           <m:mtext>]</m:mtext>
496          </xsl:otherwise>
497          </xsl:choose>
498         </m:mrow>
499        </m:mtd>
500       </m:mtr>
501       <m:mtr>
502        <m:mtd>
503         <m:mrow>
504          <m:mtext>OF ARITY</m:mtext>
505         </m:mrow>
506        </m:mtd>
507       </m:mtr>
508       <m:mtr>
509        <m:mtd>
510         <m:mrow>
511          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
512          <xsl:apply-templates select="./arity/*[1]"/>
513         </m:mrow>
514        </m:mtd>
515       </m:mtr>
516       <m:mtr>
517        <m:mtd>
518         <m:mrow>
519          <m:mtext>BUILT FROM</m:mtext>
520         </m:mrow>
521        </m:mtd>
522       </m:mtr>
523       <xsl:for-each select="./Constructor">
524       <m:mtr>
525        <m:mtd>
526         <m:mrow>
527          <xsl:choose>
528          <xsl:when test="position() = 1">
529           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
530          </xsl:when>
531          <xsl:otherwise>
532           <m:mtext>|</m:mtext>
533           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
534          </xsl:otherwise>
535          </xsl:choose>
536          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
537          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
538          <xsl:apply-templates select="./*[1]"/>
539         </m:mrow>
540        </m:mtd>
541       </m:mtr>
542       </xsl:for-each>
543      </xsl:for-each>
544      </m:mtable>
545     </m:math>
546 </xsl:template>
547
548 <!-- VARIABLE -->
549
550 <xsl:template match="Variable">
551     <m:math>
552      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
553       <m:mtr>
554        <m:mtd>
555         <m:mrow>
556          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
557         </m:mrow>
558        </m:mtd>
559       </m:mtr>
560       <m:mtr>
561        <m:mtd>
562         <m:mrow>
563          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
564          <xsl:apply-templates select="type/*[1]"/>
565         </m:mrow>
566        </m:mtd>
567       </m:mtr>
568       <xsl:if test="name(*[1])='body'">
569        <m:mtr>
570         <m:mtd>
571          <m:mrow>
572           <m:mtext>AS</m:mtext>
573          </m:mrow>
574         </m:mtd>
575        </m:mtr>
576        <m:mtr>
577         <m:mtd>
578          <m:mrow>
579           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
580           <xsl:apply-templates select="body/*[1]"/>
581          </m:mrow>
582         </m:mtd>
583        </m:mtr>
584       </xsl:if>
585      </m:mtable>
586     </m:math>
587 </xsl:template> 
588                 
589
590
591 <!-- SEQUENT -->
592 <!--
593 <xsl:template match="Sequent">
594  <xsl:variable name="rowlines">
595   <xsl:for-each select="Decl|Def">
596    <xsl:if test="position() != last()">
597     <xsl:text>none </xsl:text>
598    </xsl:if>
599   </xsl:for-each>
600   <xsl:text>solid</xsl:text>
601  </xsl:variable>
602  <xsl:variable name="no" select="@no"/>
603     <m:math>
604      <m:mi><xsl:text>?</xsl:text><xsl:value-of select="$no"/></m:mi>
605      <m:mo>:</m:mo>
606      <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
607      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
608       <xsl:for-each select="Decl|Def">
609        <m:mtr>
610         <m:mtd>
611          <m:mrow helm:xref="{@helm:xref}">
612           <m:mi><xsl:value-of select="@name"/></m:mi>
613           <xsl:choose>
614            <xsl:when test="name(.) = 'Decl'">
615             <m:mo>:</m:mo>
616            </xsl:when>
617            <xsl:otherwise>
618             <m:mo>:=</m:mo>
619            </xsl:otherwise>
620           </xsl:choose>
621           <xsl:apply-templates select="*[1]"/>
622          </m:mrow>
623         </m:mtd>
624        </m:mtr>
625       </xsl:for-each>
626       <xsl:if test="not(Decl|Def)">
627       <m:mtr>
628        <m:mtd>
629         <m:mrow>
630          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
631         </m:mrow>
632        </m:mtd>
633       </m:mtr>
634       </xsl:if>
635       <m:mtr>
636        <m:mtd>
637         <m:mrow>
638          <xsl:apply-templates select="Goal/*[1]"/>
639         </m:mrow>
640        </m:mtd>
641       </m:mtr>
642      </m:mtable>
643     </m:math>
644 </xsl:template>-->
645
646 <!--**********************-->
647 <!--        TERMS         -->
648 <!--**********************-->
649
650 <xsl:template match="m:bvar">
651  <xsl:choose>
652   <xsl:when test="m:type">
653    <xsl:variable name="charlength">
654     <xsl:apply-templates select="m:ci" mode="charcount"/>
655    </xsl:variable>
656    <xsl:choose>
657     <xsl:when test="$charlength >= $framewidth">
658      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
659       <m:mtr>
660        <m:mtd>
661         <m:mrow>
662          <xsl:apply-templates select="m:ci"/>
663          <m:mo>:</m:mo>
664         </m:mrow>
665        </m:mtd>
666       </m:mtr>
667       <m:mtr>
668        <m:mtd>
669         <m:mrow>
670          <xsl:apply-templates select="m:type"/>
671         </m:mrow>
672        </m:mtd>
673       </m:mtr>
674      </m:mtable>
675     </xsl:when>
676     <xsl:otherwise>
677      <m:mrow>
678       <xsl:apply-templates select="m:ci"/>
679       <m:mo>:</m:mo>
680       <xsl:apply-templates select="m:type"/>
681      </m:mrow>
682     </xsl:otherwise>
683    </xsl:choose>
684   </xsl:when>
685   <xsl:otherwise>
686    <xsl:apply-templates select="m:ci"/>
687   </xsl:otherwise>
688  </xsl:choose>
689 </xsl:template>
690
691 <xsl:template match="m:apply[m:implies]">
692     <xsl:variable name="charlength"><xsl:apply-templates select="m:implies" mode="charcount"/></xsl:variable>
693       <xsl:choose>
694        <xsl:when test="$charlength >= $framewidth">
695         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
696          <m:mtr>
697           <m:mtd>
698            <m:mrow>
699             <xsl:apply-templates select="*[2]"/>
700            </m:mrow>
701           </m:mtd>
702          </m:mtr>
703          <m:mtr>
704           <m:mtd>
705            <m:mrow>
706             <m:mo>&#8658;</m:mo>
707             <xsl:apply-templates select="*[position()=3]"/>
708            </m:mrow>
709           </m:mtd>
710          </m:mtr>
711         </m:mtable>
712        </xsl:when>
713        <xsl:otherwise>
714         <xsl:apply-templates select="*[2]"/>
715         <m:mo>&#8658;</m:mo>
716         <xsl:apply-templates select="*[position()=3]"/>
717        </xsl:otherwise>
718       </xsl:choose> 
719 </xsl:template>
720
721 <!-- CSYMBOL -->
722
723 <xsl:template match="m:apply[m:csymbol]">
724 <xsl:param name="nopar" select="0"/>
725     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
726     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
727     <m:mrow>
728      <xsl:if test="@id">
729       <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
730      </xsl:if>
731      <xsl:variable name="id" select="m:csymbol/@id"/>
732      <xsl:choose>
733       <!-- META -->
734       <xsl:when test="$name='meta'">
735        <m:mrow>
736         <xsl:apply-templates select="*[position()=2]"/>
737         <m:mfenced open="[" close="]" separators=";">
738          <xsl:apply-templates select="*[position()>2]"/>
739         </m:mfenced>
740        </m:mrow>
741       </xsl:when>
742       <!-- FORALL *-->
743       <xsl:when test="$name='forall'">
744        <xsl:choose>
745        <xsl:when test="$charlength >= $framewidth">
746         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
747          <m:mtr>
748           <m:mtd>
749            <m:mrow>
750             <m:mo mathcolor="Blue">&#8704;</m:mo>
751             <xsl:apply-templates select="m:bvar"/>
752            </m:mrow>
753           </m:mtd>
754          </m:mtr>
755          <m:mtr>
756           <m:mtd>
757            <m:mrow>
758             <m:mo>.</m:mo>
759             <xsl:apply-templates select="*[position()=3]"/>
760            </m:mrow>
761           </m:mtd>
762          </m:mtr>
763         </m:mtable>
764        </xsl:when>
765        <xsl:otherwise>
766         <m:mo mathcolor="Blue">&#8704;</m:mo>
767         <xsl:apply-templates select="m:bvar/m:ci"/>
768         <m:mo>:</m:mo>
769         <xsl:apply-templates select="m:bvar/m:type"/>
770         <m:mo>.</m:mo>
771         <xsl:apply-templates select="*[position()=3]"/>
772        </xsl:otherwise>
773        </xsl:choose> 
774       </xsl:when>
775       <!-- LET-IN -->
776       <xsl:when test="$name='let_in'">
777        <xsl:choose>
778        <xsl:when test="$charlength >= $framewidth">
779         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
780          <m:mtr>
781           <m:mtd>
782            <m:mrow>
783             <m:mo>LET</m:mo>
784             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
785             <xsl:apply-templates select="m:bvar"/>
786            </m:mrow>
787           </m:mtd>
788          </m:mtr>
789          <m:mtr>
790           <m:mtd>
791            <m:mrow>
792             <m:mo>=</m:mo>
793             <xsl:apply-templates select="*[position()=3]"/>
794            </m:mrow>
795           </m:mtd>
796          </m:mtr>
797          <m:mtr>
798           <m:mtd>
799            <m:mrow>
800             <m:mo>IN</m:mo>
801             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
802             <xsl:apply-templates select="*[position()=4]"/>
803            </m:mrow>
804           </m:mtd>
805          </m:mtr>
806         </m:mtable>
807        </xsl:when>
808        <xsl:otherwise>
809         <m:mo>LET</m:mo>
810         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
811         <xsl:apply-templates select="m:bvar/m:ci"/>
812         <m:mo>=</m:mo>
813         <xsl:apply-templates select="*[position()=3]"/>
814         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
815         <m:mtext>IN</m:mtext>
816         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
817         <xsl:apply-templates select="*[position()=4]"/>
818        </xsl:otherwise>
819        </xsl:choose>
820       </xsl:when> 
821       <!-- PROD *-->
822       <xsl:when test="$name='prod'">
823        <xsl:choose>
824        <xsl:when test="$charlength >= $framewidth">
825         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
826          <m:mtr>
827           <m:mtd>
828            <m:mrow>
829             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
830             <xsl:apply-templates select="m:bvar"/>
831            </m:mrow>
832           </m:mtd>
833          </m:mtr>
834          <m:mtr>
835           <m:mtd>
836            <m:mrow>
837             <m:mo>.</m:mo>
838             <xsl:apply-templates select="*[position()=3]"/>
839            </m:mrow>
840           </m:mtd>
841          </m:mtr>
842         </m:mtable>
843        </xsl:when>
844        <xsl:otherwise>
845         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
846         <xsl:apply-templates select="m:bvar/m:ci"/>
847         <m:mo>:</m:mo>
848         <xsl:apply-templates select="m:bvar/m:type"/>
849         <m:mo>.</m:mo>
850         <xsl:apply-templates select="*[position()=3]"/>
851        </xsl:otherwise>
852        </xsl:choose> 
853       </xsl:when>
854       <!-- ARROW *-->
855       <xsl:when test="$name='arrow'">
856        <xsl:choose>
857        <xsl:when test="$charlength >= $framewidth">
858         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
859          <m:mtr>
860           <m:mtd>
861            <m:mrow>
862             <xsl:if test="$nopar=0">
863              <m:mo stretchy="false">(</m:mo>
864             </xsl:if>
865             <xsl:apply-templates select="*[position()=2]"/>
866            </m:mrow>
867           </m:mtd>
868          </m:mtr>
869          <m:mtr>
870           <m:mtd>
871            <m:mrow>
872             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
873             <xsl:choose>
874             <xsl:when test="*[position()=3]/m:csymbol">
875              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
876              <xsl:choose>
877              <xsl:when test="$nextp='arrow'">
878               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
879              </xsl:when>
880              <xsl:otherwise>
881               <xsl:apply-templates select="*[position()=3]"/>
882              </xsl:otherwise>
883              </xsl:choose>
884             </xsl:when>
885             <xsl:otherwise>
886              <xsl:apply-templates select="*[position()=3]"/>
887             </xsl:otherwise>
888             </xsl:choose>
889            </m:mrow>
890           </m:mtd>
891          </m:mtr>
892          <xsl:if test="$nopar=0">
893          <m:mtr>
894           <m:mtd>
895            <m:mrow>
896             <m:mo stretchy="false">)</m:mo>
897            </m:mrow>
898           </m:mtd>
899          </m:mtr>
900          </xsl:if>
901         </m:mtable>
902        </xsl:when>
903        <xsl:otherwise>
904         <xsl:if test="$nopar=0">
905          <m:mo stretchy="false">(</m:mo>
906         </xsl:if>
907         <xsl:apply-templates select="*[position()=2]"/>
908         <m:mo mathcolor="Blue">&#x2192;</m:mo>
909         <xsl:choose>
910         <xsl:when test="*[position()=3]/m:csymbol">
911          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
912          <xsl:choose>
913          <xsl:when test="$nextp='arrow'">
914           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
915          </xsl:when>
916          <xsl:otherwise>
917           <xsl:apply-templates select="*[position()=3]"/>
918          </xsl:otherwise>
919          </xsl:choose>
920         </xsl:when>
921         <xsl:otherwise>
922          <xsl:apply-templates select="*[position()=3]"/>
923         </xsl:otherwise>
924         </xsl:choose>
925         <xsl:if test="$nopar=0">
926          <m:mo stretchy="false">)</m:mo>
927         </xsl:if>
928        </xsl:otherwise>
929        </xsl:choose>
930       </xsl:when>
931       <!-- TYPE_OF -->
932       <xsl:when test="$name='type_of'">
933        <xsl:choose>
934        <xsl:when test="$charlength >= $framewidth">
935         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
936          <m:mtr>
937           <m:mtd>
938            <m:mrow>
939             <xsl:value-of select="*[2]"/>
940             <m:mo>:</m:mo>
941            </m:mrow>
942           </m:mtd>
943          </m:mtr>
944          <m:mtr>
945           <m:mtd>
946            <m:mrow>
947             <xsl:apply-templates select="*[3]"/>
948            </m:mrow>
949           </m:mtd>
950          </m:mtr>
951         </m:mtable>
952        </xsl:when>
953        <xsl:otherwise>
954         <m:mrow>
955          <xsl:apply-templates select="*[2]"/>
956          <m:mo>:</m:mo>
957          <xsl:apply-templates select="*[3]"/>
958         </m:mrow>
959        </xsl:otherwise>
960        </xsl:choose>
961       </xsl:when>
962       <!--PRODUCT -->
963       <xsl:when test="$name='product'">
964        <xsl:choose>
965        <xsl:when test="$charlength >= $framewidth">
966         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
967          <m:mtr>
968           <m:mtd>
969            <m:mrow>
970             <m:mo mathcolor="Blue">&#931;</m:mo>
971             <xsl:apply-templates select="m:bvar/m:ci"/>
972             <m:mo>:</m:mo>
973             <xsl:apply-templates select="m:bvar/m:type"/>
974            </m:mrow>
975           </m:mtd>
976          </m:mtr>
977          <m:mtr>
978           <m:mtd>
979            <m:mrow>
980             <m:mtext>.</m:mtext>
981             <xsl:apply-templates select="*[position()=3]"/>
982            </m:mrow>
983           </m:mtd>
984          </m:mtr>
985         </m:mtable>
986        </xsl:when>
987        <xsl:otherwise>
988         <m:mrow>
989          <m:mo mathcolor="Blue">&#931;</m:mo>
990          <xsl:apply-templates select="m:bvar/m:ci"/>
991          <m:mo>:</m:mo>
992          <xsl:apply-templates select="m:bvar/m:type"/>
993          <m:mtext>.</m:mtext>
994          <xsl:apply-templates select="*[position()=3]"/>
995         </m:mrow>
996        </xsl:otherwise>
997        </xsl:choose>
998       </xsl:when>
999       <!-- PROD_IND -->
1000       <xsl:when test="$name='product_ind'">
1001        <xsl:choose>
1002        <xsl:when test="$charlength >= $framewidth">
1003         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1004          <m:mtr>
1005           <m:mtd>
1006            <m:mrow>
1007             <m:mo stretchy="false">(</m:mo>
1008             <xsl:apply-templates select="m:type"/>
1009            </m:mrow>
1010           </m:mtd>
1011          </m:mtr>
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <m:mo mathcolor="Blue">x</m:mo>
1016             <xsl:apply-templates select="*[position()=3]"/>
1017             <m:mo stretchy="false">)</m:mo>
1018            </m:mrow>
1019           </m:mtd>
1020          </m:mtr>
1021         </m:mtable>
1022        </xsl:when>
1023        <xsl:otherwise>
1024         <m:mrow>
1025          <m:mo stretchy="false">(</m:mo>
1026          <xsl:apply-templates select="m:type"/>
1027          <m:mo mathcolor="Blue">x</m:mo>
1028          <xsl:apply-templates select="*[position()=3]"/>
1029          <m:mo stretchy="false">)</m:mo>
1030         </m:mrow>
1031        </xsl:otherwise>
1032        </xsl:choose>
1033       </xsl:when>
1034       <!-- PAIR -->
1035       <xsl:when test="$name='pair'">
1036        <xsl:choose>
1037        <xsl:when test="$charlength >= $framewidth">
1038         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1039          <m:mtr>
1040           <m:mtd>
1041            <m:mrow>
1042             <m:mo mathcolor="Blue">&lt;</m:mo>
1043             <xsl:apply-templates select="*[2]"/>
1044             <m:mtext>, </m:mtext>
1045            </m:mrow>
1046           </m:mtd>
1047          </m:mtr>
1048          <m:mtr>
1049           <m:mtd>
1050            <m:mrow>
1051             <xsl:apply-templates select="*[3]"/>
1052             <m:mo mathcolor="Blue">&gt;</m:mo>
1053            </m:mrow>
1054           </m:mtd>
1055          </m:mtr>
1056         </m:mtable>
1057        </xsl:when>
1058        <xsl:otherwise>
1059         <m:mrow>
1060          <m:mo mathcolor="Blue">&lt;</m:mo>
1061          <xsl:apply-templates select="*[2]"/>
1062          <m:mtext>, </m:mtext>
1063          <xsl:apply-templates select="*[3]"/>
1064          <m:mo mathcolor="Blue">&gt;</m:mo>
1065         </m:mrow>
1066        </xsl:otherwise>
1067        </xsl:choose>
1068       </xsl:when>
1069       <!-- UNION -->
1070       <xsl:when test="$name='union'">
1071        <xsl:choose>
1072        <xsl:when test="$charlength >= $framewidth">
1073         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1074          <m:mtr>
1075           <m:mtd>
1076            <xsl:apply-templates select="*[2]"/>
1077           </m:mtd>
1078          </m:mtr>
1079          <m:mtr>
1080           <m:mtd>
1081            <m:mrow>
1082             <m:mo mathcolor="Blue">+</m:mo>
1083             <xsl:apply-templates select="*[3]"/>
1084            </m:mrow>
1085           </m:mtd>
1086          </m:mtr>
1087         </m:mtable>
1088        </xsl:when>
1089        <xsl:otherwise>
1090         <m:mrow>
1091          <xsl:apply-templates select="*[2]"/>
1092          <m:mo mathcolor="Blue">+</m:mo>
1093          <xsl:apply-templates select="*[3]"/>
1094         </m:mrow>
1095        </xsl:otherwise>
1096        </xsl:choose>
1097       </xsl:when>
1098       <!-- INL -->
1099       <xsl:when test="$name='inl'">
1100        <m:mrow>
1101         <m:mo stretchy="false" mathcolor="Blue">inl(</m:mo>
1102         <xsl:apply-templates select="*[position()=2]"/>
1103         <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1104        </m:mrow>
1105       </xsl:when>
1106       <!-- INR -->
1107       <xsl:when test="$name='inr'">
1108        <m:mrow>
1109         <m:mo stretchy="false" mathcolor="Blue">inr(</m:mo>
1110         <xsl:apply-templates select="*[position()=2]"/>
1111         <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1112        </m:mrow>
1113       </xsl:when>
1114       <!-- AXIOM -->
1115       <xsl:when test="$name='Ax'">
1116        <m:mo mathcolor="Blue">Ax</m:mo>
1117       </xsl:when>
1118       <!-- VOID -->
1119       <xsl:when test="$name='void'">
1120        <m:mo mathcolor="Blue">Void</m:mo>
1121       </xsl:when>
1122       <!-- ATOM -->
1123       <xsl:when test="$name='atom'">
1124        <m:mo mathcolor="Blue">Atom</m:mo>
1125       </xsl:when>
1126       <!-- UNIVERSE -->
1127       <xsl:when test="$name='universe'">
1128        <m:msub>
1129         <m:mo>U</m:mo>
1130         <xsl:apply-templates select="m:cn"/>
1131        </m:msub>
1132       </xsl:when>
1133       <!-- PROP -->
1134       <xsl:when test="$name='prop'">
1135        <m:msub>
1136         <m:mo>P</m:mo>
1137          <xsl:apply-templates select="m:cn"/>
1138        </m:msub>
1139       </xsl:when>
1140       <!-- EQUAL -->
1141       <xsl:when test="$name='equal'">
1142        <xsl:choose>
1143        <xsl:when test="$charlength >= $framewidth">
1144         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1145          <m:mtr>
1146           <m:mtd>
1147           <xsl:apply-templates select="*[position()=3]"/>
1148           </m:mtd>
1149          </m:mtr>
1150          <m:mtr>
1151           <m:mtd>
1152            <m:mrow>
1153             <m:mo mathcolor="Blue">=</m:mo>
1154             <xsl:apply-templates select="*[position()=4]"/>
1155            </m:mrow>
1156           </m:mtd>
1157          </m:mtr>
1158          <m:mtr>
1159           <m:mtd>
1160            <m:mrow>
1161             <m:mo mathcolor="Blue">&#x02208;</m:mo>
1162             <xsl:apply-templates select="*[position()=2]"/>
1163            </m:mrow>
1164          </m:mtd>
1165         </m:mtr>
1166        </m:mtable>
1167       </xsl:when>
1168       <xsl:otherwise>
1169        <m:mrow>
1170         <xsl:apply-templates select="*[position()=3]"/>
1171         <m:mo mathcolor="Blue">=</m:mo>
1172         <xsl:apply-templates select="*[position()=4]"/>
1173         <m:mo mathcolor="Blue">&#x02208;</m:mo>
1174         <xsl:apply-templates select="*[position()=2]"/>
1175        </m:mrow>
1176       </xsl:otherwise>
1177      </xsl:choose>
1178     </xsl:when>
1179     <!-- TOKEN  -->
1180     <xsl:when test="$name='token'">
1181      <m:mrow>
1182       <m:mo mathcolor="Blue">"</m:mo>
1183       <xsl:apply-templates select="m:ci"/>
1184       <m:mo mathcolor="Blue">"</m:mo>
1185      </m:mrow>
1186     </xsl:when>
1187     <!-- NIL  -->
1188     <xsl:when test="$name='nil'">
1189      <m:mo mathcolor="Blue">[]</m:mo>
1190     </xsl:when>
1191     <!-- CONS -->
1192     <xsl:when test="$name='cons'">
1193      <xsl:choose>
1194      <xsl:when test="$charlength >= $framewidth">
1195       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1196        <m:mtr>
1197         <m:mtd>
1198          <xsl:apply-templates select="*[2]"/>
1199         </m:mtd>
1200       </m:mtr>
1201       <m:mtr>
1202        <m:mtd>
1203         <m:mrow>
1204          <m:mo mathcolor="Blue">::</m:mo>
1205          <xsl:apply-templates select="*[3]"/>
1206         </m:mrow>
1207        </m:mtd>
1208       </m:mtr>
1209      </m:mtable>
1210     </xsl:when>
1211     <xsl:otherwise>
1212      <m:mrow>
1213       <xsl:apply-templates select="*[2]"/>
1214       <m:mo mathcolor="Blue">::</m:mo>
1215       <xsl:apply-templates select="*[3]"/>
1216      </m:mrow>
1217     </xsl:otherwise>
1218    </xsl:choose>
1219   </xsl:when>
1220
1221 <!-- REC -->
1222 <xsl:when test="$name='rec'">
1223 <xsl:choose>
1224 <xsl:when test="$charlength >= $framewidth">
1225 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1226  <m:mtr>
1227   <m:mtd>
1228    <m:mrow>
1229     <m:mo>rectype</m:mo>
1230     <xsl:apply-templates select="*[2]"/>
1231    </m:mrow>
1232   </m:mtd>
1233  </m:mtr>
1234  <m:mtr>
1235   <m:mtd>
1236    <m:mrow>
1237     <m:mo>=</m:mo>
1238     <xsl:apply-templates select="*[3]"/>
1239    </m:mrow>
1240   </m:mtd>
1241  </m:mtr>
1242 </m:mtable>
1243 </xsl:when>
1244 <xsl:otherwise>
1245 <m:mrow>
1246  <m:mo>rectype</m:mo>
1247  <xsl:apply-templates select="*[2]"/>
1248  <m:mo>=</m:mo>
1249  <xsl:apply-templates select="*[3]"/>
1250 </m:mrow>
1251 </xsl:otherwise>
1252 </xsl:choose>
1253 </xsl:when>
1254
1255 <!-- SET  -->
1256 <xsl:when test="$name='t_set'">
1257 <xsl:choose>
1258 <xsl:when test="$charlength >= $framewidth">
1259 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1260  <m:mtr>
1261   <m:mtd>
1262    <m:mrow>
1263     <m:mo mathcolor="Blue" stretchy="false">{</m:mo>
1264     <xsl:choose>
1265     <xsl:when test="m:bvar/m:ci">
1266      <xsl:apply-templates select="m:bvar/m:ci"/>
1267      <m:mo mathcolor="Blue">:</m:mo>
1268      <xsl:apply-templates select="m:bvar/m:type"/>
1269     </xsl:when>
1270     <xsl:otherwise>
1271      <xsl:apply-templates select="m:bvar/m:type"/>
1272     </xsl:otherwise>
1273     </xsl:choose>
1274    </m:mrow>
1275   </m:mtd>
1276  </m:mtr>
1277  <m:mtr>
1278   <m:mtd>
1279    <m:row>
1280     <m:mo mathcolor="Blue" stretchy="false">|</m:mo>
1281     <xsl:apply-templates select="*[3]"/>
1282     <m:mo mathcolor="Blue" stretchy="false">}</m:mo>
1283    </m:row>
1284   </m:mtd>
1285  </m:mtr>
1286 </m:mtable>
1287 </xsl:when>
1288 <xsl:otherwise>
1289 <m:row>
1290  <m:mo mathcolor="Blue" stretchy="false">{</m:mo>
1291  <xsl:choose>
1292  <xsl:when test="m:bvar/m:ci">
1293   <xsl:apply-templates select="m:bvar/m:ci"/>
1294   <m:mo mathcolor="Blue">:</m:mo>
1295   <xsl:apply-templates select="m:bvar/m:type"/>
1296  </xsl:when> 
1297  <xsl:otherwise>
1298   <xsl:apply-templates select="m:bvar/m:type"/>
1299  </xsl:otherwise>
1300  </xsl:choose>
1301  <m:mo mathcolor="Blue" stretchy="false">|</m:mo>
1302  <xsl:apply-templates select="*[3]"/>
1303  <m:mo mathcolor="Blue" stretchy="false">}</m:mo>
1304 </m:row>
1305 </xsl:otherwise>
1306 </xsl:choose>
1307 </xsl:when>
1308
1309 <!-- ISECT -->
1310 <xsl:when test="$name='isect'">
1311 <xsl:choose>
1312 <xsl:when test="$charlength >= $framewidth">
1313 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1314  <m:mtr>
1315   <m:mtd>
1316    <m:mrow>
1317     <m:mo mathcolor="Blue">&#xc7;</m:mo>
1318     <xsl:apply-templates select="m:bvar/m:ci"/>
1319     <m:mo mathcolor="Blue">:</m:mo>
1320     <xsl:apply-templates select="m:bvar/m:type"/>
1321    </m:mrow>
1322   </m:mtd>
1323  </m:mtr>
1324  <m:mtr>
1325   <m:mtd>
1326    <m:mrow>
1327     <m:mo mathcolor="Blue">.</m:mo>
1328     <xsl:apply-templates select="*[3]"/>
1329    </m:mrow>
1330   </m:mtd>
1331  </m:mtr>
1332 </m:mtable>
1333 </xsl:when>
1334 <xsl:otherwise>
1335 <m:mrow>
1336  <m:mo mathcolor="Blue">&#xc7;</m:mo>
1337  <xsl:apply-templates select="m:bvar/m:ci"/>
1338  <m:mo mathcolor="Blue">:</m:mo>
1339  <xsl:apply-templates select="m:bvar/m:type"/>
1340  <m:mo mathcolor="Blue">.</m:mo>
1341  <xsl:apply-templates select="*[3]"/>
1342 </m:mrow>
1343 </xsl:otherwise>
1344 </xsl:choose>
1345 </xsl:when>
1346 <!-- QUOTIENT -->
1347 <xsl:when test="$name='quotient'">
1348 <xsl:choose>
1349 <xsl:when test="$charlength >= $framewidth">
1350 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1351  <m:mtr>
1352   <m:mtd>
1353    <m:mrow>
1354     <xsl:apply-templates select="m:bvar[1]"/>
1355     <m:mo mathcolor="Blue">,</m:mo>
1356     <xsl:apply-templates select="m:bvar[2]"/>
1357     <m:mo mathcolor="Blue">:</m:mo>
1358     <xsl:apply-templates select="*[2]"/>
1359    </m:mrow>
1360   </m:mtd>
1361  </m:mtr>
1362  <m:mtr>
1363   <m:mtd>
1364    <m:mrow>
1365     <m:mo mathcolor="Blue">//</m:mo>
1366     <xsl:apply-templates select="*[5]"/>
1367    </m:mrow>
1368   </m:mtd>
1369  </m:mtr>
1370 </m:mtable>
1371 </xsl:when>
1372 <xsl:otherwise>
1373 <m:mrow>
1374  <xsl:apply-templates select="m:bvar[1]"/>
1375  <m:mo mathcolor="Blue">,</m:mo>
1376  <xsl:apply-templates select="m:bvar[2]"/>
1377  <m:mo mathcolor="Blue">:</m:mo>
1378  <xsl:apply-templates select="*[2]"/>
1379  <m:mo mathcolor="Blue">//</m:mo>
1380  <xsl:apply-templates select="*[5]"/>
1381 </m:mrow>
1382 </xsl:otherwise>
1383 </xsl:choose>
1384 </xsl:when>
1385 <!-- IF_THEN_ELSE -->
1386 <xsl:when test="$name='if_then_else'">
1387 <xsl:choose>
1388 <xsl:when test="$charlength >= $framewidth">
1389 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1390  <m:mtr>
1391   <m:mtd>
1392   <m:mrow>
1393    <xsl:choose>
1394    <xsl:when test="m:where = 'atom_eq'">
1395     <m:mo stretchy="false" mathcolor="Blue">atom_eq (</m:mo>
1396    </xsl:when>
1397    <xsl:when test="m:where = 'int_eq'">
1398     <m:mo stretchy="false" mathcolor="Blue">int_eq (</m:mo>
1399    </xsl:when>
1400    <xsl:when test="m:where = 'less'">
1401     <m:mo stretchy="false" mathcolor="Blue">less (</m:mo>
1402    </xsl:when>
1403    </xsl:choose>
1404    <xsl:apply-templates select="*[3]"/>
1405    <m:mo mathcolor="Blue">;</m:mo>
1406    </m:mrow>
1407   </m:mtd>
1408  </m:mtr>
1409  <m:mtr>
1410   <m:mtd>
1411    <m:mrow>
1412     <xsl:apply-templates select="*[4]"/>
1413     <m:mo mathcolor="Blue">;</m:mo>
1414    </m:mrow>
1415   </m:mtd>
1416  </m:mtr>
1417  <m:mtr>
1418   <m:mtd>
1419    <m:mrow>
1420     <xsl:apply-templates select="*[5]"/>
1421     <m:mo mathcolor="Blue">;</m:mo>
1422    </m:mrow>
1423   </m:mtd>
1424  </m:mtr>
1425  <m:mtr>
1426   <m:mtd>
1427    <m:mrow>
1428     <xsl:apply-templates select="*[6]"/>
1429     <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1430    </m:mrow>
1431   </m:mtd>
1432  </m:mtr>
1433 </m:mtable>
1434 </xsl:when>
1435 <xsl:otherwise>
1436 <m:mrow>
1437  <xsl:choose>
1438  <xsl:when test="m:where = 'atom_eq'">
1439   <m:mo stretchy="false" mathcolor="Blue">atom_eq (</m:mo>
1440  </xsl:when>
1441  <xsl:when test="m:where = 'int_eq'">
1442   <m:mo stretchy="false" mathcolor="Blue">int_eq (</m:mo>
1443  </xsl:when>
1444  <xsl:when test="m:where = 'less'">
1445   <m:mo stretchy="false" mathcolor="Blue">less (</m:mo>
1446  </xsl:when>
1447  </xsl:choose>
1448  <xsl:apply-templates select="*[3]"/>
1449  <m:mo mathcolor="Blue">;</m:mo>
1450  <xsl:apply-templates select="*[4]"/>
1451  <m:mo mathcolor="Blue">;</m:mo>
1452  <xsl:apply-templates select="*[5]"/>
1453  <m:mo mathcolor="Blue">;</m:mo> 
1454  <xsl:apply-templates select="*[6]"/>
1455  <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1456 </m:mrow>
1457 </xsl:otherwise>
1458 </xsl:choose>
1459 </xsl:when>
1460 <!-- SO_LAMBDA -->
1461 <xsl:when test="$name='so_lambda'">
1462 <xsl:choose>
1463 <xsl:when test="($charlength - 4) >= $framewidth">
1464 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1465  <m:mtr>
1466   <m:mtd>
1467    <m:mrow>
1468     <m:mo mathcolor="red">&#x03bb;</m:mo>
1469     <xsl:apply-templates select="m:apply[1]/*[2]"/>
1470    </m:mrow>
1471   </m:mtd>
1472  </m:mtr>
1473  <m:mtr>
1474   <m:mtd>
1475    <m:mrow>
1476     <m:mo>.</m:mo>
1477     <xsl:apply-templates select="*[3]"/>
1478    </m:mrow>
1479   </m:mtd>
1480  </m:mtr>
1481 </m:mtable>
1482 </xsl:when>
1483 <xsl:otherwise>
1484 <m:mrow>
1485  <m:mo mathcolor="red">&#x03bb;</m:mo>
1486  <xsl:apply-templates select="m:apply[1]/m:ci[2]"/>
1487  <m:mo>.</m:mo>
1488  <xsl:apply-templates select="*[3]"/>
1489 </m:mrow>
1490 </xsl:otherwise>
1491 </xsl:choose>
1492 </xsl:when>
1493 <!-- SO_APPLY -->
1494 <xsl:when test="$name='so_apply'">
1495 <xsl:choose>
1496 <xsl:when test="($charlength - 4) >= $framewidth">
1497 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1498  <m:mtr>
1499   <m:mtd>
1500    <m:mrow>
1501     <m:mo stretchy="false">(</m:mo>
1502     <xsl:apply-templates select="*[position()=2]">
1503      <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1504     </xsl:apply-templates>
1505    </m:mrow>
1506   </m:mtd>
1507  </m:mtr>
1508  <xsl:for-each select="*[position()>2]">
1509  <m:mtr>
1510   <m:mtd>
1511    <m:mrow>
1512     <m:mphantom stretchy="false"><m:mtext>(</m:mtext></m:mphantom>
1513     <xsl:apply-templates select=".">
1514      <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1515     </xsl:apply-templates>
1516    </m:mrow>
1517   </m:mtd>
1518  </m:mtr>
1519  </xsl:for-each>
1520  <m:mtr>
1521   <m:mtd>
1522    <m:mrow>
1523     <m:mo stretchy="false">)</m:mo>
1524    </m:mrow>
1525   </m:mtd>
1526  </m:mtr>
1527 </m:mtable>
1528 </xsl:when>
1529 <xsl:otherwise>
1530 <m:mo stretchy="false">(</m:mo>
1531 <xsl:apply-templates select="*[position()=2]">
1532  <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1533 </xsl:apply-templates>
1534 <xsl:for-each select="*[position()>2]">
1535  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1536  <xsl:apply-templates select=".">
1537   <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1538  </xsl:apply-templates>
1539 </xsl:for-each>
1540 <m:mo stretchy="false">)</m:mo>
1541 </xsl:otherwise>
1542 </xsl:choose>
1543 </xsl:when>
1544 <!-- CAST -->
1545 <xsl:when test="$name='cast'">
1546 <xsl:choose>
1547 <xsl:when test="$charlength >= $framewidth">
1548 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1549  <m:mtr>
1550   <m:mtd>
1551    <m:mrow>
1552     <m:mo stretchy="false">(</m:mo>
1553     <xsl:apply-templates select="*[position()=2]"/>
1554    </m:mrow>
1555   </m:mtd>
1556  </m:mtr>
1557  <m:mtr>
1558   <m:mtd>
1559    <m:mrow>
1560             <m:mo mathcolor="Maroon">:></m:mo>
1561             <xsl:apply-templates select="*[position()=3]"/>
1562            </m:mrow>
1563           </m:mtd>
1564          </m:mtr>
1565          <m:mtr>
1566           <m:mtd>
1567            <m:mrow>
1568             <m:mo stretchy="false">)</m:mo>
1569            </m:mrow>
1570           </m:mtd>
1571          </m:mtr>
1572         </m:mtable>
1573        </xsl:when>
1574        <xsl:otherwise>
1575         <m:mo stretchy="false">(</m:mo>
1576         <xsl:apply-templates select="*[position()=2]"/>
1577         <m:mo mathcolor="Maroon">:></m:mo>
1578         <xsl:apply-templates select="*[position()=3]"/>
1579         <m:mo stretchy="false">)</m:mo>
1580        </xsl:otherwise>
1581        </xsl:choose>
1582       </xsl:when>
1583       <!-- APP *-->
1584       <xsl:when test="$name='app'">
1585        <xsl:choose>
1586        <xsl:when test="$charlength >= $framewidth">
1587         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1588          <m:mtr>
1589           <m:mtd>
1590            <m:mrow>
1591             <m:mo stretchy="false">(</m:mo>
1592 <!-- added precedence to app = FUNCTION_PREC (99) -->
1593             <xsl:apply-templates select="*[position()=2]">
1594              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1595             </xsl:apply-templates>
1596            </m:mrow>
1597           </m:mtd>
1598          </m:mtr>
1599          <xsl:for-each select="*[position()>2]">
1600          <m:mtr>
1601           <m:mtd>
1602            <m:mrow>
1603             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
1604 <!-- added precedence to app = FUNCTION_PREC (99) -->
1605             <xsl:apply-templates select=".">
1606              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1607             </xsl:apply-templates>
1608            </m:mrow>
1609           </m:mtd>
1610          </m:mtr>
1611          </xsl:for-each>
1612          <m:mtr>
1613           <m:mtd>
1614            <m:mrow>
1615             <m:mo stretchy="false">)</m:mo>
1616            </m:mrow>
1617           </m:mtd>
1618          </m:mtr>
1619         </m:mtable>
1620        </xsl:when>
1621        <xsl:otherwise>
1622         <m:mo stretchy="false">(</m:mo>
1623 <!-- added precedence to app = FUNCTION_PREC (99) -->
1624         <xsl:apply-templates select="*[position()=2]">
1625          <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1626         </xsl:apply-templates>
1627         <xsl:for-each select="*[position()>2]">
1628          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1629 <!-- added precedence to app = FUNCTION_PREC (99) -->
1630          <xsl:apply-templates select=".">
1631           <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1632          </xsl:apply-templates>
1633         </xsl:for-each>
1634         <m:mo stretchy="false">)</m:mo>
1635        </xsl:otherwise>
1636        </xsl:choose>
1637       </xsl:when>
1638       <!-- CAST -->
1639       <xsl:when test="$name='cast'">
1640        <xsl:choose>
1641        <xsl:when test="$charlength >= $framewidth">
1642         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1643          <m:mtr>
1644           <m:mtd>
1645            <m:mrow>
1646             <m:mo stretchy="false">(</m:mo>
1647             <xsl:apply-templates select="*[position()=2]"/>
1648            </m:mrow>
1649           </m:mtd>
1650          </m:mtr>
1651          <m:mtr>
1652           <m:mtd>
1653            <m:mrow>
1654             <m:mo mathcolor="Maroon">:></m:mo>
1655             <xsl:apply-templates select="*[position()=3]"/>
1656            </m:mrow>
1657           </m:mtd>
1658          </m:mtr>
1659          <m:mtr>
1660           <m:mtd>
1661            <m:mrow>
1662             <m:mo stretchy="false">)</m:mo>
1663            </m:mrow>
1664           </m:mtd>
1665          </m:mtr>
1666         </m:mtable>
1667        </xsl:when>
1668        <xsl:otherwise>
1669         <m:mo stretchy="false">(</m:mo>
1670         <xsl:apply-templates select="*[position()=2]"/>
1671         <m:mo mathcolor="Maroon">:></m:mo>
1672         <xsl:apply-templates select="*[position()=3]"/>
1673         <m:mo stretchy="false">)</m:mo>
1674        </xsl:otherwise>
1675        </xsl:choose>
1676       </xsl:when>
1677       <!-- PROP -->
1678       <!--<xsl:when test="$name='Prop'">
1679        <m:mo>Prop</m:mo>
1680       </xsl:when>-->
1681       <!-- SET -->
1682       <!--<xsl:when test="$name='Set'">
1683        <m:mo>Set</m:mo>
1684       </xsl:when>-->
1685       <!-- TYPE -->
1686       <!--<xsl:when test="$name='Type'">
1687        <m:mo>Type</m:mo>
1688       </xsl:when>-->
1689       <!-- MUTCASE -->
1690       <xsl:when test="$name='mutcase'">
1691        <xsl:choose>
1692        <xsl:when test="$charlength >= $framewidth">
1693         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1694         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1695          <m:mtr>
1696           <m:mtd>
1697            <m:mrow>
1698             <m:mo>&lt;</m:mo>
1699             <xsl:apply-templates select="*[position()=2]"/>
1700             <xsl:if test="$framewidth > $charlength">
1701              <m:mo>&gt;</m:mo>
1702              <m:mo>CASES</m:mo>
1703              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1704              <xsl:apply-templates select="*[position()=3]"/>
1705             </xsl:if>
1706            </m:mrow>
1707           </m:mtd>
1708          </m:mtr>
1709          <xsl:if test="$charlength >= $framewidth">
1710          <m:mtr>
1711           <m:mtd>
1712            <m:mrow>
1713             <m:mo>&gt;</m:mo>
1714             <m:mo>CASES</m:mo>
1715             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1716             <xsl:apply-templates select="*[position()=3]"/>
1717            </m:mrow>
1718           </m:mtd>
1719          </m:mtr>
1720          </xsl:if>
1721          <m:mtr>
1722           <m:mtd>
1723            <m:mrow>
1724             <m:mo>OF</m:mo>
1725            </m:mrow>
1726           </m:mtd>
1727          </m:mtr>
1728          <xsl:for-each select="m:piecewise/m:piece">
1729          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1730          <m:mtr>
1731           <m:mtd>
1732            <m:mrow>
1733             <xsl:choose>
1734             <xsl:when test="position() = 1">
1735               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
1736             </xsl:when>
1737             <xsl:otherwise>
1738              <m:mo stretchy="false">|</m:mo>
1739             </xsl:otherwise>
1740             </xsl:choose>
1741             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1742             <xsl:apply-templates select="./*[2]"/>
1743             <xsl:if test="$framewidth > $charlength">
1744              <m:mo mathcolor="Green">&#x21d2;</m:mo>
1745              <xsl:apply-templates select="./*[1]"/>
1746             </xsl:if>
1747            </m:mrow>
1748           </m:mtd>
1749          </m:mtr>
1750          <xsl:if test="$charlength >= $framewidth">
1751          <m:mtr>
1752           <m:mtd>
1753            <m:mrow>
1754             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
1755             <m:mo mathcolor="Green">&#x21d2;</m:mo>
1756             <xsl:apply-templates select="./*[1]"/>
1757            </m:mrow>
1758           </m:mtd>
1759          </m:mtr>
1760          </xsl:if>
1761         </xsl:for-each>
1762          <m:mtr>
1763           <m:mtd>
1764            <m:mrow>
1765             <m:mo>END</m:mo>
1766            </m:mrow>
1767           </m:mtd>
1768          </m:mtr>
1769         </m:mtable>
1770        </xsl:when>
1771        <xsl:otherwise>
1772         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
1773         <m:mo>CASES</m:mo>
1774         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1775         <xsl:apply-templates select="*[position()=3]"/>
1776         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1777         <m:mo>OF</m:mo>
1778         <xsl:for-each select="m:piecewise/m:piece">
1779          <xsl:choose>
1780          <xsl:when test="position() != 1">
1781           <m:mo stretchy="false">|</m:mo>
1782          </xsl:when> 
1783          </xsl:choose>
1784          <xsl:apply-templates select="./*[2]"/>
1785          <m:mo mathcolor="Green">&#x21d2;</m:mo>
1786          <xsl:apply-templates select="./*[1]"/>
1787         </xsl:for-each>
1788         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1789         <m:mo>END</m:mo>
1790        </xsl:otherwise>
1791        </xsl:choose>
1792       </xsl:when>
1793       <!-- FIX -->
1794       <xsl:when test="$name='fix'">
1795        <xsl:choose>
1796        <xsl:when test="$charlength >= $framewidth">
1797         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1798          <m:mtr>
1799           <m:mtd>
1800            <m:mrow>
1801             <m:mo>FIX</m:mo>
1802             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1803             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1804             <m:mo stretchy="false">{</m:mo>
1805            </m:mrow>
1806           </m:mtd>
1807          </m:mtr>
1808          <m:mtr>
1809           <m:mtd>
1810            <m:mrow>
1811             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1812             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1813             <xsl:for-each select="m:bvar"> 
1814              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1815              <m:mtr>
1816               <m:mtd>
1817                <m:mrow>
1818                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1819                 <m:mo>:</m:mo>
1820                 <xsl:if test="$framewidth > $charlength">
1821                  <xsl:apply-templates select="m:type"/>
1822                 </xsl:if>
1823                </m:mrow>
1824               </m:mtd>
1825              </m:mtr> 
1826              <xsl:if test="$charlength >= $framewidth">
1827              <m:mtr>
1828               <m:mtd>
1829                <m:mrow>
1830                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
1831                 <xsl:apply-templates select="m:type"/>
1832                </m:mrow>
1833               </m:mtd>
1834              </m:mtr>
1835              </xsl:if>
1836              <m:mtr>
1837               <m:mtd>
1838                <m:mrow>
1839                 <m:mo>:=</m:mo>
1840                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1841                </m:mrow>
1842               </m:mtd>
1843              </m:mtr> 
1844             </xsl:for-each>
1845             </m:mtable>
1846            </m:mrow>
1847           </m:mtd>
1848          </m:mtr>
1849          <m:mtr>
1850           <m:mtd>
1851            <m:mrow>
1852             <m:mo stretchy="false">}</m:mo>
1853            </m:mrow>
1854           </m:mtd>
1855          </m:mtr>
1856         </m:mtable>
1857        </xsl:when>
1858        <xsl:otherwise>
1859         <m:mo>FIX</m:mo>
1860         <m:mi><xsl:value-of select="m:ci"/></m:mi>
1861         <m:mo stretchy="false">{</m:mo>
1862         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1863         <xsl:for-each select="m:bvar"> 
1864          <m:mtr>
1865           <m:mtd>
1866            <m:mrow>
1867             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1868             <m:mo>:</m:mo>
1869             <xsl:apply-templates select="m:type"/>
1870             <m:mo>:=</m:mo>
1871             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1872             <xsl:if test="position()=last()">
1873              <m:mo stretchy="false">}</m:mo>
1874             </xsl:if>
1875            </m:mrow>
1876           </m:mtd>
1877          </m:mtr>
1878          </xsl:for-each>
1879         </m:mtable>
1880        </xsl:otherwise>
1881        </xsl:choose>
1882       </xsl:when>
1883       <!-- COFIX -->
1884       <xsl:when test="$name='cofix'">
1885        <xsl:choose>
1886        <xsl:when test="$charlength >= $framewidth">
1887         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1888          <m:mtr>
1889           <m:mtd>
1890            <m:mrow>
1891             <m:mo>COFIX</m:mo>
1892             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1893             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1894             <m:mo stretchy="false">{</m:mo>
1895            </m:mrow>
1896           </m:mtd>
1897          </m:mtr>
1898          <m:mtr>
1899           <m:mtd>
1900            <m:mrow>
1901             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1902             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1903             <xsl:for-each select="m:bvar">
1904              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable> 
1905              <m:mtr>
1906               <m:mtd>
1907                <m:mrow>
1908                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1909                 <m:mo>:</m:mo>
1910                 <xsl:if test="$framewidth > $charlength">
1911                  <xsl:apply-templates select="m:type"/>
1912                 </xsl:if>
1913                </m:mrow>
1914               </m:mtd>
1915              </m:mtr> 
1916              <xsl:if test="$charlength >= $framewidth">
1917              <m:mtr>
1918               <m:mtd>
1919                <m:mrow>
1920                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
1921                 <xsl:apply-templates select="m:type"/>
1922                </m:mrow>
1923               </m:mtd>
1924              </m:mtr>
1925              </xsl:if>
1926              <m:mtr>
1927               <m:mtd>
1928                <m:mrow>
1929                 <m:mo>:=</m:mo>
1930                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1931                </m:mrow>
1932               </m:mtd>
1933              </m:mtr>
1934             </xsl:for-each>
1935             </m:mtable>
1936            </m:mrow>
1937           </m:mtd>
1938          </m:mtr>
1939          <m:mtr>
1940           <m:mtd>
1941            <m:mrow>
1942             <m:mo stretchy="false">}</m:mo>
1943            </m:mrow>
1944           </m:mtd>
1945          </m:mtr>
1946         </m:mtable>
1947        </xsl:when>
1948        <xsl:otherwise>
1949         <m:mo>COFIX</m:mo>
1950         <m:mi><xsl:value-of select="m:ci"/></m:mi>
1951         <m:mo stretchy="false">{</m:mo>
1952         <m:mtable align="baseline 1" equalrows="false" columnalign="left">  
1953         <xsl:for-each select="m:bvar"> 
1954          <m:mtr>
1955           <m:mtd>
1956            <m:mrow>
1957             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1958             <m:mo>:</m:mo>
1959             <xsl:apply-templates select="m:type"/>
1960             <m:mo>:=</m:mo>
1961             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1962             <xsl:if test="position()=last()">
1963              <m:mo stretchy="false">}</m:mo>
1964             </xsl:if>
1965            </m:mrow>
1966           </m:mtd>
1967          </m:mtr>
1968          </xsl:for-each>
1969         </m:mtable>
1970        </xsl:otherwise>
1971        </xsl:choose>
1972       </xsl:when>
1973       <!-- ***************************************** -->
1974       <!-- *********** PROOF ELEMENTS ************** -->
1975       <!-- ***************************************** -->
1976       <!-- PROOF -->
1977       <xsl:when test="$name='proof'">
1978         <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
1979         <xsl:variable name="test" select="(not($explodeall)) and
1980            (not(preceding-sibling::*[1]/text()='letin1')) and
1981            (not(preceding-sibling::*[1]/text()='rw_step')) and
1982            (not(name(..)='m:lambda'))"/>
1983         <xsl:variable name="hidden_details">
1984          <xsl:if test="$test">
1985           <!-- Details hided (default) -->
1986           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1987            <m:mtr>
1988             <m:mtd>
1989              <m:mrow>
1990               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
1991               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1992               <!-- the last child is either the expected type, if provided,-->
1993               <!-- or the synthesized type.                                -->
1994               <xsl:apply-templates select="*[position()=last()]"/>
1995               <m:mrow>
1996                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1997                <m:mtext mathcolor="Green">(explain)</m:mtext>
1998               </m:mrow>
1999              </m:mrow>
2000             </m:mtd>
2001            </m:mtr>
2002           </m:mtable>
2003          </xsl:if>
2004         </xsl:variable>
2005         <xsl:variable name="shown_details">
2006          <!-- Show details -->
2007          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2008           <m:mtr>
2009            <m:mtd>
2010             <m:mrow>
2011              <xsl:apply-templates select="*[position()=2]"/>
2012             </m:mrow>
2013            </m:mtd>
2014           </m:mtr>
2015           <xsl:variable name="hidedetails">
2016             <m:mrow>
2017              <m:mphantom>
2018               <m:mtext>_</m:mtext>
2019              </m:mphantom>
2020              <xsl:if test="$test">
2021               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
2022              </xsl:if>
2023             </m:mrow>
2024           </xsl:variable>
2025           <m:mtr>
2026            <m:mtd>
2027             <m:mrow>
2028              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
2029              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2030              <xsl:apply-templates select="*[position()=3]"/>
2031              <xsl:if test="not(*[4])">
2032               <xsl:copy-of select="$hidedetails"/>
2033              </xsl:if>
2034             </m:mrow>
2035            </m:mtd>
2036           </m:mtr>
2037           <xsl:if test="*[4]">
2038            <m:mtr>
2039             <m:mtd>
2040              <m:mrow>
2041               <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
2042               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2043               <xsl:apply-templates select="*[position()=4]"/>
2044               <xsl:copy-of select="$hidedetails"/>
2045              </m:mrow>
2046             </m:mtd>
2047            </m:mtr>
2048           </xsl:if>
2049          </m:mtable>
2050         </xsl:variable>
2051         <xsl:choose>
2052          <xsl:when test="$test">
2053           <m:maction actiontype="toggle">
2054            <xsl:copy-of select="$hidden_details"/>
2055            <xsl:copy-of select="$shown_details"/>
2056           </m:maction>
2057          </xsl:when>
2058          <xsl:otherwise>
2059           <xsl:copy-of select="$shown_details"/>
2060          </xsl:otherwise>
2061         </xsl:choose>
2062       </xsl:when>
2063       <!-- SIDE_PROOF -->
2064       <xsl:when test="$name='side_proof'">
2065         <xsl:variable name="test" select="(not($explodeall))"/>
2066         <xsl:variable name="hidden_details">
2067          <xsl:if test="$test">
2068           <!-- Details hided (default) -->
2069           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2070            <m:mtr>
2071             <m:mtd>
2072              <m:mrow>
2073               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
2074               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2075               <!-- the last child is either the expected type, if provided,-->
2076               <!-- or the synthesized type.                                -->
2077               <xsl:apply-templates select="*[position()=last()]"/>
2078               <m:mrow>
2079                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2080                <m:mtext mathcolor="Green">(explain)</m:mtext>
2081               </m:mrow>
2082              </m:mrow>
2083             </m:mtd>
2084            </m:mtr>
2085           </m:mtable>
2086          </xsl:if>
2087         </xsl:variable>
2088         <xsl:variable name="shown_details">
2089          <!-- Show details -->
2090          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2091           <m:mtr>
2092            <m:mtd>
2093             <m:mrow>
2094              <xsl:apply-templates select="*[position()=2]"/>
2095             </m:mrow>
2096            </m:mtd>
2097           </m:mtr>
2098           <xsl:variable name="hidedetails">
2099             <m:mrow>
2100              <m:mphantom>
2101               <m:mtext>_</m:mtext>
2102              </m:mphantom>
2103              <xsl:if test="$test">
2104               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
2105              </xsl:if>
2106             </m:mrow>
2107           </xsl:variable>
2108           <m:mtr>
2109            <m:mtd>
2110             <m:mrow>
2111              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
2112              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2113              <xsl:apply-templates select="*[position()=3]"/>
2114              <xsl:if test="not(*[4])">
2115               <xsl:copy-of select="$hidedetails"/>
2116              </xsl:if>
2117             </m:mrow>
2118            </m:mtd>
2119           </m:mtr>
2120           <xsl:if test="*[4]">
2121            <m:mtr>
2122             <m:mtd>
2123              <m:mrow>
2124               <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
2125               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2126               <xsl:apply-templates select="*[position()=4]"/>
2127               <xsl:copy-of select="$hidedetails"/>
2128              </m:mrow>
2129             </m:mtd>
2130            </m:mtr>
2131           </xsl:if>
2132          </m:mtable>
2133         </xsl:variable>
2134         <xsl:choose>
2135          <xsl:when test="$test">
2136           <m:maction actiontype="toggle">
2137            <xsl:copy-of select="$hidden_details"/>
2138            <xsl:copy-of select="$shown_details"/>
2139           </m:maction>
2140          </xsl:when>
2141          <xsl:otherwise>
2142           <xsl:copy-of select="$shown_details"/>
2143          </xsl:otherwise>
2144         </xsl:choose>
2145       </xsl:when>
2146       <!-- LETIN1 -->
2147       <xsl:when test="$name='letin1'">
2148         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2149          <m:mtr>
2150           <m:mtd>
2151            <m:mrow>
2152             <xsl:apply-templates select="*[position()=2]"/>
2153            </m:mrow>
2154           </m:mtd>
2155          </m:mtr>
2156          <m:mtr>
2157           <m:mtd>
2158            <m:mrow>
2159             <xsl:apply-templates select="*[position()=3]"/>
2160            </m:mrow>
2161           </m:mtd>
2162          </m:mtr>
2163         </m:mtable>
2164       </xsl:when>
2165       <xsl:when test="$name='by_induction'">
2166        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2167         <m:mtr>
2168          <m:mtd>
2169           <m:mrow>
2170            <m:mtext mathcolor="Red">We&#x00a0;prove</m:mtext>
2171            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2172            <xsl:apply-templates select="../*[3]"/>
2173           </m:mrow>
2174          </m:mtd>
2175         </m:mtr>
2176         <m:mtr>
2177          <m:mtd>
2178           <m:mrow>
2179            <m:mtext mathcolor="Red">by&#x00a0;induction&#x00a0;on</m:mtext>
2180            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2181            <xsl:apply-templates 
2182             select="*[position()=last()]/*[position()=last()]"/>
2183           </m:mrow>
2184          </m:mtd>
2185         </m:mtr>
2186         <m:mtr>
2187          <m:mtd>
2188           <m:mrow>
2189            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2190             <xsl:for-each select="*[position()>3 and not(position()=last())]">
2191              <m:mtr>
2192               <m:mtd>
2193                <m:mrow>
2194                 <xsl:apply-templates select="."/>
2195                </m:mrow>
2196               </m:mtd>
2197              </m:mtr>
2198             </xsl:for-each>
2199            </m:mtable>
2200           </m:mrow>
2201          </m:mtd>
2202         </m:mtr>
2203        </m:mtable>
2204       </xsl:when>
2205       <!-- inductive_case -->
2206       <xsl:when test="$name='inductive_case'">
2207        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2208         <m:mtr>
2209          <m:mtd>
2210           <m:mrow>
2211            <m:mtext mathcolor="Red">Case</m:mtext>
2212            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2213            <xsl:apply-templates select="*[2]"/>
2214           </m:mrow>
2215          </m:mtd>
2216         </m:mtr>
2217         <m:mtr>
2218          <m:mtd>
2219           <m:mrow>
2220            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2221            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2222             <xsl:if test="*[3]/*[position()>1]">
2223              <m:mtr>
2224               <m:mtd>
2225                <m:mrow>
2226                 <m:mtext mathcolor="Red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
2227                </m:mrow>
2228               </m:mtd>
2229              </m:mtr>
2230              <m:mtr>
2231               <m:mtd>
2232                <m:mrow>
2233                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2234                 <xsl:for-each select="*[3]/*[position()>1]">
2235                  <m:mo stretchy="false">(</m:mo>
2236                  <xsl:apply-templates select="m:ci"/>
2237                  <m:mo stretchy="false">) </m:mo>
2238                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2239                  <xsl:apply-templates select="m:type"/>
2240                 </xsl:for-each>
2241                </m:mrow>
2242               </m:mtd>
2243              </m:mtr>
2244             </xsl:if>
2245             <m:mtr>
2246              <m:mtd>
2247               <m:mrow>
2248                <xsl:apply-templates select="*[4]"/>
2249               </m:mrow>
2250              </m:mtd>
2251             </m:mtr>
2252            </m:mtable>
2253           </m:mrow>
2254          </m:mtd>
2255         </m:mtr>
2256        </m:mtable>
2257       </xsl:when>
2258       <!-- case_lhs  -->
2259       <xsl:when test="$name='case_lhs'">
2260        <m:mrow>
2261         <xsl:choose>
2262          <xsl:when test="count(*)=2">
2263           <xsl:apply-templates select="*[2]"/>
2264          </xsl:when>
2265          <xsl:otherwise>
2266           <m:mo stretchy="false">(</m:mo>
2267           <xsl:apply-templates select="*[2]"/>
2268           <xsl:for-each select="m:bvar">
2269            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2270            <xsl:apply-templates select="*[1]"/>
2271            <m:mtext>:</m:mtext>
2272            <xsl:apply-templates select="m:type/*[1]"/>
2273           </xsl:for-each>
2274           <m:mo stretchy="false">)</m:mo>
2275          </xsl:otherwise>
2276         </xsl:choose>
2277        </m:mrow>
2278       </xsl:when>
2279       <!-- false_ind  -->
2280       <xsl:when test="$name='false_ind'">
2281        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2282         <m:mtr>
2283          <m:mtd>
2284           <m:mrow>
2285            <xsl:apply-templates select="*[3]"/>
2286           </m:mrow>
2287          </m:mtd>
2288         </m:mtr>
2289         <m:mtr>
2290          <m:mtd>
2291           <m:mrow>
2292            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
2293           </m:mrow>
2294          </m:mtd>
2295         </m:mtr>
2296        </m:mtable>
2297       </xsl:when>
2298       <!-- LET-IN -->
2299       <xsl:when test="$name='letin'">
2300         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2301          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
2302          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
2303          <m:mtr>
2304           <m:mtd>
2305            <m:mrow>
2306             <xsl:apply-templates select="."/>
2307            </m:mrow>
2308           </m:mtd>
2309          </m:mtr>
2310          </xsl:for-each>
2311          <m:mtr>
2312           <m:mtd>
2313            <m:mrow>
2314             <xsl:apply-templates select="*[position()=last()]"/>
2315            </m:mrow>
2316           </m:mtd>
2317          </m:mtr>
2318         </m:mtable>
2319       </xsl:when>
2320       <!-- LET -->
2321       <xsl:when test="$name='let'">
2322        <m:mtext>(</m:mtext>
2323        <xsl:apply-templates select="m:ci"/>
2324        <m:mtext>) </m:mtext>
2325        <xsl:apply-templates select="*[3]"/>
2326       </xsl:when>
2327       <!-- RW_STEP -->
2328       <xsl:when test="$name='rw_step'">
2329         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2330          <m:mtr>
2331           <m:mtd>
2332            <m:mrow>
2333             <xsl:choose>
2334              <xsl:when test="name(*[2])='m:apply'">
2335               <xsl:apply-templates select="*[2]"/>
2336              </xsl:when>
2337              <xsl:otherwise>
2338               <m:mtext>Consider</m:mtext>
2339               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2340               <xsl:apply-templates select="*[2]"/>
2341              </xsl:otherwise>
2342             </xsl:choose>
2343            </m:mrow>
2344           </m:mtd>
2345          </m:mtr>
2346          <m:mtr>
2347           <m:mtd>
2348            <m:mrow>
2349             <m:mtext>Rewrite</m:mtext>
2350             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2351             <xsl:apply-templates select="*[3]"/>
2352             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2353             <m:mtext>with</m:mtext>
2354             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2355             <xsl:apply-templates select="*[4]"/>
2356             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2357             <m:mtext>by</m:mtext>
2358             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2359             <xsl:apply-templates select="*[5]"/>
2360            </m:mrow>
2361           </m:mtd>
2362          </m:mtr>
2363         </m:mtable>
2364       </xsl:when>
2365       <!-- not existing any more
2366       <xsl:when test="$name='thread'">
2367         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2368          <m:mtr>
2369           <m:mtd>
2370            <m:mrow>
2371             <xsl:choose>
2372              <xsl:when test="name(*[last()])='m:apply'">
2373               <xsl:apply-templates select="*[last()]"/>
2374              </xsl:when>
2375              <xsl:otherwise>
2376               <m:mtext>Consider</m:mtext>
2377               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2378               <xsl:apply-templates select="*[last()]"/>
2379              </xsl:otherwise>
2380             </xsl:choose>
2381            </m:mrow>
2382           </m:mtd>
2383          </m:mtr>
2384          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
2385         </m:mtable>
2386       </xsl:when>
2387       --> 
2388       <!-- REWRITE_AND_APPLY -->
2389       <xsl:when test="$name='rewrite_and_apply'">
2390         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2391          <m:mtr>
2392           <m:mtd>
2393            <m:mrow>
2394             <xsl:apply-templates select="*[2]"/>
2395            </m:mrow>
2396           </m:mtd>
2397          </m:mtr>
2398          <m:mtr>
2399           <m:mtd>
2400            <m:mrow>
2401             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
2402             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2403             <xsl:apply-templates select="*[position()>2]"/>
2404            </m:mrow>
2405           </m:mtd>
2406          </m:mtr>
2407        </m:mtable>
2408       </xsl:when>
2409       <!-- AND_IND -->
2410       <xsl:when test="$name='and_ind'">
2411         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2412          <m:mtr>
2413           <m:mtd>
2414            <m:mrow>
2415             <xsl:choose>
2416              <xsl:when test="name(*[2])='m:apply'">
2417               <xsl:apply-templates select="*[2]"/>
2418              </xsl:when>
2419              <xsl:otherwise>
2420               <m:mtext>Consider</m:mtext>
2421               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2422               <xsl:apply-templates select="*[2]"/>
2423              </xsl:otherwise>
2424             </xsl:choose>
2425            </m:mrow>
2426           </m:mtd>
2427          </m:mtr>
2428          <m:mtr>
2429           <m:mtd>
2430            <m:mrow>
2431             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
2432            </m:mrow>
2433           </m:mtd>
2434          </m:mtr>
2435          <m:mtr>
2436           <m:mtd>
2437            <m:mrow>
2438             <m:mtext>(</m:mtext>
2439             <xsl:apply-templates select="*[3]"/>
2440             <m:mtext>)</m:mtext>
2441             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2442             <xsl:apply-templates select="*[4]"/>
2443             </m:mrow>
2444           </m:mtd>
2445          </m:mtr>
2446          <m:mtr>
2447           <m:mtd>
2448            <m:mrow>
2449             <m:mtext>(</m:mtext>
2450             <xsl:apply-templates select="*[5]"/>
2451             <m:mtext>)</m:mtext>
2452             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2453             <xsl:apply-templates select="*[6]"/>
2454             </m:mrow>
2455           </m:mtd>
2456          </m:mtr>
2457          <m:mtr>
2458           <m:mtd>
2459            <m:mrow>
2460             <xsl:apply-templates select="*[7]"/>
2461            </m:mrow>
2462           </m:mtd>
2463          </m:mtr>
2464         </m:mtable>
2465       </xsl:when>
2466       <!-- full_or_ind -->
2467       <xsl:when test="$name='full_or_ind'">
2468         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2469          <m:mtr>
2470           <m:mtd>
2471            <m:mrow>
2472             <xsl:choose>
2473              <xsl:when test="name(*[2])='m:apply'">
2474               <xsl:apply-templates select="*[2]"/>
2475              </xsl:when>
2476              <xsl:otherwise>
2477               <m:mtext>Consider</m:mtext>
2478               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2479               <xsl:apply-templates select="*[2]"/>
2480              </xsl:otherwise>
2481             </xsl:choose>
2482            </m:mrow>
2483           </m:mtd>
2484          </m:mtr>
2485          <m:mtr>
2486           <m:mtd>
2487            <m:mrow>
2488             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
2489             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2490             <xsl:apply-templates select="*[3]"/>
2491            </m:mrow>
2492           </m:mtd>
2493          </m:mtr>
2494          <m:mtr>
2495           <m:mtd>
2496            <m:mrow>
2497             <m:mtext>Left:&#x00a0;suppose</m:mtext>
2498             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2499             <m:mo stretchy="false">(</m:mo>
2500             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
2501             <m:mo stretchy="false">)</m:mo>
2502             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2503             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
2504            </m:mrow>
2505           </m:mtd>
2506          </m:mtr>
2507          <m:mtr>
2508           <m:mtd>
2509            <m:mrow>
2510             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2511             <xsl:apply-templates select="*[4]/*[3]"/>
2512            </m:mrow>
2513           </m:mtd>
2514          </m:mtr>
2515          <m:mtr>
2516           <m:mtd>
2517            <m:mrow>
2518             <m:mtext>Right:&#x00a0;suppose</m:mtext>
2519             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2520             <m:mo stretchy="false">(</m:mo>
2521             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
2522             <m:mo stretchy="false">)</m:mo>
2523             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2524             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
2525            </m:mrow>
2526           </m:mtd>
2527          </m:mtr>
2528          <m:mtr>
2529           <m:mtd>
2530            <m:mrow>
2531             <xsl:apply-templates select="*[5]/*[3]"/>
2532            </m:mrow>
2533           </m:mtd>
2534          </m:mtr>
2535         </m:mtable>
2536       </xsl:when>
2537       <!-- OR_IND -->
2538       <xsl:when test="$name='or_ind'">
2539         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2540          <m:mtr>
2541           <m:mtd>
2542            <m:mrow>
2543             <xsl:choose>
2544              <xsl:when test="name(*[2])='m:apply'">
2545               <xsl:apply-templates select="*[2]"/>
2546              </xsl:when>
2547              <xsl:otherwise>
2548               <m:mtext>Consider</m:mtext>
2549               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2550               <xsl:apply-templates select="*[2]"/>
2551              </xsl:otherwise>
2552             </xsl:choose>
2553            </m:mrow>
2554           </m:mtd>
2555          </m:mtr>
2556          <m:mtr>
2557           <m:mtd>
2558            <m:mrow>
2559             <m:mtext>We&#x00a0;prove</m:mtext>
2560             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2561             <xsl:apply-templates select="*[3]"/>
2562             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2563             <m:mtext>by&#x00a0;cases:</m:mtext>
2564            </m:mrow>
2565           </m:mtd>
2566          </m:mtr>
2567          <m:mtr>
2568           <m:mtd>
2569            <m:mrow>
2570             <m:mtext>Left</m:mtext>
2571             <xsl:apply-templates select="*[4]"/>
2572            </m:mrow>
2573           </m:mtd>
2574          </m:mtr>
2575          <m:mtr>
2576           <m:mtd>
2577            <m:mrow>
2578             <m:mtext>Right</m:mtext>
2579             <xsl:apply-templates select="*[5]"/>
2580            </m:mrow>
2581           </m:mtd>
2582          </m:mtr>
2583         </m:mtable>
2584       </xsl:when>
2585       <!-- EX_IND -->
2586       <xsl:when test="$name='ex_ind'">
2587         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2588          <m:mtr>
2589           <m:mtd>
2590            <m:mrow>
2591             <xsl:choose>
2592              <xsl:when test="name(*[2])='m:apply'">
2593               <xsl:apply-templates select="*[2]"/>
2594              </xsl:when>
2595              <xsl:otherwise>
2596               <m:mtext>Consider</m:mtext>
2597               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2598               <xsl:apply-templates select="*[2]"/>
2599              </xsl:otherwise>
2600             </xsl:choose>
2601            </m:mrow>
2602           </m:mtd>
2603          </m:mtr>
2604          <m:mtr>
2605           <m:mtd>
2606            <m:mrow>
2607             <m:mtext>Let</m:mtext>
2608             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2609             <xsl:apply-templates select="*[3]"/>
2610             <m:mtext>:</m:mtext>
2611             <xsl:apply-templates select="*[4]"/>
2612             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2613             <m:mtext>such&#x00a0;that</m:mtext>
2614             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2615             <m:mtext>(</m:mtext>
2616              <xsl:apply-templates select="*[5]"/>
2617             <m:mtext>)</m:mtext>
2618             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2619             <xsl:apply-templates select="*[6]"/>
2620            </m:mrow>
2621           </m:mtd>
2622          </m:mtr>
2623          <m:mtr>
2624           <m:mtd>
2625            <m:mrow>
2626             <xsl:apply-templates select="*[7]"/>
2627            </m:mrow>
2628           </m:mtd>
2629          </m:mtr>
2630         </m:mtable>
2631       </xsl:when>
2632       <!-- EQ_CHAIN -->
2633       <xsl:when test="$name='eq_chain'">
2634        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2635         <m:mtr>
2636          <m:mtd>
2637           <m:mrow>
2638            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;equality&#x00a0;chain:</m:mtext>
2639           </m:mrow>
2640          </m:mtd>
2641         </m:mtr>
2642         <xsl:for-each select="*[position() mod 2 = 0]">
2643         <xsl:variable name="pos" select="position()"/>
2644         <m:mtr>
2645          <m:mtd>
2646           <m:mrow>
2647            <xsl:choose>
2648            <xsl:when test="$pos = 1">
2649             <xsl:apply-templates select="."/>
2650             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2651             <m:mo>=</m:mo>
2652            </xsl:when>
2653            <xsl:otherwise>
2654             <m:mo>=</m:mo>
2655             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2656             <xsl:apply-templates select="."/>
2657            </xsl:otherwise>
2658            </xsl:choose>
2659           </m:mrow>
2660          </m:mtd>
2661         </m:mtr>
2662         <xsl:if test="$pos != last()">
2663         <m:mtr>
2664          <m:mtd>
2665           <m:mrow>
2666            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
2667            <xsl:apply-templates select="../*[position()=2*$pos +1]"/>
2668           </m:mrow>
2669          </m:mtd>
2670         </m:mtr>
2671         </xsl:if>
2672         </xsl:for-each>
2673        </m:mtable>
2674       </xsl:when>
2675       <!-- DISEQ_CHAIN -->
2676       <xsl:when test="$name='diseq_chain'">
2677        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2678         <m:mtr>
2679          <m:mtd>
2680           <m:mrow>
2681            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;disequality&#x00a0;chain:</m:mtext>
2682           </m:mrow>
2683          </m:mtd>
2684         </m:mtr>
2685         <xsl:for-each select="*[position() mod 3 = 2]">
2686         <xsl:variable name="pos" select="position()"/>
2687         <m:mtr>
2688          <m:mtd>
2689           <m:mrow>
2690            <xsl:choose>
2691            <xsl:when test="$pos = 1">
2692             <xsl:apply-templates select="."/>
2693             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2694             <mo><xsl:apply-templates select="../*[position()=3*$pos]"/></mo>
2695            </xsl:when>
2696            <xsl:otherwise>
2697             <mo><xsl:apply-templates select="../*[position()=3*($pos - 1)]"/></mo>
2698             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2699             <xsl:apply-templates select="."/>
2700            </xsl:otherwise>
2701            </xsl:choose>
2702           </m:mrow>
2703          </m:mtd>
2704         </m:mtr>
2705         <xsl:if test="$pos != last()">
2706         <m:mtr>
2707          <m:mtd>
2708           <m:mrow>
2709            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
2710            <xsl:apply-templates select="../*[position()=3*$pos +1]"/>
2711           </m:mrow>
2712          </m:mtd>
2713         </m:mtr>
2714         </xsl:if>
2715         </xsl:for-each>
2716        </m:mtable>
2717       </xsl:when>
2718       <!-- ***************************************** -->
2719       <!-- *********** NOTATIONS ******************* -->
2720       <!-- ***************************************** -->
2721       <!-- subst -->
2722       <xsl:when test="$name='subst'">
2723         <xsl:apply-templates select="*[3]"/>
2724 <!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
2725         <m:mo stretchy="false">[</m:mo>
2726         <xsl:apply-templates select="*[4]"/>
2727         <m:mo mathcolor="Green">
2728          <xsl:if test="$id != ''">
2729           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2730          </xsl:if>&#8592;</m:mo>
2731         <xsl:apply-templates select="*[2]"/>
2732         <m:mo stretchy="false">]</m:mo>
2733       </xsl:when>
2734       <!-- lift -->
2735       <xsl:when test="$name='lift'">
2736         <m:msup>
2737          <m:mo mathcolor="Green">
2738           <xsl:if test="$id != ''">
2739            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2740           </xsl:if>&#8593;</m:mo>
2741          <xsl:apply-templates select="*[2]"/>
2742         </m:msup>
2743         <m:mrow>
2744          <m:mo stretchy="false">(</m:mo>
2745          <xsl:apply-templates select="*[3]"/>
2746          <m:mo stretchy="false">)</m:mo>
2747         </m:mrow>
2748       </xsl:when>
2749       <!-- lift_with_base -->
2750       <xsl:when test="$name='lift_with_base'">
2751         <m:msubsup>
2752          <m:mo mathcolor="Green">
2753           <xsl:if test="$id != ''">
2754            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2755           </xsl:if>&#8593;</m:mo>
2756          <xsl:apply-templates select="*[3]"/>
2757          <xsl:apply-templates select="*[4]"/>
2758         </m:msubsup>
2759         <m:mrow>
2760          <m:mo stretchy="false">(</m:mo>
2761          <xsl:apply-templates select="*[2]"/>
2762          <m:mo stretchy="false">)</m:mo>
2763         </m:mrow>       
2764       </xsl:when>
2765       <!-- beta_red1 -->
2766       <xsl:when test="$name='beta_red1'">
2767         <xsl:apply-templates select="*[2]"/>
2768         <m:munder>
2769          <m:mo mathcolor="Green">
2770           <xsl:if test="$id != ''">
2771            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2772           </xsl:if>&#8594;</m:mo>
2773           <m:mi mathcolor="Green">&#946;</m:mi>
2774         </m:munder>
2775         <xsl:apply-templates select="*[3]"/>
2776       </xsl:when>
2777       <!-- beta_red -->
2778       <xsl:when test="$name='beta_red'">
2779         <xsl:apply-templates select="*[2]"/>
2780         <m:munderover>
2781          <m:mo mathcolor="Green">
2782           <xsl:if test="$id != ''">
2783            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2784           </xsl:if>&#8594;</m:mo>
2785           <m:mi mathcolor="Green">&#946;</m:mi>
2786           <m:mi mathcolor="Green">*</m:mi>
2787         </m:munderover>
2788         <xsl:apply-templates select="*[3]"/>
2789       </xsl:when>
2790       <!-- par_beta_red1 -->
2791       <xsl:when test="$name='par_beta_red1'">
2792         <xsl:apply-templates select="*[2]"/>
2793         <m:munder>
2794          <m:mo mathcolor="Green">
2795           <xsl:if test="$id != ''">
2796            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2797           </xsl:if>&#8658;</m:mo>
2798           <m:mi mathcolor="Green">&#946;</m:mi>
2799         </m:munder>
2800         <xsl:apply-templates select="*[3]"/>
2801       </xsl:when>
2802       <!-- par_beta_red -->
2803       <xsl:when test="$name='par_beta_red'">
2804         <xsl:apply-templates select="*[2]"/>
2805         <m:munderover>
2806          <m:mo mathcolor="Green">
2807           <xsl:if test="$id != ''">
2808            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2809           </xsl:if>&#8658;</m:mo>
2810           <m:mi mathcolor="Green">&#946;</m:mi>
2811           <m:mi mathcolor="Green">*</m:mi>
2812         </m:munderover>
2813         <xsl:apply-templates select="*[3]"/>
2814       </xsl:when>
2815       <!-- forgetful -->
2816       <xsl:when test="$name='forgetful'">
2817        <m:mfenced open="|" close="|">
2818         <xsl:if test="$id != ''">
2819          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2820         </xsl:if>
2821         <xsl:apply-templates select="*[2]"/>
2822        </m:mfenced>
2823       </xsl:when>
2824       <!-- isomorphic -->
2825       <xsl:when test="$name='isomorphic'">
2826         <xsl:apply-templates select="*[2]"/>
2827         <m:mo mathcolor="Green">
2828          <xsl:if test="$id != ''">
2829           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2830          </xsl:if>&#8773;</m:mo>
2831         <xsl:apply-templates select="*[3]"/>
2832       </xsl:when>
2833       <!-- interp -->
2834       <xsl:when test="$name='forgetful'">
2835        <m:mfenced open="[" close="]">
2836         <xsl:if test="$id != ''">
2837          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2838         </xsl:if>
2839         <xsl:apply-templates select="*[2]"/>
2840        </m:mfenced>
2841       </xsl:when> 
2842
2843       <!-- ERROR -->
2844       <xsl:otherwise>
2845        <m:mi>ERROR</m:mi>
2846       </xsl:otherwise>
2847      </xsl:choose>
2848     </m:mrow>
2849 </xsl:template>
2850
2851 <!-- Il modo Thread non esiste piu' 
2852 <xsl:template match="*" mode="thread">
2853  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
2854  <xsl:choose>
2855   <xsl:when test="$name='rw_step'">
2856          <m:mtr>
2857           <m:mtd>
2858            <m:mrow>
2859             <m:mtext>Rewrite</m:mtext>
2860             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2861             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
2862             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2863             <m:mtext>with</m:mtext>
2864             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2865             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
2866             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2867             <m:mtext>by</m:mtext>
2868             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2869             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
2870            </m:mrow>
2871           </m:mtd>
2872          </m:mtr>
2873          <m:mtr>
2874           <m:mtd>
2875            <m:mrow>
2876             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
2877             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2878             <xsl:apply-templates select="."/>
2879            </m:mrow>
2880           </m:mtd>
2881          </m:mtr>
2882    </xsl:when>
2883    <xsl:otherwise>
2884          <m:mtr>
2885           <m:mtd>
2886            <m:mrow>
2887             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
2888            </m:mrow>
2889           </m:mtd>
2890          </m:mtr>
2891          <m:mtr>
2892           <m:mtd>
2893            <m:mrow>
2894             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
2895             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2896             <xsl:apply-templates select="."/>
2897            </m:mrow>
2898           </m:mtd>
2899          </m:mtr>
2900     </xsl:otherwise>
2901    </xsl:choose>
2902          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
2903 </xsl:template>
2904 -->
2905
2906 <!-- LAMBDA -->
2907
2908 <xsl:template match="m:lambda">
2909     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
2910     <m:mrow>
2911      <xsl:if test="@id">
2912       <xsl:attribute name="xref">
2913        <xsl:value-of select="@id"/>
2914       </xsl:attribute>
2915      </xsl:if>
2916      <xsl:choose>
2917      <xsl:when test="$charlength >= $framewidth">
2918       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2919         <m:mtr>
2920           <m:mtd>
2921            <m:mrow>
2922             <m:mo mathcolor="Red">&#x03bb;</m:mo>
2923             <!--<xsl:apply-templates select="m:bvar"/>-->
2924             <xsl:apply-templates select="m:bvar/m:ci"/>
2925            </m:mrow>
2926           </m:mtd>
2927          </m:mtr>
2928        <m:mtr>
2929         <m:mtd>
2930          <m:mrow>
2931           <m:mo>.</m:mo>
2932           <xsl:apply-templates select="*[position()=2]"/>
2933          </m:mrow>
2934         </m:mtd>
2935        </m:mtr>
2936       </m:mtable>
2937      </xsl:when>
2938      <xsl:otherwise>
2939       <m:mo mathcolor="Red">&#x03bb;</m:mo>
2940       <!--<xsl:apply-templates select="m:bvar/m:ci"/>
2941       <m:mo>:</m:mo>
2942       <xsl:apply-templates select="m:bvar/m:type"/>-->
2943       <xsl:apply-templates select="m:bvar/m:ci"/>
2944       <m:mo>.</m:mo>
2945       <xsl:apply-templates select="*[position()=2]"/>
2946      </xsl:otherwise>
2947      </xsl:choose>
2948     </m:mrow>
2949 </xsl:template>
2950
2951
2952 <!--**********************-->
2953 <!--       COUNTING       -->
2954 <!--**********************-->
2955
2956 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
2957  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
2958  |m:plus|m:minus|m:times" mode="charcount">
2959 <xsl:param name="incurrent_length" select="0"/> 
2960     <xsl:choose>
2961     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
2962      <xsl:variable name="siblength">
2963       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2964        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2965       </xsl:apply-templates>
2966      </xsl:variable>
2967      <xsl:choose>
2968      <xsl:when test="string($siblength) = &quot;&quot;">
2969       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2970      </xsl:when>
2971      <xsl:otherwise>
2972       <xsl:value-of select="number($siblength)"/>
2973      </xsl:otherwise>
2974      </xsl:choose>
2975     </xsl:when>
2976     <xsl:otherwise>
2977      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2978     </xsl:otherwise>
2979     </xsl:choose>
2980 </xsl:template>
2981
2982 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2983 <xsl:param name="incurrent_length" select="0"/> 
2984 <xsl:param name="nosibling" select="0"/>
2985     <xsl:choose>
2986     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2987      <xsl:variable name="siblength">
2988       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2989        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2990       </xsl:apply-templates>
2991      </xsl:variable>
2992      <xsl:choose>
2993      <xsl:when test="string($siblength) = &quot;&quot;">
2994       <xsl:value-of select="$incurrent_length + string-length()"/>
2995      </xsl:when>
2996      <xsl:otherwise>
2997       <xsl:value-of select="number($siblength)"/>
2998      </xsl:otherwise>
2999      </xsl:choose>
3000     </xsl:when>
3001     <xsl:otherwise>
3002      <xsl:value-of select="$incurrent_length + string-length()"/>
3003     </xsl:otherwise>
3004     </xsl:choose>
3005 </xsl:template> 
3006
3007 <xsl:template match="*" mode="charcount">
3008 <xsl:param name="incurrent_length" select="0"/>
3009 <xsl:param name="nosibling" select="0"/>
3010  <xsl:choose>
3011   <xsl:when test="count(child::*) = 0">
3012    <!-- CSC: tremendous bug fixed. An empty element can still have siblings!!! -->
3013    <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
3014    <xsl:choose>
3015     <xsl:when test="string($siblength) = &quot;&quot;">
3016      <xsl:value-of select="$incurrent_length"/>
3017     </xsl:when>
3018     <xsl:otherwise>
3019       <xsl:value-of select="number($siblength)"/>
3020     </xsl:otherwise>
3021    </xsl:choose>
3022   </xsl:when>
3023   <xsl:otherwise>
3024     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/><xsl:with-param name="nosibling" select="0"/></xsl:apply-templates></xsl:variable>
3025     <xsl:choose>
3026     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
3027      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
3028      <xsl:choose>
3029      <xsl:when test="string($siblength) = &quot;&quot;">
3030       <xsl:value-of select="number($childlength)"/>
3031      </xsl:when>
3032      <xsl:otherwise>
3033       <xsl:value-of select="number($siblength)"/>
3034      </xsl:otherwise>
3035      </xsl:choose>
3036     </xsl:when>
3037     <xsl:otherwise>
3038      <xsl:value-of select="number($childlength)"/>
3039     </xsl:otherwise>
3040     </xsl:choose>
3041   </xsl:otherwise>
3042  </xsl:choose>
3043 </xsl:template>
3044
3045 </xsl:stylesheet> 
3046