]> matita.cs.unibo.it Git - helm.git/blob - helm/style/mmlextension.xsl
----------------------------------------------------------------------
[helm.git] / helm / style / 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 <xsl:import href="mmlctop.xsl-0.14"/>
44
45 <xsl:import href="mmltheoryextension.xsl"/>
46
47 <xsl:param name="explodeall" select="false()"/>
48
49 <!--***********************************************************************-->
50 <!-- Parameter affecting line-breaking                                     -->
51 <!--***********************************************************************-->
52
53 <xsl:variable name="framewidth" select="35"/>
54
55 <!--***********************************************************************-->
56 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
57 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
58 <!-- sono i termini: la presentation per un termine e' generata come primo -->
59 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
60 <!-- nel secondo figlio di semantics, annotation-xml                       -->
61 <!--***********************************************************************-->
62
63 <!--**********************-->
64 <!--        OBJECTS       -->
65 <!--**********************-->
66
67 <xsl:param name="type" select="'standalone'"/>
68
69 <xsl:template match="/">
70  <xsl:choose>
71   <xsl:when test="$type = 'standalone'">
72    <xsl:apply-templates select="*"/>
73   </xsl:when>
74   <xsl:otherwise>
75    <to_be_embedded>
76     <xsl:apply-templates select="*"/>
77    </to_be_embedded>
78   </xsl:otherwise> 
79  </xsl:choose>
80 </xsl:template>
81
82 <!-- DEFINITION -->
83
84 <xsl:template match="Definition">
85     <m:math>
86      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
87       <m:mtr>
88        <m:mtd>
89         <m:mrow>
90          <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>
91         </m:mrow>
92        </m:mtd>
93       </m:mtr>
94       <m:mtr>
95        <m:mtd>
96         <m:mrow>
97          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
98          <xsl:apply-templates select="type/*[1]"/>
99         </m:mrow>
100        </m:mtd>
101       </m:mtr>
102       <m:mtr>
103        <m:mtd>
104         <m:mrow>
105          <m:mtext>AS</m:mtext>
106         </m:mrow>
107        </m:mtd>
108       </m:mtr>
109       <m:mtr>
110        <m:mtd>
111         <m:mrow>
112          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
113          <xsl:apply-templates select="body/*[1]"/>
114         </m:mrow>
115        </m:mtd>
116       </m:mtr>
117      </m:mtable>
118     </m:math>
119 </xsl:template>
120
121 <!-- AXIOM -->
122
123 <xsl:template match="Axiom">
124     <m:math>
125      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
126       <m:mtr>
127        <m:mtd>
128         <m:mrow>
129          <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>
130         </m:mrow>
131        </m:mtd>
132       </m:mtr>
133       <m:mtr>
134        <m:mtd>
135         <m:mrow>
136          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
137          <xsl:apply-templates select="type/*[1]"/>
138         </m:mrow>
139        </m:mtd>
140       </m:mtr>
141      </m:mtable>
142     </m:math>
143 </xsl:template>
144
145 <!-- UNFINISHED PROOF -->
146
147 <xsl:template match="CurrentProof">
148     <m:math>
149      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
150       <m:mtr>
151        <m:mtd>
152         <m:mrow>
153          <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>
154         </m:mrow>
155        </m:mtd>
156       </m:mtr>
157       <m:mtr>
158        <m:mtd>
159         <m:mrow>
160          <m:mtext>THESIS:</m:mtext>
161         </m:mrow>
162        </m:mtd>
163       </m:mtr>
164       <m:mtr>
165        <m:mtd>
166         <m:mrow>
167          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
168          <xsl:apply-templates select="type/*[1]"/>
169         </m:mrow>
170        </m:mtd>
171       </m:mtr>
172       <m:mtr>
173        <m:mtd>
174         <m:mrow>
175          <m:mtext>CONJECTURES:</m:mtext>
176         </m:mrow>
177        </m:mtd>
178       </m:mtr>
179       <xsl:for-each select="Conjecture">
180       <m:mtr>
181        <m:mtd>
182         <m:mrow>
183          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
184          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
185          <xsl:apply-templates select="./*[1]"/>
186         </m:mrow>
187        </m:mtd>
188       </m:mtr>
189       </xsl:for-each>
190       <m:mtr>
191        <m:mtd>
192         <m:mrow>
193          <m:mtext>CORRESPONDING PROOF:</m:mtext>
194         </m:mrow>
195        </m:mtd>
196       </m:mtr>
197       <m:mtr>
198        <m:mtd>
199         <m:mrow>
200          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
201          <xsl:apply-templates select="body/*[1]"/>
202         </m:mrow>
203        </m:mtd>
204       </m:mtr>
205      </m:mtable>
206     </m:math>
207 </xsl:template>
208
209 <!-- MUTUAL INDUCTIVE DEFINITION -->
210
211 <xsl:template match="InductiveDefinition">
212     <m:math>
213      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
214      <xsl:for-each select="InductiveType">
215       <m:mtr>
216        <m:mtd>
217         <m:mrow>
218          <xsl:choose>
219          <xsl:when test="position() = 1">
220           <xsl:choose>
221           <xsl:when test="string(./@inductive) = &quot;true&quot;">
222            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
223           </xsl:when>
224           <xsl:otherwise>
225            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
226           </xsl:otherwise>
227           </xsl:choose>  
228          </xsl:when>
229          <xsl:otherwise>
230           <m:mtext>AND</m:mtext>
231          </xsl:otherwise>
232          </xsl:choose>
233          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
234          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
235         </m:mrow>
236        </m:mtd>
237       </m:mtr>
238       <m:mtr>
239        <m:mtd>
240         <m:mrow> 
241          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
242          <m:mtext>[</m:mtext>
243          <xsl:choose>
244          <xsl:when test="string(../Param) != &quot;&quot;">         
245           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
246            <xsl:for-each select="../Param">
247             <m:mtr>
248              <m:mtd>
249               <m:mrow>   
250                <m:mi><xsl:value-of select="./@name"/></m:mi>
251                <m:mo>:</m:mo>
252                <xsl:apply-templates select="*"/>
253               </m:mrow>
254              </m:mtd>
255             </m:mtr>
256            </xsl:for-each>
257             <m:mtr>
258              <m:mtd>
259               <m:mrow>
260                <m:mtext>]</m:mtext>
261               </m:mrow>
262              </m:mtd>
263             </m:mtr>
264           </m:mtable>
265          </xsl:when>
266          <xsl:otherwise>
267           <m:mtext>]</m:mtext>
268          </xsl:otherwise>
269          </xsl:choose>
270         </m:mrow>
271        </m:mtd>
272       </m:mtr>
273       <m:mtr>
274        <m:mtd>
275         <m:mrow>
276          <m:mtext>OF ARITY</m:mtext>
277         </m:mrow>
278        </m:mtd>
279       </m:mtr>
280       <m:mtr>
281        <m:mtd>
282         <m:mrow>
283          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
284          <xsl:apply-templates select="./arity/*[1]"/>
285         </m:mrow>
286        </m:mtd>
287       </m:mtr>
288       <m:mtr>
289        <m:mtd>
290         <m:mrow>
291          <m:mtext>BUILT FROM</m:mtext>
292         </m:mrow>
293        </m:mtd>
294       </m:mtr>
295       <xsl:for-each select="./Constructor">
296       <m:mtr>
297        <m:mtd>
298         <m:mrow>
299          <xsl:choose>
300          <xsl:when test="position() = 1">
301           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
302          </xsl:when>
303          <xsl:otherwise>
304           <m:mtext>|</m:mtext>
305           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
306          </xsl:otherwise>
307          </xsl:choose>
308          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
309          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
310          <xsl:apply-templates select="./*[1]"/>
311         </m:mrow>
312        </m:mtd>
313       </m:mtr>
314       </xsl:for-each>
315      </xsl:for-each>
316      </m:mtable>
317     </m:math>
318 </xsl:template>
319
320 <!-- VARIABLE -->
321
322 <xsl:template match="Variable">
323     <m:math>
324      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
325       <m:mtr>
326        <m:mtd>
327         <m:mrow>
328          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
329         </m:mrow>
330        </m:mtd>
331       </m:mtr>
332       <m:mtr>
333        <m:mtd>
334         <m:mrow>
335          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
336          <xsl:apply-templates select="type/*[1]"/>
337         </m:mrow>
338        </m:mtd>
339       </m:mtr>
340       <xsl:if test="name(*[1])='body'">
341        <m:mtr>
342         <m:mtd>
343          <m:mrow>
344           <m:mtext>AS</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="body/*[1]"/>
353          </m:mrow>
354         </m:mtd>
355        </m:mtr>
356       </xsl:if>
357      </m:mtable>
358     </m:math>
359 </xsl:template>
360
361 <!--**********************-->
362 <!--        TERMS         -->
363 <!--**********************-->
364
365 <xsl:template match="m:bvar">
366  <xsl:choose>
367   <xsl:when test="m:type">
368    <xsl:variable name="charlength">
369     <xsl:apply-templates select="m:ci" mode="charcount"/>
370    </xsl:variable>
371    <xsl:choose>
372     <xsl:when test="$charlength >= $framewidth">
373      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
374       <m:mtr>
375        <m:mtd>
376         <m:mrow>
377          <xsl:apply-templates select="m:ci"/>
378          <m:mo>:</m:mo>
379         </m:mrow>
380        </m:mtd>
381       </m:mtr>
382       <m:mtr>
383        <m:mtd>
384         <m:mrow>
385          <xsl:apply-templates select="m:type"/>
386         </m:mrow>
387        </m:mtd>
388       </m:mtr>
389      </m:mtable>
390     </xsl:when>
391     <xsl:otherwise>
392      <m:mrow>
393       <xsl:apply-templates select="m:ci"/>
394       <m:mo>:</m:mo>
395       <xsl:apply-templates select="m:type"/>
396      </m:mrow>
397     </xsl:otherwise>
398    </xsl:choose>
399   </xsl:when>
400   <xsl:otherwise>
401    <xsl:apply-templates select="m:ci"/>
402   </xsl:otherwise>
403  </xsl:choose>
404 </xsl:template>
405
406
407 <!-- CSYMBOL -->
408
409 <xsl:template match="m:apply[m:csymbol]">
410 <xsl:param name="nopar" select="0"/>
411     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
412     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
413     <m:mrow>
414      <xsl:if test="@id">
415       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
416      </xsl:if>
417      <xsl:choose>
418       <!-- FORALL -->
419       <xsl:when test="$name='forall'">
420        <xsl:choose>
421        <xsl:when test="$charlength >= $framewidth">
422         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
423          <m:mtr>
424           <m:mtd>
425            <m:mrow>
426             <m:mo mathcolor="Blue">&#8704;</m:mo>
427             <xsl:apply-templates select="m:bvar"/>
428            </m:mrow>
429           </m:mtd>
430          </m:mtr>
431          <m:mtr>
432           <m:mtd>
433            <m:mrow>
434             <m:mo>.</m:mo>
435             <xsl:apply-templates select="*[position()=3]"/>
436            </m:mrow>
437           </m:mtd>
438          </m:mtr>
439         </m:mtable>
440        </xsl:when>
441        <xsl:otherwise>
442         <m:mo mathcolor="Blue">&#8704;</m:mo>
443         <xsl:apply-templates select="m:bvar/m:ci"/>
444         <m:mo>:</m:mo>
445         <xsl:apply-templates select="m:bvar/m:type"/>
446         <m:mo>.</m:mo>
447         <xsl:apply-templates select="*[position()=3]"/>
448        </xsl:otherwise>
449        </xsl:choose> 
450       </xsl:when>
451       <!-- LET-IN -->
452       <xsl:when test="$name='let_in'">
453        <xsl:choose>
454        <xsl:when test="$charlength >= $framewidth">
455         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
456          <m:mtr>
457           <m:mtd>
458            <m:mrow>
459             <m:mo>LET</m:mo>
460             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
461             <xsl:apply-templates select="m:bvar"/>
462            </m:mrow>
463           </m:mtd>
464          </m:mtr>
465          <m:mtr>
466           <m:mtd>
467            <m:mrow>
468             <m:mo>=</m:mo>
469             <xsl:apply-templates select="*[position()=3]"/>
470            </m:mrow>
471           </m:mtd>
472          </m:mtr>
473          <m:mtr>
474           <m:mtd>
475            <m:mrow>
476             <m:mo>IN</m:mo>
477             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
478             <xsl:apply-templates select="*[position()=4]"/>
479            </m:mrow>
480           </m:mtd>
481          </m:mtr>
482         </m:mtable>
483        </xsl:when>
484        <xsl:otherwise>
485         <m:mo>LET</m:mo>
486         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
487         <xsl:apply-templates select="m:bvar/m:ci"/>
488         <m:mo>=</m:mo>
489         <xsl:apply-templates select="*[position()=3]"/>
490         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
491         <m:mtext>IN</m:mtext>
492         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
493         <xsl:apply-templates select="*[position()=4]"/>
494        </xsl:otherwise>
495        </xsl:choose>
496       </xsl:when> 
497       <!-- PROD -->
498       <xsl:when test="$name='prod'">
499        <xsl:choose>
500        <xsl:when test="$charlength >= $framewidth">
501         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
502          <m:mtr>
503           <m:mtd>
504            <m:mrow>
505             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
506             <xsl:apply-templates select="m:bvar"/>
507            </m:mrow>
508           </m:mtd>
509          </m:mtr>
510          <m:mtr>
511           <m:mtd>
512            <m:mrow>
513             <m:mo>.</m:mo>
514             <xsl:apply-templates select="*[position()=3]"/>
515            </m:mrow>
516           </m:mtd>
517          </m:mtr>
518         </m:mtable>
519        </xsl:when>
520        <xsl:otherwise>
521         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
522         <xsl:apply-templates select="m:bvar/m:ci"/>
523         <m:mo>:</m:mo>
524         <xsl:apply-templates select="m:bvar/m:type"/>
525         <m:mo>.</m:mo>
526         <xsl:apply-templates select="*[position()=3]"/>
527        </xsl:otherwise>
528        </xsl:choose> 
529       </xsl:when>
530       <!-- ARROW -->
531       <xsl:when test="$name='arrow'">
532        <xsl:choose>
533        <xsl:when test="$charlength >= $framewidth">
534         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
535          <m:mtr>
536           <m:mtd>
537            <m:mrow>
538             <xsl:if test="$nopar=0">
539              <m:mo stretchy="false">(</m:mo>
540             </xsl:if>
541             <xsl:apply-templates select="*[position()=2]"/>
542            </m:mrow>
543           </m:mtd>
544          </m:mtr>
545          <m:mtr>
546           <m:mtd>
547            <m:mrow>
548             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
549             <xsl:choose>
550             <xsl:when test="*[position()=3]/m:csymbol">
551              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
552              <xsl:choose>
553              <xsl:when test="$nextp='arrow'">
554               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
555              </xsl:when>
556              <xsl:otherwise>
557               <xsl:apply-templates select="*[position()=3]"/>
558              </xsl:otherwise>
559              </xsl:choose>
560             </xsl:when>
561             <xsl:otherwise>
562              <xsl:apply-templates select="*[position()=3]"/>
563             </xsl:otherwise>
564             </xsl:choose>
565            </m:mrow>
566           </m:mtd>
567          </m:mtr>
568          <xsl:if test="$nopar=0">
569          <m:mtr>
570           <m:mtd>
571            <m:mrow>
572             <m:mo stretchy="false">)</m:mo>
573            </m:mrow>
574           </m:mtd>
575          </m:mtr>
576          </xsl:if>
577         </m:mtable>
578        </xsl:when>
579        <xsl:otherwise>
580         <xsl:if test="$nopar=0">
581          <m:mo stretchy="false">(</m:mo>
582         </xsl:if>
583         <xsl:apply-templates select="*[position()=2]"/>
584         <m:mo mathcolor="Blue">&#x2192;</m:mo>
585         <xsl:choose>
586         <xsl:when test="*[position()=3]/m:csymbol">
587          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
588          <xsl:choose>
589          <xsl:when test="$nextp='arrow'">
590           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
591          </xsl:when>
592          <xsl:otherwise>
593           <xsl:apply-templates select="*[position()=3]"/>
594          </xsl:otherwise>
595          </xsl:choose>
596         </xsl:when>
597         <xsl:otherwise>
598          <xsl:apply-templates select="*[position()=3]"/>
599         </xsl:otherwise>
600         </xsl:choose>
601         <xsl:if test="$nopar=0">
602          <m:mo stretchy="false">)</m:mo>
603         </xsl:if>
604        </xsl:otherwise>
605        </xsl:choose>
606       </xsl:when>
607       <!-- APP -->
608       <xsl:when test="$name='app'">
609        <xsl:choose>
610        <xsl:when test="$charlength >= $framewidth">
611         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
612          <m:mtr>
613           <m:mtd>
614            <m:mrow>
615             <m:mo stretchy="false">(</m:mo>
616             <xsl:apply-templates select="*[position()=2]"/>
617            </m:mrow>
618           </m:mtd>
619          </m:mtr>
620          <xsl:for-each select="*[position()>2]">
621          <m:mtr>
622           <m:mtd>
623            <m:mrow>
624             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
625             <xsl:apply-templates select="."/>
626            </m:mrow>
627           </m:mtd>
628          </m:mtr>
629          </xsl:for-each>
630          <m:mtr>
631           <m:mtd>
632            <m:mrow>
633             <m:mo stretchy="false">)</m:mo>
634            </m:mrow>
635           </m:mtd>
636          </m:mtr>
637         </m:mtable>
638        </xsl:when>
639        <xsl:otherwise>
640         <m:mo stretchy="false">(</m:mo>
641         <xsl:apply-templates select="*[position()=2]"/>
642         <xsl:for-each select="*[position()>2]">
643          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
644          <xsl:apply-templates select="."/>
645         </xsl:for-each>
646         <m:mo stretchy="false">)</m:mo>
647        </xsl:otherwise>
648        </xsl:choose>
649       </xsl:when>
650       <!-- CAST -->
651       <xsl:when test="$name='cast'">
652        <xsl:choose>
653        <xsl:when test="$charlength >= $framewidth">
654         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
655          <m:mtr>
656           <m:mtd>
657            <m:mrow>
658             <m:mo stretchy="false">(</m:mo>
659             <xsl:apply-templates select="*[position()=2]"/>
660            </m:mrow>
661           </m:mtd>
662          </m:mtr>
663          <m:mtr>
664           <m:mtd>
665            <m:mrow>
666             <m:mo mathcolor="Maroon">:></m:mo>
667             <xsl:apply-templates select="*[position()=3]"/>
668            </m:mrow>
669           </m:mtd>
670          </m:mtr>
671          <m:mtr>
672           <m:mtd>
673            <m:mrow>
674             <m:mo stretchy="false">)</m:mo>
675            </m:mrow>
676           </m:mtd>
677          </m:mtr>
678         </m:mtable>
679        </xsl:when>
680        <xsl:otherwise>
681         <m:mo stretchy="false">(</m:mo>
682         <xsl:apply-templates select="*[position()=2]"/>
683         <m:mo mathcolor="Maroon">:></m:mo>
684         <xsl:apply-templates select="*[position()=3]"/>
685         <m:mo stretchy="false">)</m:mo>
686        </xsl:otherwise>
687        </xsl:choose>
688       </xsl:when>
689       <!-- PROP -->
690       <xsl:when test="$name='Prop'">
691        <m:mo>Prop</m:mo>
692       </xsl:when>
693       <!-- SET -->
694       <xsl:when test="$name='Set'">
695        <m:mo>Set</m:mo>
696       </xsl:when>
697       <!-- TYPE -->
698       <xsl:when test="$name='Type'">
699        <m:mo>Type</m:mo>
700       </xsl:when>
701       <!-- MUTCASE -->
702       <xsl:when test="$name='mutcase'">
703        <xsl:choose>
704        <xsl:when test="$charlength >= $framewidth">
705         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
706         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
707          <m:mtr>
708           <m:mtd>
709            <m:mrow>
710             <m:mo>&lt;</m:mo>
711             <xsl:apply-templates select="*[position()=2]"/>
712             <xsl:if test="$framewidth > $charlength">
713              <m:mo>&gt;</m:mo>
714              <m:mo>CASES</m:mo>
715              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
716              <xsl:apply-templates select="*[position()=3]"/>
717             </xsl:if>
718            </m:mrow>
719           </m:mtd>
720          </m:mtr>
721          <xsl:if test="$charlength >= $framewidth">
722          <m:mtr>
723           <m:mtd>
724            <m:mrow>
725             <m:mo>&gt;</m:mo>
726             <m:mo>CASES</m:mo>
727             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
728             <xsl:apply-templates select="*[position()=3]"/>
729            </m:mrow>
730           </m:mtd>
731          </m:mtr>
732          </xsl:if>
733          <m:mtr>
734           <m:mtd>
735            <m:mrow>
736             <m:mo>OF</m:mo>
737            </m:mrow>
738           </m:mtd>
739          </m:mtr>
740          <xsl:for-each select="piecewise/piece">
741          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
742          <m:mtr>
743           <m:mtd>
744            <m:mrow>
745             <xsl:choose>
746             <xsl:when test="position() = 1">
747               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
748             </xsl:when>
749             <xsl:otherwise>
750              <m:mo stretchy="false">|</m:mo>
751             </xsl:otherwise>
752             </xsl:choose>
753             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
754             <xsl:apply-templates select="./*[2]"/>
755             <xsl:if test="$framewidth > $charlength">
756              <m:mo mathcolor="Green">&#x21d2;</m:mo>
757              <xsl:apply-templates select="./*[1]"/>
758             </xsl:if>
759            </m:mrow>
760           </m:mtd>
761          </m:mtr>
762          <xsl:if test="$charlength >= $framewidth">
763          <m:mtr>
764           <m:mtd>
765            <m:mrow>
766             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
767             <m:mo mathcolor="Green">&#x21d2;</m:mo>
768             <xsl:apply-templates select="./*[1]"/>
769            </m:mrow>
770           </m:mtd>
771          </m:mtr>
772          </xsl:if>
773         </xsl:for-each>
774          <m:mtr>
775           <m:mtd>
776            <m:mrow>
777             <m:mo>END</m:mo>
778            </m:mrow>
779           </m:mtd>
780          </m:mtr>
781         </m:mtable>
782        </xsl:when>
783        <xsl:otherwise>
784         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
785         <m:mo>CASES</m:mo>
786         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
787         <xsl:apply-templates select="*[position()=3]"/>
788         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
789         <m:mo>OF</m:mo>
790         <xsl:for-each select="piecewise/piece">
791          <xsl:choose>
792          <xsl:when test="position() != 1">
793           <m:mo stretchy="false">|</m:mo>
794          </xsl:when> 
795          </xsl:choose>
796          <xsl:apply-templates select="./*[2]"/>
797          <m:mo mathcolor="Green">&#x21d2;</m:mo>
798          <xsl:apply-templates select="./*[1]"/>
799         </xsl:for-each>
800         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
801         <m:mo>END</m:mo>
802        </xsl:otherwise>
803        </xsl:choose>
804       </xsl:when>
805       <!-- FIX -->
806       <xsl:when test="$name='fix'">
807        <xsl:choose>
808        <xsl:when test="$charlength >= $framewidth">
809         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
810          <m:mtr>
811           <m:mtd>
812            <m:mrow>
813             <m:mo>FIX</m:mo>
814             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
815             <m:mi><xsl:value-of select="m:ci"/></m:mi>
816             <m:mo stretchy="false">{</m:mo>
817            </m:mrow>
818           </m:mtd>
819          </m:mtr>
820          <m:mtr>
821           <m:mtd>
822            <m:mrow>
823             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
824             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
825             <xsl:for-each select="m:bvar"> 
826              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
827              <m:mtr>
828               <m:mtd>
829                <m:mrow>
830                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
831                 <m:mo>:</m:mo>
832                 <xsl:if test="$framewidth > $charlength">
833                  <xsl:apply-templates select="m:type"/>
834                 </xsl:if>
835                </m:mrow>
836               </m:mtd>
837              </m:mtr> 
838              <xsl:if test="$charlength >= $framewidth">
839              <m:mtr>
840               <m:mtd>
841                <m:mrow>
842                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
843                 <xsl:apply-templates select="m:type"/>
844                </m:mrow>
845               </m:mtd>
846              </m:mtr>
847              </xsl:if>
848              <m:mtr>
849               <m:mtd>
850                <m:mrow>
851                 <m:mo>:=</m:mo>
852                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
853                </m:mrow>
854               </m:mtd>
855              </m:mtr> 
856             </xsl:for-each>
857             </m:mtable>
858            </m:mrow>
859           </m:mtd>
860          </m:mtr>
861          <m:mtr>
862           <m:mtd>
863            <m:mrow>
864             <m:mo stretchy="false">}</m:mo>
865            </m:mrow>
866           </m:mtd>
867          </m:mtr>
868         </m:mtable>
869        </xsl:when>
870        <xsl:otherwise>
871         <m:mo>FIX</m:mo>
872         <m:mi><xsl:value-of select="m:ci"/></m:mi>
873         <m:mo stretchy="false">{</m:mo>
874         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
875         <xsl:for-each select="m:bvar"> 
876          <m:mtr>
877           <m:mtd>
878            <m:mrow>
879             <m:mi><xsl:value-of select="m:ci"/></m:mi>
880             <m:mo>:</m:mo>
881             <xsl:apply-templates select="m:type"/>
882             <m:mo>:=</m:mo>
883             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
884             <xsl:if test="position()=last()">
885              <m:mo stretchy="false">}</m:mo>
886             </xsl:if>
887            </m:mrow>
888           </m:mtd>
889          </m:mtr>
890          </xsl:for-each>
891         </m:mtable>
892        </xsl:otherwise>
893        </xsl:choose>
894       </xsl:when>
895       <!-- COFIX -->
896       <xsl:when test="$name='cofix'">
897        <xsl:choose>
898        <xsl:when test="$charlength >= $framewidth">
899         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
900          <m:mtr>
901           <m:mtd>
902            <m:mrow>
903             <m:mo>COFIX</m:mo>
904             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
905             <m:mi><xsl:value-of select="m:ci"/></m:mi>
906             <m:mo stretchy="false">{</m:mo>
907            </m:mrow>
908           </m:mtd>
909          </m:mtr>
910          <m:mtr>
911           <m:mtd>
912            <m:mrow>
913             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
914             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
915             <xsl:for-each select="m:bvar">
916              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable> 
917              <m:mtr>
918               <m:mtd>
919                <m:mrow>
920                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
921                 <m:mo>:</m:mo>
922                 <xsl:if test="$framewidth > $charlength">
923                  <xsl:apply-templates select="m:type"/>
924                 </xsl:if>
925                </m:mrow>
926               </m:mtd>
927              </m:mtr> 
928              <xsl:if test="$charlength >= $framewidth">
929              <m:mtr>
930               <m:mtd>
931                <m:mrow>
932                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
933                 <xsl:apply-templates select="m:type"/>
934                </m:mrow>
935               </m:mtd>
936              </m:mtr>
937              </xsl:if>
938              <m:mtr>
939               <m:mtd>
940                <m:mrow>
941                 <m:mo>:=</m:mo>
942                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
943                </m:mrow>
944               </m:mtd>
945              </m:mtr>
946             </xsl:for-each>
947             </m:mtable>
948            </m:mrow>
949           </m:mtd>
950          </m:mtr>
951          <m:mtr>
952           <m:mtd>
953            <m:mrow>
954             <m:mo stretchy="false">}</m:mo>
955            </m:mrow>
956           </m:mtd>
957          </m:mtr>
958         </m:mtable>
959        </xsl:when>
960        <xsl:otherwise>
961         <m:mo>COFIX</m:mo>
962         <m:mi><xsl:value-of select="m:ci"/></m:mi>
963         <m:mo stretchy="false">{</m:mo>
964         <m:mtable align="baseline 1" equalrows="false" columnalign="left">  
965         <xsl:for-each select="m:bvar"> 
966          <m:mtr>
967           <m:mtd>
968            <m:mrow>
969             <m:mi><xsl:value-of select="m:ci"/></m:mi>
970             <m:mo>:</m:mo>
971             <xsl:apply-templates select="m:type"/>
972             <m:mo>:=</m:mo>
973             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
974             <xsl:if test="position()=last()">
975              <m:mo stretchy="false">}</m:mo>
976             </xsl:if>
977            </m:mrow>
978           </m:mtd>
979          </m:mtr>
980          </xsl:for-each>
981         </m:mtable>
982        </xsl:otherwise>
983        </xsl:choose>
984       </xsl:when>
985       <!-- ***************************************** -->
986       <!-- *********** PROOF ELEMENTS ************** -->
987       <!-- ***************************************** -->
988       <!-- PROOF -->
989       <xsl:when test="$name='proof'">
990        <m:maction actiontype="toggle">
991         <!-- CSC: next if until the annotationHelper can handle mactions -->
992         <xsl:if test="not($explodeall)">
993          <!-- Details hided (default) -->
994          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
995           <m:mtr>
996            <m:mtd>
997             <m:mrow>
998              <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
999              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1000              <xsl:apply-templates select="*[position()=3]"/>
1001              <m:mrow>
1002               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1003               <m:mtext mathcolor="Green">(explain)</m:mtext>
1004              </m:mrow>
1005             </m:mrow>
1006            </m:mtd>
1007           </m:mtr>
1008          </m:mtable>
1009         </xsl:if>
1010         <!-- Show details -->
1011         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <xsl:apply-templates select="*[position()=2]"/>
1016            </m:mrow>
1017           </m:mtd>
1018          </m:mtr>
1019          <m:mtr>
1020           <m:mtd>
1021            <m:mrow>
1022             <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
1023             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1024             <xsl:apply-templates select="*[position()=3]"/>
1025             <m:mrow>
1026              <m:mphantom>
1027               <m:mtext>_</m:mtext>
1028              </m:mphantom>
1029              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1030             </m:mrow>
1031            </m:mrow>
1032           </m:mtd>
1033          </m:mtr>
1034         </m:mtable>
1035        </m:maction>
1036       </xsl:when>
1037       <!-- LETIN1 -->
1038       <xsl:when test="$name='letin1'">
1039         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1040          <m:mtr>
1041           <m:mtd>
1042            <m:mrow>
1043             <xsl:apply-templates select="*[2]"/>
1044            </m:mrow>
1045           </m:mtd>
1046          </m:mtr>
1047          <m:mtr>
1048           <m:mtd>
1049            <m:mrow>
1050             <xsl:apply-templates select="*[3]"/>
1051            </m:mrow>
1052           </m:mtd>
1053          </m:mtr>
1054         </m:mtable>
1055       </xsl:when>
1056       <xsl:when test="$name='by_induction'">
1057        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1058         <m:mtr>
1059          <m:mtd>
1060           <m:mrow>
1061            <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
1062            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1063            <xsl:apply-templates select="../*[3]"/>
1064           </m:mrow>
1065          </m:mtd>
1066         </m:mtr>
1067         <m:mtr>
1068          <m:mtd>
1069           <m:mrow>
1070            <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
1071            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1072            <xsl:apply-templates 
1073             select="*[position()=last()]/*[position()=last()]"/>
1074           </m:mrow>
1075          </m:mtd>
1076         </m:mtr>
1077         <m:mtr>
1078          <m:mtd>
1079           <m:mrow>
1080            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1081             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1082              <m:mtr>
1083               <m:mtd>
1084                <m:mrow>
1085                 <xsl:apply-templates select="."/>
1086                </m:mrow>
1087               </m:mtd>
1088              </m:mtr>
1089             </xsl:for-each>
1090            </m:mtable>
1091           </m:mrow>
1092          </m:mtd>
1093         </m:mtr>
1094        </m:mtable>
1095       </xsl:when>
1096       <!-- inductive_case -->
1097       <xsl:when test="$name='inductive_case'">
1098        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1099         <m:mtr>
1100          <m:mtd>
1101           <m:mrow>
1102            <m:mtext mathcolor="red">Case</m:mtext>
1103            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1104            <xsl:apply-templates select="*[2]"/>
1105           </m:mrow>
1106          </m:mtd>
1107         </m:mtr>
1108         <m:mtr>
1109          <m:mtd>
1110           <m:mrow>
1111            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1112            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1113             <xsl:if test="*[3]/*[position()>1]">
1114              <m:mtr>
1115               <m:mtd>
1116                <m:mrow>
1117                 <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
1118                </m:mrow>
1119               </m:mtd>
1120              </m:mtr>
1121              <m:mtr>
1122               <m:mtd>
1123                <m:mrow>
1124                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1125                 <xsl:for-each select="*[3]/*[position()>1]">
1126                  <m:mo stretchy="false">(</m:mo>
1127                  <xsl:apply-templates select="m:ci"/>
1128                  <m:mo stretchy="false">) </m:mo>
1129                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1130                  <xsl:apply-templates select="m:type"/>
1131                 </xsl:for-each>
1132                </m:mrow>
1133               </m:mtd>
1134              </m:mtr>
1135             </xsl:if>
1136             <m:mtr>
1137              <m:mtd>
1138               <m:mrow>
1139                <xsl:apply-templates select="*[4]"/>
1140               </m:mrow>
1141              </m:mtd>
1142             </m:mtr>
1143            </m:mtable>
1144           </m:mrow>
1145          </m:mtd>
1146         </m:mtr>
1147        </m:mtable>
1148       </xsl:when>
1149       <!-- case_lhs  -->
1150       <xsl:when test="$name='case_lhs'">
1151        <m:mrow>
1152         <xsl:choose>
1153          <xsl:when test="count(*)=2">
1154           <xsl:apply-templates select="*[2]"/>
1155          </xsl:when>
1156          <xsl:otherwise>
1157           <m:mo stretchy="false">(</m:mo>
1158           <xsl:apply-templates select="*[2]"/>
1159           <xsl:for-each select="m:bvar">
1160            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1161            <xsl:apply-templates select="*[1]"/>
1162            <m:mtext>:</m:mtext>
1163            <xsl:apply-templates select="m:type/*[1]"/>
1164           </xsl:for-each>
1165           <m:mo stretchy="false">)</m:mo>
1166          </xsl:otherwise>
1167         </xsl:choose>
1168        </m:mrow>
1169       </xsl:when>
1170       <!-- false_ind  -->
1171       <xsl:when test="$name='false_ind'">
1172        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1173         <m:mtr>
1174          <m:mtd>
1175           <m:mrow>
1176            <xsl:apply-templates select="*[3]"/>
1177           </m:mrow>
1178          </m:mtd>
1179         </m:mtr>
1180         <m:mtr>
1181          <m:mtd>
1182           <m:mrow>
1183            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1184           </m:mrow>
1185          </m:mtd>
1186         </m:mtr>
1187        </m:mtable>
1188       </xsl:when>
1189       <!-- LET-IN -->
1190       <xsl:when test="$name='letin'">
1191         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1192          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1193          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1194          <m:mtr>
1195           <m:mtd>
1196            <m:mrow>
1197             <xsl:apply-templates select="."/>
1198            </m:mrow>
1199           </m:mtd>
1200          </m:mtr>
1201          </xsl:for-each>
1202          <m:mtr>
1203           <m:mtd>
1204            <m:mrow>
1205             <xsl:apply-templates select="*[position()=last()]"/>
1206            </m:mrow>
1207           </m:mtd>
1208          </m:mtr>
1209         </m:mtable>
1210       </xsl:when>
1211       <!-- LET -->
1212       <xsl:when test="$name='let'">
1213        <m:mtext>(</m:mtext>
1214        <xsl:apply-templates select="m:ci"/>
1215        <m:mtext>) </m:mtext>
1216        <xsl:apply-templates select="*[3]"/>
1217       </xsl:when>
1218       <!-- RW_STEP -->
1219       <xsl:when test="$name='rw_step'">
1220         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1221          <m:mtr>
1222           <m:mtd>
1223            <m:mrow>
1224             <xsl:choose>
1225              <xsl:when test="name(*[2])='m:apply'">
1226               <xsl:apply-templates select="*[2]"/>
1227              </xsl:when>
1228              <xsl:otherwise>
1229               <m:mtext>Consider</m:mtext>
1230               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1231               <xsl:apply-templates select="*[2]"/>
1232              </xsl:otherwise>
1233             </xsl:choose>
1234            </m:mrow>
1235           </m:mtd>
1236          </m:mtr>
1237          <m:mtr>
1238           <m:mtd>
1239            <m:mrow>
1240             <m:mtext>Rewrite</m:mtext>
1241             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1242             <xsl:apply-templates select="*[3]"/>
1243             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1244             <m:mtext>with</m:mtext>
1245             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1246             <xsl:apply-templates select="*[4]"/>
1247             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1248             <m:mtext>by</m:mtext>
1249             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1250             <xsl:apply-templates select="*[5]"/>
1251            </m:mrow>
1252           </m:mtd>
1253          </m:mtr>
1254         </m:mtable>
1255       </xsl:when>
1256       <!-- not existing any more
1257       <xsl:when test="$name='thread'">
1258         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1259          <m:mtr>
1260           <m:mtd>
1261            <m:mrow>
1262             <xsl:choose>
1263              <xsl:when test="name(*[last()])='m:apply'">
1264               <xsl:apply-templates select="*[last()]"/>
1265              </xsl:when>
1266              <xsl:otherwise>
1267               <m:mtext>Consider</m:mtext>
1268               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1269               <xsl:apply-templates select="*[last()]"/>
1270              </xsl:otherwise>
1271             </xsl:choose>
1272            </m:mrow>
1273           </m:mtd>
1274          </m:mtr>
1275          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
1276         </m:mtable>
1277       </xsl:when>
1278       --> 
1279       <!-- REWRITE_AND_APPLY -->
1280       <xsl:when test="$name='rewrite_and_apply'">
1281         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1282          <m:mtr>
1283           <m:mtd>
1284            <m:mrow>
1285             <xsl:apply-templates select="*[2]"/>
1286            </m:mrow>
1287           </m:mtd>
1288          </m:mtr>
1289          <m:mtr>
1290           <m:mtd>
1291            <m:mrow>
1292             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
1293             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1294             <xsl:apply-templates select="*[position()>2]"/>
1295            </m:mrow>
1296           </m:mtd>
1297          </m:mtr>
1298        </m:mtable>
1299       </xsl:when>
1300       <!-- AND_IND -->
1301       <xsl:when test="$name='and_ind'">
1302         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1303          <m:mtr>
1304           <m:mtd>
1305            <m:mrow>
1306             <xsl:choose>
1307              <xsl:when test="name(*[2])='m:apply'">
1308               <xsl:apply-templates select="*[2]"/>
1309              </xsl:when>
1310              <xsl:otherwise>
1311               <m:mtext>Consider</m:mtext>
1312               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1313               <xsl:apply-templates select="*[2]"/>
1314              </xsl:otherwise>
1315             </xsl:choose>
1316            </m:mrow>
1317           </m:mtd>
1318          </m:mtr>
1319          <m:mtr>
1320           <m:mtd>
1321            <m:mrow>
1322             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
1323            </m:mrow>
1324           </m:mtd>
1325          </m:mtr>
1326          <m:mtr>
1327           <m:mtd>
1328            <m:mrow>
1329             <m:mtext>(</m:mtext>
1330             <xsl:apply-templates select="*[3]"/>
1331             <m:mtext>)</m:mtext>
1332             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1333             <xsl:apply-templates select="*[4]"/>
1334             </m:mrow>
1335           </m:mtd>
1336          </m:mtr>
1337          <m:mtr>
1338           <m:mtd>
1339            <m:mrow>
1340             <m:mtext>(</m:mtext>
1341             <xsl:apply-templates select="*[5]"/>
1342             <m:mtext>)</m:mtext>
1343             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1344             <xsl:apply-templates select="*[6]"/>
1345             </m:mrow>
1346           </m:mtd>
1347          </m:mtr>
1348          <m:mtr>
1349           <m:mtd>
1350            <m:mrow>
1351             <xsl:apply-templates select="*[7]"/>
1352            </m:mrow>
1353           </m:mtd>
1354          </m:mtr>
1355         </m:mtable>
1356       </xsl:when>
1357       <!-- full_or_ind -->
1358       <xsl:when test="$name='full_or_ind'">
1359         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1360          <m:mtr>
1361           <m:mtd>
1362            <m:mrow>
1363             <xsl:choose>
1364              <xsl:when test="name(*[2])='m:apply'">
1365               <xsl:apply-templates select="*[2]"/>
1366              </xsl:when>
1367              <xsl:otherwise>
1368               <m:mtext>Consider</m:mtext>
1369               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1370               <xsl:apply-templates select="*[2]"/>
1371              </xsl:otherwise>
1372             </xsl:choose>
1373            </m:mrow>
1374           </m:mtd>
1375          </m:mtr>
1376          <m:mtr>
1377           <m:mtd>
1378            <m:mrow>
1379             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
1380             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1381             <xsl:apply-templates select="*[3]"/>
1382            </m:mrow>
1383           </m:mtd>
1384          </m:mtr>
1385          <m:mtr>
1386           <m:mtd>
1387            <m:mrow>
1388             <m:mtext>Left:&#x00a0;suppose</m:mtext>
1389             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1390             <m:mo stretchy="false">(</m:mo>
1391             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1392             <m:mo stretchy="false">)</m:mo>
1393             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1394             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1395            </m:mrow>
1396           </m:mtd>
1397          </m:mtr>
1398          <m:mtr>
1399           <m:mtd>
1400            <m:mrow>
1401             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1402             <xsl:apply-templates select="*[4]/*[3]"/>
1403            </m:mrow>
1404           </m:mtd>
1405          </m:mtr>
1406          <m:mtr>
1407           <m:mtd>
1408            <m:mrow>
1409             <m:mtext>Right:&#x00a0;suppose</m:mtext>
1410             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1411             <m:mo stretchy="false">(</m:mo>
1412             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1413             <m:mo stretchy="false">)</m:mo>
1414             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1415             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1416            </m:mrow>
1417           </m:mtd>
1418          </m:mtr>
1419          <m:mtr>
1420           <m:mtd>
1421            <m:mrow>
1422             <xsl:apply-templates select="*[5]/*[3]"/>
1423            </m:mrow>
1424           </m:mtd>
1425          </m:mtr>
1426         </m:mtable>
1427       </xsl:when>
1428       <!-- OR_IND -->
1429       <xsl:when test="$name='or_ind'">
1430         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1431          <m:mtr>
1432           <m:mtd>
1433            <m:mrow>
1434             <xsl:choose>
1435              <xsl:when test="name(*[2])='m:apply'">
1436               <xsl:apply-templates select="*[2]"/>
1437              </xsl:when>
1438              <xsl:otherwise>
1439               <m:mtext>Consider</m:mtext>
1440               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1441               <xsl:apply-templates select="*[2]"/>
1442              </xsl:otherwise>
1443             </xsl:choose>
1444            </m:mrow>
1445           </m:mtd>
1446          </m:mtr>
1447          <m:mtr>
1448           <m:mtd>
1449            <m:mrow>
1450             <m:mtext>We&#x00a0;prove</m:mtext>
1451             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1452             <xsl:apply-templates select="*[3]"/>
1453             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1454             <m:mtext>by&#x00a0;cases:</m:mtext>
1455            </m:mrow>
1456           </m:mtd>
1457          </m:mtr>
1458          <m:mtr>
1459           <m:mtd>
1460            <m:mrow>
1461             <m:mtext>Left</m:mtext>
1462             <xsl:apply-templates select="*[4]"/>
1463            </m:mrow>
1464           </m:mtd>
1465          </m:mtr>
1466          <m:mtr>
1467           <m:mtd>
1468            <m:mrow>
1469             <m:mtext>Right</m:mtext>
1470             <xsl:apply-templates select="*[5]"/>
1471            </m:mrow>
1472           </m:mtd>
1473          </m:mtr>
1474         </m:mtable>
1475       </xsl:when>
1476       <!-- EX_IND -->
1477       <xsl:when test="$name='ex_ind'">
1478         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1479          <m:mtr>
1480           <m:mtd>
1481            <m:mrow>
1482             <xsl:choose>
1483              <xsl:when test="name(*[2])='m:apply'">
1484               <xsl:apply-templates select="*[2]"/>
1485              </xsl:when>
1486              <xsl:otherwise>
1487               <m:mtext>Consider</m:mtext>
1488               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1489               <xsl:apply-templates select="*[2]"/>
1490              </xsl:otherwise>
1491             </xsl:choose>
1492            </m:mrow>
1493           </m:mtd>
1494          </m:mtr>
1495          <m:mtr>
1496           <m:mtd>
1497            <m:mrow>
1498             <m:mtext>Let</m:mtext>
1499             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1500             <xsl:apply-templates select="*[3]"/>
1501             <m:mtext>:</m:mtext>
1502             <xsl:apply-templates select="*[4]"/>
1503             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1504             <m:mtext>such&#x00a0;that</m:mtext>
1505             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1506             <m:mtext>(</m:mtext>
1507              <xsl:apply-templates select="*[5]"/>
1508             <m:mtext>)</m:mtext>
1509             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1510             <xsl:apply-templates select="*[6]"/>
1511            </m:mrow>
1512           </m:mtd>
1513          </m:mtr>
1514          <m:mtr>
1515           <m:mtd>
1516            <m:mrow>
1517             <xsl:apply-templates select="*[7]"/>
1518            </m:mrow>
1519           </m:mtd>
1520          </m:mtr>
1521         </m:mtable>
1522       </xsl:when>
1523       <!-- ***************************************** -->
1524       <!-- *********** NOTATIONS ******************* -->
1525       <!-- ***************************************** -->
1526       <!-- subst -->
1527       <xsl:when test="$name='subst'">
1528         <xsl:apply-templates select="*[3]"/>
1529 <!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
1530         <m:mo stretchy="false">[</m:mo>
1531         <xsl:apply-templates select="*[4]"/>
1532         <m:mo mathcolor="green">
1533          <xsl:if test="$id != ''">
1534           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1535          </xsl:if>&#8592;</m:mo>
1536         <xsl:apply-templates select="*[2]"/>
1537         <m:mo stretchy="false">]</m:mo>
1538       </xsl:when>
1539       <!-- lift -->
1540       <xsl:when test="$name='lift'">
1541         <m:msup>
1542          <m:mo mathcolor="green">
1543           <xsl:if test="$id != ''">
1544            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1545           </xsl:if>&#8593;</m:mo>
1546          <xsl:apply-templates select="*[2]"/>
1547         </m:msup>
1548         <m:mrow>
1549          <m:mo stretchy="false">(</m:mo>
1550          <xsl:apply-templates select="*[3]"/>
1551          <m:mo stretchy="false">)</m:mo>
1552         </m:mrow>
1553       </xsl:when>
1554       <!-- lift_with_base -->
1555       <xsl:when test="$name='lift_with_base'">
1556         <m:msubsup>
1557          <m:mo mathcolor="green">
1558           <xsl:if test="$id != ''">
1559            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1560           </xsl:if>&#8593;</m:mo>
1561          <xsl:apply-templates select="*[3]"/>
1562          <xsl:apply-templates select="*[4]"/>
1563         </m:msubsup>
1564         <m:mrow>
1565          <m:mo stretchy="false">(</m:mo>
1566          <xsl:apply-templates select="*[2]"/>
1567          <m:mo stretchy="false">)</m:mo>
1568         </m:mrow>       
1569       </xsl:when>
1570       <!-- beta_red1 -->
1571       <xsl:when test="$name='beta_red1'">
1572         <xsl:apply-templates select="*[2]"/>
1573         <m:munder>
1574          <m:mo mathcolor="green">
1575           <xsl:if test="$id != ''">
1576            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1577           </xsl:if>&#8594;</m:mo>
1578           <m:mi mathcolor="green">&#946;</m:mi>
1579         </m:munder>
1580         <xsl:apply-templates select="*[3]"/>
1581       </xsl:when>
1582       <!-- beta_red -->
1583       <xsl:when test="$name='beta_red'">
1584         <xsl:apply-templates select="*[2]"/>
1585         <m:munderover>
1586          <m:mo mathcolor="green">
1587           <xsl:if test="$id != ''">
1588            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1589           </xsl:if>&#8594;</m:mo>
1590           <m:mi mathcolor="green">&#946;</m:mi>
1591           <m:mi mathcolor="green">*</m:mi>
1592         </m:munderover>
1593         <xsl:apply-templates select="*[3]"/>
1594       </xsl:when>
1595       <!-- par_beta_red1 -->
1596       <xsl:when test="$name='par_beta_red1'">
1597         <xsl:apply-templates select="*[2]"/>
1598         <m:munder>
1599          <m:mo mathcolor="green">
1600           <xsl:if test="$id != ''">
1601            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1602           </xsl:if>&#8658;</m:mo>
1603           <m:mi mathcolor="green">&#946;</m:mi>
1604         </m:munder>
1605         <xsl:apply-templates select="*[3]"/>
1606       </xsl:when>
1607       <!-- par_beta_red -->
1608       <xsl:when test="$name='par_beta_red'">
1609         <xsl:apply-templates select="*[2]"/>
1610         <m:munderover>
1611          <m:mo mathcolor="green">
1612           <xsl:if test="$id != ''">
1613            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1614           </xsl:if>&#8658;</m:mo>
1615           <m:mi mathcolor="green">&#946;</m:mi>
1616           <m:mi mathcolor="green">*</m:mi>
1617         </m:munderover>
1618         <xsl:apply-templates select="*[3]"/>
1619       </xsl:when>
1620       <!-- forgetful -->
1621       <xsl:when test="$name='forgetful'">
1622        <m:mfenced open="|" close="|">
1623         <xsl:if test="$id != ''">
1624          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1625         </xsl:if>
1626         <xsl:apply-templates select="*[2]"/>
1627        </m:mfenced>
1628       </xsl:when>
1629       <!-- isomorphic -->
1630       <xsl:when test="$name='isomorphic'">
1631         <xsl:apply-templates select="*[2]"/>
1632         <m:mo mathcolor="green">
1633          <xsl:if test="$id != ''">
1634           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1635          </xsl:if>&#8773;</m:mo>
1636         <xsl:apply-templates select="*[3]"/>
1637       </xsl:when>
1638       <!-- interp -->
1639       <xsl:when test="$name='forgetful'">
1640        <m:mfenced open="[" close="]">
1641         <xsl:if test="$id != ''">
1642          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1643         </xsl:if>
1644         <xsl:apply-templates select="*[2]"/>
1645        </m:mfenced>
1646       </xsl:when> 
1647
1648       <!-- ERROR -->
1649       <xsl:otherwise>
1650        <m:mi>ERROR</m:mi>
1651       </xsl:otherwise>
1652      </xsl:choose>
1653     </m:mrow>
1654 </xsl:template>
1655
1656 <!-- Il modo Thread non esiste piu' 
1657 <xsl:template match="*" mode="thread">
1658  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1659  <xsl:choose>
1660   <xsl:when test="$name='rw_step'">
1661          <m:mtr>
1662           <m:mtd>
1663            <m:mrow>
1664             <m:mtext>Rewrite</m:mtext>
1665             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1666             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1667             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1668             <m:mtext>with</m:mtext>
1669             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1670             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1671             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1672             <m:mtext>by</m:mtext>
1673             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1674             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1675            </m:mrow>
1676           </m:mtd>
1677          </m:mtr>
1678          <m:mtr>
1679           <m:mtd>
1680            <m:mrow>
1681             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1682             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1683             <xsl:apply-templates select="."/>
1684            </m:mrow>
1685           </m:mtd>
1686          </m:mtr>
1687    </xsl:when>
1688    <xsl:otherwise>
1689          <m:mtr>
1690           <m:mtd>
1691            <m:mrow>
1692             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1693            </m:mrow>
1694           </m:mtd>
1695          </m:mtr>
1696          <m:mtr>
1697           <m:mtd>
1698            <m:mrow>
1699             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1700             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1701             <xsl:apply-templates select="."/>
1702            </m:mrow>
1703           </m:mtd>
1704          </m:mtr>
1705     </xsl:otherwise>
1706    </xsl:choose>
1707          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1708 </xsl:template>
1709 -->
1710
1711 <!-- LAMBDA -->
1712
1713 <xsl:template match="m:lambda">
1714     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1715     <m:mrow m:xref="{@id}">
1716      <xsl:choose>
1717      <xsl:when test="$charlength >= $framewidth">
1718       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1719         <m:mtr>
1720           <m:mtd>
1721            <m:mrow>
1722             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1723             <xsl:apply-templates select="m:bvar"/>
1724            </m:mrow>
1725           </m:mtd>
1726          </m:mtr>
1727        <m:mtr>
1728         <m:mtd>
1729          <m:mrow>
1730           <m:mo>.</m:mo>
1731           <xsl:apply-templates select="*[position()=2]"/>
1732          </m:mrow>
1733         </m:mtd>
1734        </m:mtr>
1735       </m:mtable>
1736      </xsl:when>
1737      <xsl:otherwise>
1738       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1739       <xsl:apply-templates select="m:bvar/m:ci"/>
1740       <m:mo>:</m:mo>
1741       <xsl:apply-templates select="m:bvar/m:type"/>
1742       <m:mo>.</m:mo>
1743       <xsl:apply-templates select="*[position()=2]"/>
1744      </xsl:otherwise>
1745      </xsl:choose>
1746     </m:mrow>
1747 </xsl:template>
1748
1749 <!-- *********************************** -->
1750 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1751 <!-- *********************************** -->
1752
1753 <!-- Logic -->
1754
1755 <xsl:template match = "m:apply[m:eq[1]]">
1756  <xsl:variable name="charlength">
1757   <xsl:apply-templates select="*[1]" mode="charcount"/>
1758  </xsl:variable>
1759  <xsl:choose>
1760   <xsl:when test="$charlength >= $framewidth">
1761    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1762     <xsl:if test="@id">
1763      <xsl:attribute name="m:xref">
1764       <xsl:value-of select="@id"/>
1765      </xsl:attribute>
1766     </xsl:if>    
1767     <m:mtr>
1768      <m:mtd>
1769       <m:mrow>
1770        <m:mo stretchy="false">(</m:mo>
1771        <xsl:apply-templates select="*[position()=2]"/>
1772       </m:mrow>
1773      </m:mtd>
1774     </m:mtr>
1775     <xsl:for-each select = "*[position()>2]">
1776      <m:mtr>
1777       <m:mtd>
1778        <m:mrow>
1779         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1780         <m:mo>
1781          <xsl:if test="m:in/@id">
1782           <xsl:attribute name="m:xref">
1783            <xsl:value-of select="m:in/@id"/>
1784           </xsl:attribute>
1785          </xsl:if>=</m:mo>
1786         <xsl:apply-templates select="."/>
1787        </m:mrow>
1788       </m:mtd>
1789      </m:mtr>
1790     </xsl:for-each>
1791     <m:mtr>
1792      <m:mtd>
1793       <m:mrow>
1794        <m:mo stretchy="false">)</m:mo>
1795       </m:mrow>
1796      </m:mtd>
1797     </m:mtr>
1798    </m:mtable>
1799   </xsl:when>
1800   <xsl:otherwise>
1801    <xsl:apply-imports/>
1802   </xsl:otherwise>
1803  </xsl:choose>
1804 </xsl:template>
1805
1806
1807 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1808           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1809           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1810           |m:prsubset|m:setdiff[1]]">
1811  <xsl:variable name="symbol">
1812   <xsl:choose>
1813    <xsl:when test="m:and[1]">
1814     <xsl:value-of select="'&#8743;'"/>
1815    </xsl:when>
1816    <xsl:when test="m:or[1]">
1817     <xsl:value-of select="'&#8744;'"/>
1818    </xsl:when>
1819    <xsl:when test="m:geq[1]">
1820     <xsl:value-of select="'&#8805;'"/>
1821    </xsl:when>
1822    <xsl:when test="m:leq[1]">
1823     <xsl:value-of select="'&#8804;'"/>
1824    </xsl:when>
1825    <xsl:when test="m:gt[1]">
1826     <xsl:value-of select="'&#62;'"/>
1827    </xsl:when>
1828    <xsl:when test="m:lt[1]">
1829     <xsl:value-of select="'&#60;&#32;'"/>
1830    </xsl:when>
1831    <xsl:when test="m:eq[1]">
1832     <xsl:value-of select="'&#61;'"/>
1833    </xsl:when>
1834    <xsl:when test="m:in[1]">
1835     <xsl:value-of select="'&#x02208;'"/>
1836    </xsl:when>
1837    <xsl:when test="m:subset[1]">
1838     <xsl:value-of select="'&#x02286;'"/>
1839    </xsl:when>
1840    <xsl:when test="m:prsubset[1]">
1841     <xsl:value-of select="'&#x02282;'"/>
1842    </xsl:when>
1843    <xsl:when test="m:intersect[1]">
1844     <xsl:value-of select="'&#x022C2;'"/>
1845    </xsl:when>
1846    <xsl:when test="m:union[1]">
1847     <xsl:value-of select="'&#x022C3;'"/>
1848    </xsl:when>
1849    <xsl:when test="m:setdiff[1]">
1850     <xsl:value-of select="'&#x02216;'"/>
1851    </xsl:when>
1852   </xsl:choose>
1853  </xsl:variable>
1854  <xsl:variable name="charlength">
1855   <xsl:apply-templates select="*[1]" mode="charcount"/>
1856  </xsl:variable>
1857  <xsl:choose>
1858   <xsl:when test="$charlength >= $framewidth">
1859    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1860     <xsl:if test="@id">
1861      <xsl:attribute name="m:xref">
1862       <xsl:value-of select="@id"/>
1863      </xsl:attribute>
1864     </xsl:if>    
1865     <m:mtr>
1866      <m:mtd>
1867       <m:mrow>
1868        <m:mo stretchy="false">(</m:mo>
1869        <xsl:apply-templates select="*[position()=2]"/>
1870       </m:mrow>
1871      </m:mtd>
1872     </m:mtr>
1873     <xsl:for-each select = "*[position()>2]">
1874      <m:mtr>
1875       <m:mtd>
1876        <m:mrow>
1877         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1878         <m:mo>
1879          <xsl:if test="*[1]/@id">
1880           <xsl:attribute name="m:xref">
1881            <xsl:value-of select="*[1]/@id"/>
1882           </xsl:attribute>
1883          </xsl:if><xsl:value-of select="$symbol"/></m:mo>
1884         <xsl:apply-templates select="."/>
1885        </m:mrow>
1886       </m:mtd>
1887      </m:mtr>
1888     </xsl:for-each>
1889     <m:mtr>
1890      <m:mtd>
1891       <m:mrow>
1892        <m:mo stretchy="false">)</m:mo>
1893       </m:mrow>
1894      </m:mtd>
1895     </m:mtr>
1896    </m:mtable>
1897   </xsl:when>
1898   <xsl:otherwise>
1899    <xsl:apply-imports/>
1900   </xsl:otherwise>
1901  </xsl:choose>
1902 </xsl:template>
1903
1904 <xsl:template match = "m:set">
1905  <xsl:choose>
1906   <xsl:when test="count(child::*) = 0">
1907    <m:mi>
1908     <xsl:if test="@id">
1909      <xsl:attribute name="m:xref">
1910       <xsl:value-of select="@id"/>
1911      </xsl:attribute>
1912     </xsl:if>&#x02205;</m:mi>
1913   </xsl:when>
1914   <xsl:otherwise>
1915    <xsl:variable name="charlength">
1916     <xsl:apply-templates select="*[1]" mode="charcount"/>
1917    </xsl:variable>
1918    <xsl:choose>
1919     <xsl:when test="$charlength >= $framewidth">
1920      <xsl:choose>
1921       <xsl:when test="name(*[1]) = 'm:bvar'">
1922        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1923         <m:mtr>
1924          <m:mtd>
1925           <m:mrow>
1926            <m:mo stretchy="false">
1927             <xsl:if test="@id">
1928              <xsl:attribute name="m:xref">
1929               <xsl:value-of select="@id"/>
1930              </xsl:attribute>
1931             </xsl:if>{</m:mo>
1932            <xsl:apply-templates select="*[position()=1]"/>
1933           </m:mrow>
1934          </m:mtd>
1935         </m:mtr>
1936         <m:mtr>
1937          <m:mtd>
1938           <m:mrow>
1939            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1940            <m:mo stretchy="false">|</m:mo>
1941            <xsl:apply-templates select="m:condition/*[1]"/>
1942           </m:mrow>
1943          </m:mtd>
1944         </m:mtr>
1945         <m:mtr>
1946          <m:mtd>
1947           <m:mrow>
1948            <m:mo stretchy="false">
1949             <xsl:if test="@id">
1950              <xsl:attribute name="m:xref">
1951               <xsl:value-of select="@id"/>
1952              </xsl:attribute>
1953             </xsl:if>}</m:mo>
1954           </m:mrow>
1955          </m:mtd>
1956         </m:mtr>
1957        </m:mtable>
1958       </xsl:when>
1959       <xsl:otherwise>
1960        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1961         <m:mtr>
1962          <m:mtd>
1963           <m:mrow>
1964            <m:mo stretchy="false">
1965             <xsl:if test="@id">
1966              <xsl:attribute name="m:xref">
1967               <xsl:value-of select="@id"/>
1968              </xsl:attribute>
1969             </xsl:if>{</m:mo>
1970            <xsl:apply-templates select="*[position()=1]"/>
1971            <xsl:if test="position() != last()">
1972             <mo>,</mo>
1973            </xsl:if>
1974           </m:mrow>
1975          </m:mtd>
1976         </m:mtr>
1977         <xsl:for-each select = "*[position()>2]">
1978          <m:mtr>
1979           <m:mtd>
1980            <m:mrow>
1981             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1982             <xsl:apply-templates select="."/>
1983             <xsl:if test="position() != last()">
1984              <mo>,</mo>
1985             </xsl:if>
1986            </m:mrow>
1987           </m:mtd>
1988          </m:mtr>
1989         </xsl:for-each>
1990         <m:mtr>
1991          <m:mtd>
1992           <m:mrow>
1993            <m:mo stretchy="false">
1994             <xsl:if test="@id">
1995              <xsl:attribute name="m:xref">
1996               <xsl:value-of select="@id"/>
1997              </xsl:attribute>
1998             </xsl:if>}</m:mo>
1999           </m:mrow>
2000          </m:mtd>
2001         </m:mtr>
2002        </m:mtable>
2003       </xsl:otherwise>
2004      </xsl:choose>
2005     </xsl:when>
2006     <xsl:otherwise>
2007      <xsl:apply-imports/>
2008     </xsl:otherwise>
2009    </xsl:choose>
2010   </xsl:otherwise>
2011  </xsl:choose>
2012 </xsl:template>      
2013
2014 <xsl:template match = "m:apply[m:card[1]]">
2015   <m:mfenced open="|" close="|" stretchy="false">
2016     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
2017       <xsl:attribute name="m:xref">
2018         <xsl:value-of select="@id"/>
2019       </xsl:attribute>
2020     </xsl:if>
2021   <xsl:apply-templates select="*[2]"/>
2022   </m:mfenced>
2023 </xsl:template>
2024
2025
2026 <!--**********************-->
2027 <!--       COUNTING       -->
2028 <!--**********************-->
2029
2030 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
2031  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
2032  |m:plus|m:minus|m:times" mode="charcount">
2033 <xsl:param name="incurrent_length" select="0"/> 
2034     <xsl:choose>
2035     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
2036      <xsl:variable name="siblength">
2037       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2038        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2039       </xsl:apply-templates>
2040      </xsl:variable>
2041      <xsl:choose>
2042      <xsl:when test="string($siblength) = &quot;&quot;">
2043       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2044      </xsl:when>
2045      <xsl:otherwise>
2046       <xsl:value-of select="number($siblength)"/>
2047      </xsl:otherwise>
2048      </xsl:choose>
2049     </xsl:when>
2050     <xsl:otherwise>
2051      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2052     </xsl:otherwise>
2053     </xsl:choose>
2054 </xsl:template>
2055
2056 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2057 <xsl:param name="incurrent_length" select="0"/> 
2058 <xsl:param name="nosibling" select="0"/>
2059     <xsl:choose>
2060     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2061      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
2062      <xsl:choose>
2063      <xsl:when test="string($siblength) = &quot;&quot;">
2064       <xsl:value-of select="$incurrent_length + string-length()"/>
2065      </xsl:when>
2066      <xsl:otherwise>
2067       <xsl:value-of select="number($siblength)"/>
2068      </xsl:otherwise>
2069      </xsl:choose>
2070     </xsl:when>
2071     <xsl:otherwise>
2072      <xsl:value-of select="$incurrent_length + string-length()"/>
2073     </xsl:otherwise>
2074     </xsl:choose>
2075 </xsl:template> 
2076
2077 <xsl:template match="*" mode="charcount">
2078 <xsl:param name="incurrent_length" select="0"/>
2079 <xsl:param name="nosibling" select="0"/>
2080  <xsl:choose>
2081   <xsl:when test="count(child::*) = 0">
2082    <xsl:value-of select="$incurrent_length"/>
2083   </xsl:when>
2084   <xsl:otherwise>
2085     <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>
2086     <xsl:choose>
2087     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
2088      <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>
2089      <xsl:choose>
2090      <xsl:when test="string($siblength) = &quot;&quot;">
2091       <xsl:value-of select="number($childlength)"/>
2092      </xsl:when>
2093      <xsl:otherwise>
2094       <xsl:value-of select="number($siblength)"/>
2095      </xsl:otherwise>
2096      </xsl:choose>
2097     </xsl:when>
2098     <xsl:otherwise>
2099      <xsl:value-of select="number($childlength)"/>
2100     </xsl:otherwise>
2101     </xsl:choose>
2102   </xsl:otherwise>
2103  </xsl:choose>
2104 </xsl:template>
2105
2106 </xsl:stylesheet>