]> matita.cs.unibo.it Git - helm.git/blob - helm/style/mmlextension.xsl
Requires and Provides now fixed
[helm.git] / helm / style / mmlextension.xsl
1 <?xml version="1.0"?>
2
3 <!--***********************************************************************--> 
4 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
5 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
6 <!-- Revised: March 3 2000, Irene Schena                                   -->
7 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
8 <!-- Revised: March 21 2000, Irene Schena                                  -->
9 <!--***********************************************************************--> 
10
11 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
12                               xmlns:m="http://www.w3.org/1998/Math/MathML"
13                               xmlns:helm="http://www.cs.unibo.it/helm">
14
15 <xsl:import href="mml2mmlv1_0.xsl"/>
16
17 <!--***********************************************************************-->
18 <!-- Parameter affecting line-breaking                                     -->
19 <!--***********************************************************************-->
20
21 <xsl:variable name="framewidth" select="35"/>
22
23 <!--***********************************************************************-->
24 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
25 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
26 <!-- sono i termini: la presentation per un termine e' generata come primo -->
27 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
28 <!-- nel secondo figlio di semantics, annotation-xml                       -->
29 <!--***********************************************************************-->
30
31 <!--**********************-->
32 <!--        OBJECTS       -->
33 <!--**********************-->
34
35 <xsl:template match="/">
36  <xsl:processing-instruction name="cocoon-format">type="text/xhtml"</xsl:processing-instruction>
37  <xsl:apply-templates select="*"/>
38 </xsl:template>
39
40 <!-- DEFINITION -->
41
42 <xsl:template match="Definition">
43     <m:math>
44      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
45       <m:mtr>
46        <m:mtd>
47         <m:mrow>
48          <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>
49         </m:mrow>
50        </m:mtd>
51       </m:mtr>
52       <m:mtr>
53        <m:mtd>
54         <m:mrow>
55          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
56          <xsl:apply-templates select="type/*[1]"/>
57         </m:mrow>
58        </m:mtd>
59       </m:mtr>
60       <m:mtr>
61        <m:mtd>
62         <m:mrow>
63          <m:mtext>AS</m:mtext>
64         </m:mrow>
65        </m:mtd>
66       </m:mtr>
67       <m:mtr>
68        <m:mtd>
69         <m:mrow>
70          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
71          <xsl:apply-templates select="body/*[1]"/>
72         </m:mrow>
73        </m:mtd>
74       </m:mtr>
75      </m:mtable>
76     </m:math>
77 </xsl:template>
78
79 <!-- AXIOM -->
80
81 <xsl:template match="Axiom">
82     <m:math>
83      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
84       <m:mtr>
85        <m:mtd>
86         <m:mrow>
87          <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>
88         </m:mrow>
89        </m:mtd>
90       </m:mtr>
91       <m:mtr>
92        <m:mtd>
93         <m:mrow>
94          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
95          <xsl:apply-templates select="type/*[1]"/>
96         </m:mrow>
97        </m:mtd>
98       </m:mtr>
99      </m:mtable>
100     </m:math>
101 </xsl:template>
102
103 <!-- UNFINISHED PROOF -->
104
105 <xsl:template match="CurrentProof">
106     <m:math>
107      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
108       <m:mtr>
109        <m:mtd>
110         <m:mrow>
111          <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>
112         </m:mrow>
113        </m:mtd>
114       </m:mtr>
115       <m:mtr>
116        <m:mtd>
117         <m:mrow>
118          <m:mtext>THESIS:</m:mtext>
119         </m:mrow>
120        </m:mtd>
121       </m:mtr>
122       <m:mtr>
123        <m:mtd>
124         <m:mrow>
125          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
126          <xsl:apply-templates select="type/*[1]"/>
127         </m:mrow>
128        </m:mtd>
129       </m:mtr>
130       <m:mtr>
131        <m:mtd>
132         <m:mrow>
133          <m:mtext>CONJECTURES:</m:mtext>
134         </m:mrow>
135        </m:mtd>
136       </m:mtr>
137       <xsl:for-each select="Conjecture">
138       <m:mtr>
139        <m:mtd>
140         <m:mrow>
141          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
142          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
143          <xsl:apply-templates select="./*[1]"/>
144         </m:mrow>
145        </m:mtd>
146       </m:mtr>
147       </xsl:for-each>
148       <m:mtr>
149        <m:mtd>
150         <m:mrow>
151          <m:mtext>CORRESPONDING PROOF:</m:mtext>
152         </m:mrow>
153        </m:mtd>
154       </m:mtr>
155       <m:mtr>
156        <m:mtd>
157         <m:mrow>
158          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
159          <xsl:apply-templates select="body/*[1]"/>
160         </m:mrow>
161        </m:mtd>
162       </m:mtr>
163      </m:mtable>
164     </m:math>
165 </xsl:template>
166
167 <!-- MUTUAL INDUCTIVE DEFINITION -->
168
169 <xsl:template match="InductiveDefinition">
170     <m:math>
171      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
172      <xsl:for-each select="InductiveType">
173       <m:mtr>
174        <m:mtd>
175         <m:mrow>
176          <xsl:choose>
177          <xsl:when test="position() = 1">
178           <xsl:choose>
179           <xsl:when test="string(./@inductive) = &quot;true&quot;">
180            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
181           </xsl:when>
182           <xsl:otherwise>
183            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
184           </xsl:otherwise>
185           </xsl:choose>  
186          </xsl:when>
187          <xsl:otherwise>
188           <m:mtext>AND</m:mtext>
189          </xsl:otherwise>
190          </xsl:choose>
191          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
192          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
193         </m:mrow>
194        </m:mtd>
195       </m:mtr>
196       <m:mtr>
197        <m:mtd>
198         <m:mrow> 
199          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
200          <m:mtext>[</m:mtext>
201          <xsl:choose>
202          <xsl:when test="string(../Param) != &quot;&quot;">         
203           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
204            <xsl:for-each select="../Param">
205             <m:mtr>
206              <m:mtd>
207               <m:mrow>   
208                <m:mi><xsl:value-of select="./@name"/></m:mi>
209                <m:mo>:</m:mo>
210                <xsl:apply-templates select="*"/>
211               </m:mrow>
212              </m:mtd>
213             </m:mtr>
214            </xsl:for-each>
215             <m:mtr>
216              <m:mtd>
217               <m:mrow>
218                <m:mtext>]</m:mtext>
219               </m:mrow>
220              </m:mtd>
221             </m:mtr>
222           </m:mtable>
223          </xsl:when>
224          <xsl:otherwise>
225           <m:mtext>]</m:mtext>
226          </xsl:otherwise>
227          </xsl:choose>
228         </m:mrow>
229        </m:mtd>
230       </m:mtr>
231       <m:mtr>
232        <m:mtd>
233         <m:mrow>
234          <m:mtext>OF ARITY</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          <xsl:apply-templates select="./arity/*[1]"/>
243         </m:mrow>
244        </m:mtd>
245       </m:mtr>
246       <m:mtr>
247        <m:mtd>
248         <m:mrow>
249          <m:mtext>BUILT FROM</m:mtext>
250         </m:mrow>
251        </m:mtd>
252       </m:mtr>
253       <xsl:for-each select="./Constructor">
254       <m:mtr>
255        <m:mtd>
256         <m:mrow>
257          <xsl:choose>
258          <xsl:when test="position() = 1">
259           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
260          </xsl:when>
261          <xsl:otherwise>
262           <m:mtext>|</m:mtext>
263           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
264          </xsl:otherwise>
265          </xsl:choose>
266          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
267          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
268          <xsl:apply-templates select="./*[1]"/>
269         </m:mrow>
270        </m:mtd>
271       </m:mtr>
272       </xsl:for-each>
273      </xsl:for-each>
274      </m:mtable>
275     </m:math>
276 </xsl:template>
277
278 <!-- VARIABLE -->
279
280 <xsl:template match="Variable">
281     <m:math>
282      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
283       <m:mtr>
284        <m:mtd>
285         <m:mrow>
286          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
287         </m:mrow>
288        </m:mtd>
289       </m:mtr>
290       <m:mtr>
291        <m:mtd>
292         <m:mrow>
293          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
294          <xsl:apply-templates select="type/*[1]"/>
295         </m:mrow>
296        </m:mtd>
297       </m:mtr>
298      </m:mtable>
299     </m:math>
300 </xsl:template>
301
302 <!--**********************-->
303 <!--        TERMS         -->
304 <!--**********************-->
305
306 <xsl:template match="m:bvar">
307  <xsl:choose>
308   <xsl:when test="m:type">
309    <xsl:variable name="charlength">
310     <xsl:apply-templates select="m:ci" mode="charcount"/>
311    </xsl:variable>
312    <xsl:choose>
313     <xsl:when test="$charlength >= $framewidth">
314      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
315       <m:mtr>
316        <m:mtd>
317         <xsl:apply-templates select="m:ci"/>
318         <m:mo>:</m:mo>
319        </m:mtd>
320       </m:mtr>
321       <m:mtr>
322        <m:mtd>
323          <xsl:apply-templates select="m:type"/>
324        </m:mtd>
325       </m:mtr>
326      </m:mtable>
327     </xsl:when>
328     <xsl:otherwise>
329      <xsl:apply-templates select="m:ci"/>
330      <m:mo>:</m:mo>
331      <xsl:apply-templates select="m:type"/>
332     </xsl:otherwise>
333    </xsl:choose>
334   </xsl:when>
335   <xsl:otherwise>
336    <xsl:apply-templates select="m:ci"/>
337   </xsl:otherwise>
338  </xsl:choose>
339 </xsl:template>
340
341
342 <!-- CSYMBOL -->
343
344 <xsl:template match="m:apply[m:csymbol]">
345     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
346     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
347     <m:mrow>
348      <xsl:if test="@helm:xref">
349       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
350      </xsl:if>
351      <xsl:choose>
352       <xsl:when test="$name='forall'">
353        <xsl:choose>
354        <xsl:when test="$charlength >= $framewidth">
355         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
356          <m:mtr>
357           <m:mtd>
358             <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
359             <xsl:apply-templates select="m:bvar"/>
360           </m:mtd>
361          </m:mtr>
362          <m:mtr>
363           <m:mtd>
364            <m:mrow>
365             <m:mo>.</m:mo>
366             <xsl:apply-templates select="*[position()=3]"/>
367            </m:mrow>
368           </m:mtd>
369          </m:mtr>
370         </m:mtable>
371        </xsl:when>
372        <xsl:otherwise>
373         <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
374         <xsl:apply-templates select="m:bvar/m:ci"/>
375         <m:mo>:</m:mo>
376         <xsl:apply-templates select="m:bvar/m:type"/>
377         <m:mo>.</m:mo>
378         <xsl:apply-templates select="*[position()=3]"/>
379        </xsl:otherwise>
380        </xsl:choose> 
381       </xsl:when>
382       <xsl:when test="$name='prod'">
383        <xsl:choose>
384        <xsl:when test="$charlength >= $framewidth">
385         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
386          <m:mtr>
387           <m:mtd>
388             <m:mo color="Blue">&#x03a0;</m:mo>
389             <xsl:apply-templates select="m:bvar"/>
390           </m:mtd>
391          </m:mtr>
392          <m:mtr>
393           <m:mtd>
394            <m:mrow>
395             <m:mo>.</m:mo>
396             <xsl:apply-templates select="*[position()=3]"/>
397            </m:mrow>
398           </m:mtd>
399          </m:mtr>
400         </m:mtable>
401        </xsl:when>
402        <xsl:otherwise>
403         <m:mo color="Blue">&#x03a0;</m:mo>
404         <xsl:apply-templates select="m:bvar/m:ci"/>
405         <m:mo>:</m:mo>
406         <xsl:apply-templates select="m:bvar/m:type"/>
407         <m:mo>.</m:mo>
408         <xsl:apply-templates select="*[position()=3]"/>
409        </xsl:otherwise>
410        </xsl:choose> 
411       </xsl:when>
412       <xsl:when test="$name='arrow'">
413        <xsl:choose>
414        <xsl:when test="$charlength >= $framewidth">
415         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
416          <m:mtr>
417           <m:mtd>
418            <m:mrow>
419             <m:mo stretchy="false">(</m:mo>
420             <xsl:apply-templates select="*[position()=2]"/>
421            </m:mrow>
422           </m:mtd>
423          </m:mtr>
424          <m:mtr>
425           <m:mtd>
426            <m:mrow>
427             <m:mo color="Blue">&#x2192;</m:mo>
428             <xsl:apply-templates select="*[position()=3]"/>
429            </m:mrow>
430           </m:mtd>
431          </m:mtr>
432          <m:mtr>
433           <m:mtd>
434            <m:mrow>
435             <m:mo stretchy="false">)</m:mo>
436            </m:mrow>
437           </m:mtd>
438          </m:mtr>
439         </m:mtable>
440        </xsl:when>
441        <xsl:otherwise>
442         <m:mo stretchy="false">(</m:mo>
443         <xsl:apply-templates select="*[position()=2]"/>
444         <m:mo color="Blue">&#x2192;</m:mo>
445         <xsl:apply-templates select="*[position()=3]"/>
446         <m:mo stretchy="false">)</m:mo>
447        </xsl:otherwise>
448        </xsl:choose>
449       </xsl:when>
450       <xsl:when test="$name='app'">
451        <xsl:choose>
452        <xsl:when test="$charlength >= $framewidth">
453         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
454          <m:mtr>
455           <m:mtd>
456            <m:mrow>
457             <m:mo stretchy="false">(</m:mo>
458             <xsl:apply-templates select="*[position()=2]"/>
459            </m:mrow>
460           </m:mtd>
461          </m:mtr>
462          <xsl:for-each select="*[position()>2]">
463          <m:mtr>
464           <m:mtd>
465            <m:mrow>
466             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
467             <xsl:apply-templates select="."/>
468            </m:mrow>
469           </m:mtd>
470          </m:mtr>
471          </xsl:for-each>
472          <m:mtr>
473           <m:mtd>
474            <m:mrow>
475             <m:mo stretchy="false">)</m:mo>
476            </m:mrow>
477           </m:mtd>
478          </m:mtr>
479         </m:mtable>
480        </xsl:when>
481        <xsl:otherwise>
482         <m:mo stretchy="false">(</m:mo>
483         <xsl:apply-templates select="*[position()=2]"/>
484         <xsl:for-each select="*[position()>2]">
485          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
486          <xsl:apply-templates select="."/>
487         </xsl:for-each>
488         <m:mo stretchy="false">)</m:mo>
489        </xsl:otherwise>
490        </xsl:choose>
491       </xsl:when>
492       <xsl:when test="$name='cast'">
493        <xsl:choose>
494        <xsl:when test="$charlength >= $framewidth">
495         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
496          <m:mtr>
497           <m:mtd>
498            <m:mrow>
499             <m:mo stretchy="false">(</m:mo>
500             <xsl:apply-templates select="*[position()=2]"/>
501            </m:mrow>
502           </m:mtd>
503          </m:mtr>
504          <m:mtr>
505           <m:mtd>
506            <m:mrow>
507             <m:mo color="Maroon">:></m:mo>
508             <xsl:apply-templates select="*[position()=3]"/>
509            </m:mrow>
510           </m:mtd>
511          </m:mtr>
512          <m:mtr>
513           <m:mtd>
514            <m:mrow>
515             <m:mo stretchy="false">)</m:mo>
516            </m:mrow>
517           </m:mtd>
518          </m:mtr>
519         </m:mtable>
520        </xsl:when>
521        <xsl:otherwise>
522         <m:mo stretchy="false">(</m:mo>
523         <xsl:apply-templates select="*[position()=2]"/>
524         <m:mo color="Maroon">:></m:mo>
525         <xsl:apply-templates select="*[position()=3]"/>
526         <m:mo stretchy="false">)</m:mo>
527        </xsl:otherwise>
528        </xsl:choose>
529       </xsl:when>
530       <xsl:when test="$name='Prop'">
531        <m:mo>Prop</m:mo>
532       </xsl:when>
533       <xsl:when test="$name='Set'">
534        <m:mo>Set</m:mo>
535       </xsl:when>
536       <xsl:when test="$name='Type'">
537        <m:mo>Type</m:mo>
538       </xsl:when>
539       <xsl:when test="$name='mutcase'">
540        <xsl:choose>
541        <xsl:when test="$charlength >= $framewidth">
542         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
543         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
544          <m:mtr>
545           <m:mtd>
546            <m:mrow>
547             <m:mo>&lt;</m:mo>
548             <xsl:apply-templates select="*[position()=2]"/>
549             <xsl:if test="$framewidth > $charlength">
550              <m:mo>&gt;</m:mo>
551              <m:mo>CASES</m:mo>
552              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
553              <xsl:apply-templates select="*[position()=3]"/>
554             </xsl:if>
555            </m:mrow>
556           </m:mtd>
557          </m:mtr>
558          <xsl:if test="$charlength >= $framewidth">
559          <m:mtr>
560           <m:mtd>
561            <m:mrow>
562             <m:mo>&gt;</m:mo>
563             <m:mo>CASES</m:mo>
564             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
565             <xsl:apply-templates select="*[position()=3]"/>
566            </m:mrow>
567           </m:mtd>
568          </m:mtr>
569          </xsl:if>
570          <m:mtr>
571           <m:mtd>
572            <m:mrow>
573             <m:mo>OF</m:mo>
574            </m:mrow>
575           </m:mtd>
576          </m:mtr>
577          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
578          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
579          <m:mtr>
580           <m:mtd>
581            <m:mrow>
582             <xsl:choose>
583             <xsl:when test="position() = 1">
584               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
585             </xsl:when>
586             <xsl:otherwise>
587              <m:mo stretchy="false">|</m:mo>
588             </xsl:otherwise>
589             </xsl:choose>
590             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
591             <xsl:apply-templates select="."/>
592             <xsl:if test="$framewidth > $charlength">
593              <m:mo color="Green">&#x21d2;</m:mo>
594              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
595             </xsl:if>
596            </m:mrow>
597           </m:mtd>
598          </m:mtr>
599          <xsl:if test="$charlength >= $framewidth">
600          <m:mtr>
601           <m:mtd>
602            <m:mrow>
603             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
604             <m:mo color="Green">&#x21d2;</m:mo>
605             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
606            </m:mrow>
607           </m:mtd>
608          </m:mtr>
609          </xsl:if>
610         </xsl:for-each>
611          <m:mtr>
612           <m:mtd>
613            <m:mrow>
614             <m:mo>END</m:mo>
615            </m:mrow>
616           </m:mtd>
617          </m:mtr>
618         </m:mtable>
619        </xsl:when>
620        <xsl:otherwise>
621         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
622         <m:mo>CASES</m:mo>
623         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
624         <xsl:apply-templates select="*[position()=3]"/>
625         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
626         <m:mo>OF</m:mo>
627         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
628          <xsl:choose>
629          <xsl:when test="position() != 1">
630           <m:mo stretchy="false">|</m:mo>
631          </xsl:when> 
632          </xsl:choose>
633          <xsl:apply-templates select="."/>
634          <m:mo color="Green">&#x21d2;</m:mo>
635          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
636         </xsl:for-each>
637         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
638         <m:mo>END</m:mo>
639        </xsl:otherwise>
640        </xsl:choose>
641       </xsl:when>
642       <xsl:when test="$name='fix'">
643        <xsl:choose>
644        <xsl:when test="$charlength >= $framewidth">
645         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
646          <m:mtr>
647           <m:mtd>
648            <m:mrow>
649             <m:mo>FIX</m:mo>
650             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
651             <m:mi><xsl:value-of select="m:ci"/></m:mi>
652             <m:mo stretchy="false">{</m:mo>
653            </m:mrow>
654           </m:mtd>
655          </m:mtr>
656          <m:mtr>
657           <m:mtd>
658            <m:mrow>
659             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
660             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
661             <xsl:for-each select="m:bvar"> 
662              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
663              <m:mtr>
664               <m:mtd>
665                <m:mrow>
666                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
667                 <m:mo>:</m:mo>
668                 <xsl:if test="$framewidth > $charlength">
669                  <xsl:apply-templates select="m:type"/>
670                 </xsl:if>
671                </m:mrow>
672               </m:mtd>
673              </m:mtr> 
674              <xsl:if test="$charlength >= $framewidth">
675              <m:mtr>
676               <m:mtd>
677                <m:mrow>
678                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
679                 <xsl:apply-templates select="m:type"/>
680                </m:mrow>
681               </m:mtd>
682              </m:mtr>
683              </xsl:if>
684              <m:mtr>
685               <m:mtd>
686                <m:mrow>
687                 <m:mo>:=</m:mo>
688                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
689                </m:mrow>
690               </m:mtd>
691              </m:mtr> 
692             </xsl:for-each>
693             </m:mtable>
694            </m:mrow>
695           </m:mtd>
696          </m:mtr>
697          <m:mtr>
698           <m:mtd>
699            <m:mrow>
700             <m:mo stretchy="false">}</m:mo>
701            </m:mrow>
702           </m:mtd>
703          </m:mtr>
704         </m:mtable>
705        </xsl:when>
706        <xsl:otherwise>
707         <m:mo>FIX</m:mo>
708         <m:mi><xsl:value-of select="m:ci"/></m:mi>
709         <m:mo stretchy="false">{</m:mo>
710         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
711         <xsl:for-each select="m:bvar"> 
712          <m:mtr>
713           <m:mtd>
714            <m:mrow>
715             <m:mi><xsl:value-of select="m:ci"/></m:mi>
716             <m:mo>:</m:mo>
717             <xsl:apply-templates select="m:type"/>
718             <m:mo>:=</m:mo>
719             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
720             <xsl:if test="position()=last()">
721              <m:mo stretchy="false">}</m:mo>
722             </xsl:if>
723            </m:mrow>
724           </m:mtd>
725          </m:mtr>
726          </xsl:for-each>
727         </m:mtable>
728        </xsl:otherwise>
729        </xsl:choose>
730       </xsl:when>
731       <xsl:when test="$name='cofix'">
732        <xsl:choose>
733        <xsl:when test="$charlength >= $framewidth">
734         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
735          <m:mtr>
736           <m:mtd>
737            <m:mrow>
738             <m:mo>COFIX</m:mo>
739             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
740             <m:mi><xsl:value-of select="m:ci"/></m:mi>
741             <m:mo stretchy="false">{</m:mo>
742            </m:mrow>
743           </m:mtd>
744          </m:mtr>
745          <m:mtr>
746           <m:mtd>
747            <m:mrow>
748             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
749             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
750             <xsl:for-each select="m:bvar">
751              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable> 
752              <m:mtr>
753               <m:mtd>
754                <m:mrow>
755                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
756                 <m:mo>:</m:mo>
757                 <xsl:if test="$framewidth > $charlength">
758                  <xsl:apply-templates select="m:type"/>
759                 </xsl:if>
760                </m:mrow>
761               </m:mtd>
762              </m:mtr> 
763              <xsl:if test="$charlength >= $framewidth">
764              <m:mtr>
765               <m:mtd>
766                <m:mrow>
767                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
768                 <xsl:apply-templates select="m:type"/>
769                </m:mrow>
770               </m:mtd>
771              </m:mtr>
772              </xsl:if>
773              <m:mtr>
774               <m:mtd>
775                <m:mrow>
776                 <m:mo>:=</m:mo>
777                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
778                </m:mrow>
779               </m:mtd>
780              </m:mtr>
781             </xsl:for-each>
782             </m:mtable>
783            </m:mrow>
784           </m:mtd>
785          </m:mtr>
786          <m:mtr>
787           <m:mtd>
788            <m:mrow>
789             <m:mo stretchy="false">}</m:mo>
790            </m:mrow>
791           </m:mtd>
792          </m:mtr>
793         </m:mtable>
794        </xsl:when>
795        <xsl:otherwise>
796         <m:mo>COFIX</m:mo>
797         <m:mi><xsl:value-of select="m:ci"/></m:mi>
798         <m:mo stretchy="false">{</m:mo>
799         <m:mtable align="baseline 1" equalrows="false" columnalign="left">  
800         <xsl:for-each select="m:bvar"> 
801          <m:mtr>
802           <m:mtd>
803            <m:mrow>
804             <m:mi><xsl:value-of select="m:ci"/></m:mi>
805             <m:mo>:</m:mo>
806             <xsl:apply-templates select="m:type"/>
807             <m:mo>:=</m:mo>
808             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
809             <xsl:if test="position()=last()">
810              <m:mo stretchy="false">}</m:mo>
811             </xsl:if>
812            </m:mrow>
813           </m:mtd>
814          </m:mtr>
815          </xsl:for-each>
816         </m:mtable>
817        </xsl:otherwise>
818        </xsl:choose>
819       </xsl:when>
820       <!-- ***************************************** -->
821       <!-- *********** PROOF ELEMENTS ************** -->
822       <!-- ***************************************** -->
823       <xsl:when test="$name='proof'">
824         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
825          <m:mtr>
826           <m:mtd>
827            <m:mrow>
828             <xsl:apply-templates select="*[position()=2]"/>
829            </m:mrow>
830           </m:mtd>
831          </m:mtr>
832          <m:mtr>
833           <m:mtd>
834            <m:mrow>
835             <m:mtext color="Maroon">we proved </m:mtext>
836             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
837             <xsl:apply-templates select="*[position()=3]"/>
838            </m:mrow>
839           </m:mtd>
840          </m:mtr>
841         </m:mtable>
842       </xsl:when>
843       <xsl:when test="$name='letin'">
844         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
845          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
846          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
847          <m:mtr>
848           <m:mtd>
849            <m:mrow>
850             <xsl:apply-templates select="."/>
851            </m:mrow>
852           </m:mtd>
853          </m:mtr>
854          </xsl:for-each>
855          <m:mtr>
856           <m:mtd>
857            <m:mrow>
858             <xsl:apply-templates select="*[position()=last()]"/>
859            </m:mrow>
860           </m:mtd>
861          </m:mtr>
862         </m:mtable>
863       </xsl:when>
864       <xsl:when test="$name='let'">
865        <m:mtext>(</m:mtext>
866        <xsl:apply-templates select="m:ci"/>
867        <m:mtext>) </m:mtext>
868        <xsl:apply-templates select="*[3]"/>
869       </xsl:when>
870       <xsl:when test="$name='thread'">
871         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
872          <m:mtr>
873           <m:mtd>
874            <m:mrow>
875             <xsl:choose>
876              <xsl:when test="name(*[last()])='m:apply'">
877               <xsl:apply-templates select="*[last()]"/>
878              </xsl:when>
879              <xsl:otherwise>
880               <m:mtext>Consider </m:mtext>
881               <xsl:apply-templates select="*[last()]"/>
882              </xsl:otherwise>
883             </xsl:choose>
884            </m:mrow>
885           </m:mtd>
886          </m:mtr>
887          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
888         </m:mtable>
889       </xsl:when> 
890       <xsl:when test="$name='rewrite_and_apply'">
891         <m:mtable>
892          <m:mtr>
893           <m:mtd>
894            <m:mrow>
895             <m:mtext>Rewrite</m:mtext>
896             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
897             <xsl:apply-templates select="*[2]/*[2]"/>
898             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
899             <m:mtext>with</m:mtext>
900             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
901             <xsl:apply-templates select="*[2]/*[3]"/>
902             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
903             <m:mtext>by</m:mtext>
904             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
905             <xsl:apply-templates select="*[2]/*[4]"/>
906             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
907             <m:mtext>in</m:mtext>
908             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
909             <xsl:apply-templates select="*[3]"/>
910             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
911             <m:mtext>and apply to</m:mtext>
912             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
913             <xsl:apply-templates select="*[position()>3]"/>
914            </m:mrow>
915           </m:mtd>
916          </m:mtr>
917        </m:mtable>
918       </xsl:when> 
919       <xsl:when test="$name='and_ind'">
920         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
921          <m:mtr>
922           <m:mtd>
923            <m:mrow>
924             <xsl:choose>
925              <xsl:when test="name(*[2])='m:apply'">
926               <xsl:apply-templates select="*[2]"/>
927              </xsl:when>
928              <xsl:otherwise>
929               <m:mtext>Consider </m:mtext>
930               <xsl:apply-templates select="*[2]"/>
931              </xsl:otherwise>
932             </xsl:choose>
933            </m:mrow>
934           </m:mtd>
935          </m:mtr>
936          <m:mtr>
937           <m:mtd>
938            <m:mtext>In particular, we have</m:mtext>
939           </m:mtd>
940          </m:mtr>
941          <m:mtr>
942           <m:mtd>
943            <m:mrow>
944             <m:mtext>(</m:mtext>
945             <xsl:apply-templates select="*[3]"/>
946             <m:mtext>)</m:mtext>
947             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
948             <xsl:apply-templates select="*[4]"/>
949             </m:mrow>
950           </m:mtd>
951          </m:mtr>
952          <m:mtr>
953           <m:mtd>
954            <m:mrow>
955             <m:mtext>(</m:mtext>
956             <xsl:apply-templates select="*[5]"/>
957             <m:mtext>)</m:mtext>
958             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
959             <xsl:apply-templates select="*[6]"/>
960             </m:mrow>
961           </m:mtd>
962          </m:mtr>
963          <m:mtr>
964           <m:mtd>
965            <m:mrow>
966             <xsl:apply-templates select="*[7]"/>
967            </m:mrow>
968           </m:mtd>
969          </m:mtr>
970         </m:mtable>
971       </xsl:when>
972       <xsl:when test="$name='or_ind'">
973         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
974          <m:mtr>
975           <m:mtd>
976            <m:mrow>
977             <xsl:choose>
978              <xsl:when test="name(*[2])='m:apply'">
979               <xsl:apply-templates select="*[2]"/>
980              </xsl:when>
981              <xsl:otherwise>
982               <m:mtext>Consider</m:mtext>
983               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
984               <xsl:apply-templates select="*[2]"/>
985              </xsl:otherwise>
986             </xsl:choose>
987            </m:mrow>
988           </m:mtd>
989          </m:mtr>
990          <m:mtr>
991           <m:mtd>
992            <m:mtext>We prove</m:mtext>
993            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
994            <xsl:apply-templates select="*[3]"/>
995            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
996            <m:mtext>by cases:</m:mtext>
997           </m:mtd>
998          </m:mtr>
999          <m:mtr>
1000           <m:mtd>
1001            <m:mrow>
1002             <m:mtext>*</m:mtext>
1003             <xsl:apply-templates select="*[4]"/>
1004            </m:mrow>
1005           </m:mtd>
1006          </m:mtr>
1007          <m:mtr>
1008           <m:mtd>
1009            <m:mrow>
1010             <m:mtext>*</m:mtext>
1011             <xsl:apply-templates select="*[5]"/>
1012            </m:mrow>
1013           </m:mtd>
1014          </m:mtr>
1015         </m:mtable>
1016       </xsl:when>
1017       <xsl:otherwise>
1018        <m:ci>ERROR</m:ci>
1019       </xsl:otherwise>
1020      </xsl:choose>
1021     </m:mrow>
1022 </xsl:template>
1023
1024 <xsl:template match="*" mode="thread">
1025  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1026  <xsl:choose>
1027   <xsl:when test="$name='rw_step'">
1028          <m:mtr>
1029           <m:mtd>
1030            <m:mrow>
1031             <m:mtext>Rewrite</m:mtext>
1032             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1033             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1034             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1035             <m:mtext>with</m:mtext>
1036             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1037             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1038             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1039             <m:mtext>by</m:mtext>
1040             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1041             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1042            </m:mrow>
1043           </m:mtd>
1044          </m:mtr>
1045          <m:mtr>
1046           <m:mtd>
1047            <m:mrow>
1048             <m:mtext color="Maroon">we get</m:mtext>
1049             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1050             <xsl:apply-templates select="."/>
1051            </m:mrow>
1052           </m:mtd>
1053          </m:mtr>
1054    </xsl:when>
1055    <xsl:otherwise>
1056          <m:mtr>
1057           <m:mtd>
1058            <m:mrow>
1059             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1060            </m:mrow>
1061           </m:mtd>
1062          </m:mtr>
1063          <m:mtr>
1064           <m:mtd>
1065            <m:mrow>
1066             <m:mtext color="Maroon">we get</m:mtext>
1067             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1068             <xsl:apply-templates select="."/>
1069            </m:mrow>
1070           </m:mtd>
1071          </m:mtr>
1072     </xsl:otherwise>
1073    </xsl:choose>
1074          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1075 </xsl:template>
1076
1077
1078 <!-- LAMBDA -->
1079
1080 <xsl:template match="m:lambda">
1081     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1082     <m:mrow helm:xref="{@helm:xref}">
1083      <xsl:choose>
1084      <xsl:when test="$charlength >= $framewidth">
1085       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1086         <m:mtr>
1087           <m:mtd>
1088             <m:mo color="Red">&#x03bb;</m:mo>
1089             <xsl:apply-templates select="m:bvar"/>
1090           </m:mtd>
1091          </m:mtr>
1092        <m:mtr>
1093         <m:mtd>
1094          <m:mrow>
1095           <m:mo>.</m:mo>
1096           <xsl:apply-templates select="*[position()=2]"/>
1097          </m:mrow>
1098         </m:mtd>
1099        </m:mtr>
1100       </m:mtable>
1101      </xsl:when>
1102      <xsl:otherwise>
1103       <m:mo color="Red">&#x03bb;</m:mo>
1104       <xsl:apply-templates select="m:bvar/m:ci"/>
1105       <m:mo>:</m:mo>
1106       <xsl:apply-templates select="m:bvar/m:type"/>
1107       <m:mo>.</m:mo>
1108       <xsl:apply-templates select="*[position()=2]"/>
1109      </xsl:otherwise>
1110      </xsl:choose>
1111     </m:mrow>
1112 </xsl:template>
1113
1114 <!-- *********************************** -->
1115 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1116 <!-- *********************************** -->
1117
1118 <!-- Logic -->
1119
1120 <xsl:template match = "m:apply[m:eq[1]]">
1121  <xsl:variable name="charlength">
1122   <xsl:apply-templates select="*[1]" mode="charcount"/>
1123  </xsl:variable>
1124  <xsl:choose>
1125   <xsl:when test="$charlength >= $framewidth">
1126    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1127     <xsl:if test="@helm:xref">
1128      <xsl:attribute name="helm:xref">
1129       <xsl:value-of select="@helm:xref"/>
1130      </xsl:attribute>
1131     </xsl:if>    
1132     <m:mtr>
1133      <m:mtd>
1134       <m:mo stretchy="false">(</m:mo>
1135       <xsl:apply-templates select="*[position()=2]"/>
1136      </m:mtd>
1137     </m:mtr>
1138     <xsl:for-each select = "*[position()>2]">
1139      <m:mtr>
1140       <m:mtd>
1141        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1142        <m:mo helm:xref="m:in/@helm:xref"> 
1143         =
1144        </m:mo>
1145        <xsl:apply-templates select="."/>
1146       </m:mtd>
1147      </m:mtr>
1148     </xsl:for-each>
1149     <m:mtr>
1150      <m:mtd>
1151       <m:mo stretchy="false">)</m:mo>
1152      </m:mtd>
1153     </m:mtr>
1154    </m:mtable>
1155   </xsl:when>
1156   <xsl:otherwise>
1157    <xsl:apply-imports/>
1158   </xsl:otherwise>
1159  </xsl:choose>
1160 </xsl:template>
1161
1162
1163 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1164           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1165           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1166           |m:prsubset|m:setdiff[1]]">
1167  <xsl:variable name="symbol">
1168   <xsl:choose>
1169    <xsl:when test="m:and[1]">
1170     <xsl:value-of select="'wedge'"/>
1171    </xsl:when>
1172    <xsl:when test="m:or[1]">
1173     <xsl:value-of select="'vee'"/>
1174    </xsl:when>
1175    <xsl:when test="m:geq[1]">
1176     <xsl:value-of select="'geq'"/>
1177    </xsl:when>
1178    <xsl:when test="m:leq[1]">
1179     <xsl:value-of select="'leq'"/>
1180    </xsl:when>
1181    <xsl:when test="m:gt[1]">
1182     <xsl:value-of select="'gt'"/>
1183    </xsl:when>
1184    <xsl:when test="m:lt[1]">
1185     <xsl:value-of select="'lt'"/>
1186    </xsl:when>
1187    <xsl:when test="m:eq[1]">
1188     <xsl:value-of select="'Equal'"/>
1189    </xsl:when>
1190    <xsl:when test="m:in[1]">
1191     <xsl:value-of select="'Element'"/>
1192    </xsl:when>
1193    <xsl:when test="m:subset[1]">
1194     <xsl:value-of select="'SubsetEqual'"/>
1195    </xsl:when>
1196    <xsl:when test="m:prsubset[1]">
1197     <xsl:value-of select="'subset'"/>
1198    </xsl:when>
1199    <xsl:when test="m:intersect[1]">
1200     <xsl:value-of select="'Intersection'"/>
1201    </xsl:when>
1202    <xsl:when test="m:union[1]">
1203     <xsl:value-of select="'Union'"/>
1204    </xsl:when>
1205    <xsl:when test="m:setdiff[1]">
1206     <xsl:value-of select="'Backslash'"/>
1207    </xsl:when>
1208   </xsl:choose>
1209  </xsl:variable>
1210  <xsl:variable name="charlength">
1211   <xsl:apply-templates select="*[1]" mode="charcount"/>
1212  </xsl:variable>
1213  <xsl:choose>
1214   <xsl:when test="$charlength >= $framewidth">
1215    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1216     <xsl:if test="@helm:xref">
1217      <xsl:attribute name="helm:xref">
1218       <xsl:value-of select="@helm:xref"/>
1219      </xsl:attribute>
1220     </xsl:if>    
1221     <m:mtr>
1222      <m:mtd>
1223       <m:mo stretchy="false">(</m:mo>
1224       <xsl:apply-templates select="*[position()=2]"/>
1225      </m:mtd>
1226     </m:mtr>
1227     <xsl:for-each select = "*[position()>2]">
1228      <m:mtr>
1229       <m:mtd>
1230        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1231        <m:mo helm:xref="{*[1]/@helm:xref}"> 
1232         <m:mchar name="{$symbol}"/>
1233        </m:mo>
1234        <xsl:apply-templates select="."/>
1235       </m:mtd>
1236      </m:mtr>
1237     </xsl:for-each>
1238     <m:mtr>
1239      <m:mtd>
1240       <m:mo stretchy="false">)</m:mo>
1241      </m:mtd>
1242     </m:mtr>
1243    </m:mtable>
1244   </xsl:when>
1245   <xsl:otherwise>
1246    <xsl:apply-imports/>
1247   </xsl:otherwise>
1248  </xsl:choose>
1249 </xsl:template>
1250
1251 <xsl:template match = "m:set">
1252  <xsl:choose>
1253   <xsl:when test="count(child::*) = 0">
1254    <m:mi> 
1255     <m:mchar name="emptyset"/>
1256    </m:mi>
1257   </xsl:when>
1258   <xsl:otherwise>
1259    <xsl:variable name="charlength">
1260     <xsl:apply-templates select="*[1]" mode="charcount"/>
1261    </xsl:variable>
1262    <xsl:choose>
1263     <xsl:when test="$charlength >= $framewidth">
1264      <xsl:choose>
1265       <xsl:when test="name(*[1]) = 'm:bvar'">
1266        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1267         <m:mtr>
1268          <m:mtd>
1269           <m:mo stretchy="false">{</m:mo>
1270           <xsl:apply-templates select="*[position()=1]"/>
1271          </m:mtd>
1272         </m:mtr>
1273         <m:mtr>
1274          <m:mtd>
1275           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1276           <m:mo stretchy="false">|</m:mo>
1277           <xsl:apply-templates select="m:condition/*[1]"/>
1278          </m:mtd>
1279         </m:mtr>
1280         <m:mtr>
1281          <m:mtd>
1282           <m:mo stretchy="false">}</m:mo>
1283          </m:mtd>
1284         </m:mtr>
1285        </m:mtable>
1286       </xsl:when>
1287       <xsl:otherwise>
1288        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1289         <m:mtr>
1290          <m:mtd>
1291           <m:mo stretchy="false">{</m:mo>
1292           <xsl:apply-templates select="*[position()=1]"/>
1293           <xsl:if test="position() != last()">
1294            <mo>,</mo>
1295           </xsl:if>
1296          </m:mtd>
1297         </m:mtr>
1298         <xsl:for-each select = "*[position()>2]">
1299          <m:mtr>
1300           <m:mtd>
1301            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1302            <xsl:apply-templates select="."/>
1303            <xsl:if test="position() != last()">
1304             <mo>,</mo>
1305            </xsl:if>
1306           </m:mtd>
1307          </m:mtr>
1308         </xsl:for-each>
1309         <m:mtr>
1310          <m:mtd>
1311           <m:mo stretchy="false">}</m:mo>
1312          </m:mtd>
1313         </m:mtr>
1314        </m:mtable>
1315       </xsl:otherwise>
1316      </xsl:choose>
1317     </xsl:when>
1318     <xsl:otherwise>
1319      <xsl:apply-imports/>
1320     </xsl:otherwise>
1321    </xsl:choose>
1322   </xsl:otherwise>
1323  </xsl:choose>
1324 </xsl:template>      
1325
1326 <xsl:template match = "m:apply[m:card[1]]">
1327  <m:mo stretchy="false">|</m:mo>
1328   <xsl:apply-templates select="*[2]"/>
1329  <m:mo stretchy="false">|</m:mo>
1330 </xsl:template>
1331
1332 <!-- *********************************** -->
1333 <!--          PROOF ELEMENTS             -->
1334 <!-- *********************************** -->
1335
1336
1337
1338 <!--**********************-->
1339 <!--       COUNTING       -->
1340 <!--**********************-->
1341
1342 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1343  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1344  |m:plus|m:minus|m:times" mode="charcount">
1345 <xsl:param name="incurrent_length" select="0"/> 
1346     <xsl:choose>
1347     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1348      <xsl:variable name="siblength">
1349       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1350        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1351       </xsl:apply-templates>
1352      </xsl:variable>
1353      <xsl:choose>
1354      <xsl:when test="string($siblength) = &quot;&quot;">
1355       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1356      </xsl:when>
1357      <xsl:otherwise>
1358       <xsl:value-of select="number($siblength)"/>
1359      </xsl:otherwise>
1360      </xsl:choose>
1361     </xsl:when>
1362     <xsl:otherwise>
1363      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1364     </xsl:otherwise>
1365     </xsl:choose>
1366 </xsl:template>
1367
1368 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1369 <xsl:param name="incurrent_length" select="0"/> 
1370 <xsl:param name="nosibling" select="0"/>
1371     <xsl:choose>
1372     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1373      <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>
1374      <xsl:choose>
1375      <xsl:when test="string($siblength) = &quot;&quot;">
1376       <xsl:value-of select="$incurrent_length + string-length()"/>
1377      </xsl:when>
1378      <xsl:otherwise>
1379       <xsl:value-of select="number($siblength)"/>
1380      </xsl:otherwise>
1381      </xsl:choose>
1382     </xsl:when>
1383     <xsl:otherwise>
1384      <xsl:value-of select="$incurrent_length + string-length()"/>
1385     </xsl:otherwise>
1386     </xsl:choose>
1387 </xsl:template> 
1388
1389 <xsl:template match="*" mode="charcount">
1390 <xsl:param name="incurrent_length" select="0"/>
1391 <xsl:param name="nosibling" select="0"/>
1392  <xsl:choose>
1393   <xsl:when test="count(child::*) = 0">
1394    <xsl:value-of select="$incurrent_length"/>
1395   </xsl:when>
1396   <xsl:otherwise>
1397     <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>
1398     <xsl:choose>
1399     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1400      <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>
1401      <xsl:choose>
1402      <xsl:when test="string($siblength) = &quot;&quot;">
1403       <xsl:value-of select="number($childlength)"/>
1404      </xsl:when>
1405      <xsl:otherwise>
1406       <xsl:value-of select="number($siblength)"/>
1407      </xsl:otherwise>
1408      </xsl:choose>>
1409     </xsl:when>
1410     <xsl:otherwise>
1411      <xsl:value-of select="number($childlength)"/>
1412     </xsl:otherwise>
1413     </xsl:choose>
1414   </xsl:otherwise>
1415  </xsl:choose>
1416 </xsl:template>
1417
1418 </xsl:stylesheet> 
1419