3 <!-- Copyright (C) 2000, HELM Team -->
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. -->
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. -->
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. -->
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. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
28 xmlns:m="http://www.w3.org/1998/Math/MathML">
30 <!--***********************************************************************-->
31 <!-- From MathML content to HTML -->
32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi -->
33 <!--***********************************************************************-->
35 <xsl:param name="CICURI" select="''"/>
36 <xsl:param name="type" select="'standalone'"/>
37 <xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
39 <xsl:include href="html_init.xsl"/>
40 <xsl:include href="html_set.xsl"/>
41 <xsl:include href="html_reals.xsl"/>
43 <xsl:variable name="showcast" select="0"/>
45 <!--***********************************************************************-->
46 <!-- HTML Head and Body -->
47 <!--***********************************************************************-->
49 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
51 <!-- document needs method="xml" and searches locally for the dtd if -->
52 <!-- doctype-system is specified (the dtd must exist locally for parsing). -->
53 <!-- For having output html must be media-type="html" and for having the -->
54 <!-- correct <br /> you must specify at least the remote dtd by means of -->
55 <!-- doctype-public -->
59 media-type="text/html"
60 doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
62 <xsl:variable name="framewidth" select="55"/>
64 <xsl:template name="mksymbol-1">
65 <xsl:param name="symbol" select="''"/>
66 <xsl:param name="color" select="''"/>
67 <xsl:param name="size" select="''"/>
69 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
70 <xsl:variable name="fontsymbol">
72 <xsl:when test="$symbol = 'append'">
73 <xsl:value-of select="'@'"/>
75 <xsl:when test="$symbol = 'iff'">
76 <xsl:value-of select="'«'"/>
78 <xsl:when test="$symbol = 'forall'">
79 <xsl:value-of select="'"'"/>
81 <xsl:when test="$symbol = 'lambda'">
82 <xsl:value-of select="'l'"/>
84 <xsl:when test="$symbol = 'prod'">
85 <xsl:value-of select="'Õ'"/>
87 <xsl:when test="$symbol = 'arrow'">
88 <xsl:value-of select="'®'"/>
90 <xsl:when test="$symbol = 'RightArrow'">
91 <xsl:value-of select="'Þ'"/>
93 <xsl:when test="$symbol = 'subst'">
94 <xsl:value-of select="'¬'"/>
96 <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
97 <xsl:value-of select="'­'"/>
99 <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
100 <xsl:value-of select="'®'"/>
102 <xsl:when test="$symbol = 'beta'">
103 <xsl:value-of select="'b'"/>
105 <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
106 <xsl:value-of select="'Þ'"/>
108 <xsl:when test="$symbol = 'isomorphic'">
109 <xsl:value-of select="'@'"/>
112 <xsl:text>???</xsl:text>
116 <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
117 <xsl:value-of select="$fontsymbol"/>
121 <xsl:variable name="unicodesymbol">
123 <xsl:when test="$symbol = 'append'">
124 <xsl:value-of select="'@'"/>
126 <xsl:when test="$symbol = 'iff'">
127 <xsl:value-of select="'↔'"/>
129 <xsl:when test="$symbol = 'forall'">
130 <xsl:value-of select="'∀'"/>
132 <xsl:when test="$symbol = 'lambda'">
133 <xsl:value-of select="'λ'"/>
135 <xsl:when test="$symbol = 'prod'">
136 <xsl:value-of select="'Π'"/>
138 <xsl:when test="$symbol = 'arrow'">
139 <xsl:value-of select="'→'"/>
141 <xsl:when test="$symbol = 'RightArrow'">
142 <xsl:value-of select="'⇒'"/>
144 <xsl:when test="$symbol = 'subst'">
145 <xsl:value-of select="'←'"/>
147 <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
148 <xsl:value-of select="'↑'"/>
150 <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
151 <xsl:value-of select="'→'"/>
153 <xsl:when test="$symbol = 'beta'">
154 <xsl:value-of select="'β'"/>
156 <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
157 <xsl:value-of select="'⇒'"/>
159 <xsl:when test="$symbol = 'isomorphic'">
160 <xsl:value-of select="'≅'"/>
163 <xsl:text>???</xsl:text>
167 <FONT color="{$color}">
168 <xsl:value-of select="$unicodesymbol"/>
174 <xsl:template match="/">
175 <xsl:param name="current_indent" select="0"/>
177 <xsl:when test="$type = 'standalone'">
180 <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
181 <style> A { text-decoration: none } </style>
183 <xsl:text disable-output-escaping="yes">
185 function Hide(which){
186 if (!document.getElementById)
188 which.style.display="none"
191 function Show(which){
192 if (!document.getElementById)
194 which.style.display=""
197 document.to_be_deleted = new Array();
202 <body bgcolor="white">
203 <xsl:attribute name="onLoad">
204 if(document.getElementById)
205 for(var i=0;i<document.to_be_deleted.length;i++)
206 Hide(document.getElementById(document.to_be_deleted[i]));
208 <xsl:apply-templates>
209 <xsl:with-param name="current_indent" select="0"/>
210 </xsl:apply-templates>
216 <xsl:apply-templates>
217 <xsl:with-param name="current_indent" select="0"/>
218 </xsl:apply-templates>
224 <!--***********************************************************************-->
226 <!--***********************************************************************-->
228 <xsl:template name="make_indent">
229 <xsl:param name="current_indent" select="0"/>
230 <!-- non funziona bene con netscape !!!
232 <xsl:attribute name="style">
233 <xsl:value-of select="concat('margin-left:',string($current_indent div 3), 'em')"/>
236 <xsl:if test="$current_indent > 0">
237 <xsl:text> </xsl:text>
238 <xsl:call-template name="make_indent">
239 <xsl:with-param name="current_indent" select="$current_indent - 1"/>
244 <!-- Syntactic Sugar -->
245 <xsl:template match="m:type">
246 <xsl:param name="current_indent" select="0"/>
247 <xsl:apply-templates>
248 <xsl:with-param name="current_indent"
249 select="$current_indent"/>
250 </xsl:apply-templates>
253 <xsl:template match="m:condition">
254 <xsl:param name="current_indent" select="0"/>
255 <xsl:apply-templates>
256 <xsl:with-param name="current_indent"
257 select="$current_indent"/>
258 </xsl:apply-templates>
261 <xsl:template match="m:math">
262 <xsl:param name="current_indent" select="0"/>
263 <xsl:apply-templates>
264 <xsl:with-param name="current_indent"
265 select="$current_indent"/>
266 </xsl:apply-templates>
269 <!--*********************************************************************-->
271 <!--*********************************************************************-->
274 <xsl:template mode="inline" match="m:ci">
276 <xsl:when test="boolean(@definitionURL)">
277 <a href="{@definitionURL}">
278 <xsl:apply-templates/>
282 <xsl:value-of select="."/>
289 <xsl:template match="m:apply[m:csymbol]" mode="inline">
290 <xsl:variable name="name">
291 <xsl:value-of select="m:csymbol"/>
293 <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
296 <xsl:when test="$name='forall'">
297 <xsl:call-template name="mksymbol-1">
298 <xsl:with-param name="symbol" select="$name"/>
299 <xsl:with-param name="color" select="'blue'"/>
300 <xsl:with-param name="size" select="'+2'"/>
302 <xsl:apply-templates select="m:bvar/m:ci"/>
303 <xsl:text>:</xsl:text>
304 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
305 <xsl:text>.</xsl:text>
306 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
308 <xsl:when test="$name='prod'">
309 <xsl:call-template name="mksymbol-1">
310 <xsl:with-param name="symbol" select="$name"/>
311 <xsl:with-param name="color" select="'blue'"/>
312 <xsl:with-param name="size" select="'+2'"/>
314 <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
315 <xsl:text>:</xsl:text>
316 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
317 <xsl:text>.</xsl:text>
318 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
321 <xsl:when test="$name='arrow'">
322 <xsl:text>(</xsl:text>
323 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
324 <xsl:call-template name="mksymbol-1">
325 <xsl:with-param name="symbol" select="$name"/>
326 <xsl:with-param name="color" select="'blue'"/>
327 <xsl:with-param name="size" select="'+0'"/>
329 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
330 <xsl:text>)</xsl:text>
333 <xsl:when test="$name='iff'">
334 <xsl:text>(</xsl:text>
335 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
336 <xsl:call-template name="mksymbol-1">
337 <xsl:with-param name="symbol" select="$name"/>
338 <xsl:with-param name="color" select="'blue'"/>
339 <xsl:with-param name="size" select="'+0'"/>
341 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
342 <xsl:text>)</xsl:text>
345 <xsl:when test="$name='append'">
346 <xsl:text>(</xsl:text>
347 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
348 <xsl:call-template name="mksymbol-1">
349 <xsl:with-param name="symbol" select="$name"/>
350 <xsl:with-param name="color" select="'blue'"/>
351 <xsl:with-param name="size" select="'+0'"/>
353 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
354 <xsl:text>)</xsl:text>
357 <xsl:when test="$name='app'">
358 <xsl:text>(</xsl:text>
359 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
360 <xsl:for-each select="*[position()>2]">
361 <xsl:text> </xsl:text>
362 <xsl:apply-templates mode="inline" select="."/>
364 <xsl:text>)</xsl:text>
367 <xsl:when test="$name='cast'">
368 <xsl:text>(</xsl:text>
369 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
370 <xsl:text>:</xsl:text>
371 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
372 <xsl:text>)</xsl:text>
374 <xsl:when test="$name='Prop'">
375 <FONT color="violet">Prop</FONT>
377 <xsl:when test="$name='Set'">
378 <FONT color="violet">Set</FONT>
380 <xsl:when test="$name='Type'">
381 <FONT color="violet">Type</FONT>
384 <xsl:when test="$name='mutcase'">
385 <xsl:text><</xsl:text>
386 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
387 <xsl:text>> </xsl:text>
388 <FONT color="red">CASE </FONT>
389 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
390 <FONT color="red"> OF </FONT>
391 <xsl:for-each select="m:piecewise/m:piece">
392 <!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
394 <xsl:when test="not(position() = 1)">
395 <xsl:text> | </xsl:text>
398 <xsl:apply-templates mode="inline" select="./*[2]"/>
399 <xsl:call-template name="mksymbol-1">
400 <xsl:with-param name="symbol" select="'RightArrow'"/>
401 <xsl:with-param name="color" select="'green'"/>
402 <xsl:with-param name="size" select="'+0'"/>
404 <xsl:apply-templates mode="inline"
409 <xsl:when test="$name='inst'">
410 <xsl:apply-templates select="*[2]" mode="inline"/>
411 <FONT color="blue">{</FONT>
412 <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
413 <xsl:apply-templates select="following-sibling::*[position() = 1]" mode="inline"/>
414 <FONT color="blue">/</FONT>
415 <xsl:if test="name()='m:ci'">
416 <a href="{@definitionURL}">
417 <xsl:apply-templates/>
420 <!-- <xsl:apply-templates select="." mode="inline"/> -->
422 <FONT color="blue">}</FONT>
426 <xsl:when test="$name='fix'">
427 <FONT color="red">FIX</FONT>
428 <xsl:value-of select="m:ci"/>
429 <xsl:text>{</xsl:text>
430 <xsl:for-each select="m:bvar">
431 <xsl:value-of select="m:ci"/>
432 <xsl:text>:</xsl:text>
433 <xsl:apply-templates mode="inline" select="m:type"/>
434 <xsl:text>:=</xsl:text>
435 <xsl:apply-templates mode="inline"
436 select="following-sibling::*[position() = 1]"/>
438 <xsl:when test="position()=last()">
439 <xsl:text>}</xsl:text>
442 <xsl:text>;</xsl:text>
448 <xsl:when test="$name='cofix'">
449 <xsl:text>COFIX</xsl:text>
450 <xsl:value-of select="m:ci"/>
451 <xsl:text>{</xsl:text>
452 <xsl:for-each select="m:bvar">
453 <xsl:value-of select="m:ci"/>
454 <xsl:text>:</xsl:text>
455 <xsl:apply-templates mode="inline" select="m:type"/>
456 <xsl:text>:=</xsl:text>
457 <xsl:apply-templates mode="inline"
458 select="following-sibling::*[position() = 1]"/>
460 <xsl:when test="position()=last()">
461 <xsl:text>}</xsl:text>
464 <xsl:text>;</xsl:text>
469 <!-- if then else -->
470 <xsl:when test="$name='ite'">
471 <xsl:text>if </xsl:text>
472 <xsl:apply-templates select="*[2]"/>
473 <xsl:text> then </xsl:text>
474 <xsl:apply-templates select="*[3]"/>
475 <xsl:text> else </xsl:text>
476 <xsl:apply-templates select="*[4]"/>
478 <!-- proof and side_proof -->
479 <xsl:when test="$name='proof' or $name='side_proof'">
480 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
481 <FONT color="red"> proves </FONT>
482 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
484 <FONT color="red"> which is equivalent to </FONT>
485 <xsl:apply-templates mode="inline" select="*[position()=4]"/>
489 <xsl:when test="$name='letin1'">
490 <xsl:text>letin1 (inline error)</xsl:text>
493 <xsl:when test="$name='false_ind'">
494 <xsl:apply-templates mode="inline" select="*[3]"/>
495 <FONT color="red">Contradiction.</FONT>
498 <xsl:when test="$name='and_ind'">
499 <FONT color="red">From </FONT>
500 <xsl:apply-templates select="*[2]"/>
501 <FONT color="red"> we get</FONT>
503 <xsl:apply-templates select="*[3]"/>
505 <xsl:apply-templates mode="inline" select="*[4]"/>
506 <FONT color="red"> and </FONT>
508 <xsl:apply-templates select="*[5]"/>
510 <xsl:apply-templates mode="inline" select="*[6]"/>
512 <FONT color="red"> hence </FONT>
513 <xsl:apply-templates mode="inline" select="*[7]"/>
516 <xsl:when test="$name='subst'">
517 <xsl:apply-templates select="*[3]" mode="inline"/>
518 <xsl:text>[</xsl:text>
519 <xsl:apply-templates select="*[4]" mode="inline"/>
521 <xsl:when test="$uri != ''">
523 <xsl:call-template name="mksymbol-1">
524 <xsl:with-param name="symbol" select="$name"/>
525 <xsl:with-param name="color" select="'green'"/>
526 <xsl:with-param name="size" select="'+0'"/>
531 <xsl:call-template name="mksymbol-1">
532 <xsl:with-param name="symbol" select="$name"/>
533 <xsl:with-param name="color" select="'green'"/>
534 <xsl:with-param name="size" select="'+0'"/>
538 <xsl:apply-templates select="*[2]" mode="inline"/>
539 <xsl:text>]</xsl:text>
542 <xsl:when test="$name='lift_with_base'">
544 <xsl:apply-templates select="*[3]" mode="inline"/>
547 <xsl:when test="$uri != ''">
549 <xsl:call-template name="mksymbol-1">
550 <xsl:with-param name="symbol" select="$name"/>
551 <xsl:with-param name="color" select="'green'"/>
552 <xsl:with-param name="size" select="'+0'"/>
557 <xsl:call-template name="mksymbol-1">
558 <xsl:with-param name="symbol" select="$name"/>
559 <xsl:with-param name="color" select="'green'"/>
560 <xsl:with-param name="size" select="'+0'"/>
565 <xsl:apply-templates select="*[4]" mode="inline"/>
567 <xsl:text>(</xsl:text>
568 <xsl:apply-templates select="*[2]" mode="inline"/>
569 <xsl:text>)</xsl:text>
572 <xsl:when test="$name='lift'">
574 <xsl:when test="$uri != ''">
576 <xsl:call-template name="mksymbol-1">
577 <xsl:with-param name="symbol" select="$name"/>
578 <xsl:with-param name="color" select="'green'"/>
579 <xsl:with-param name="size" select="'+0'"/>
584 <xsl:call-template name="mksymbol-1">
585 <xsl:with-param name="symbol" select="$name"/>
586 <xsl:with-param name="color" select="'green'"/>
587 <xsl:with-param name="size" select="'+0'"/>
592 <xsl:apply-templates select="*[2]" mode="inline"/>
594 <xsl:text>(</xsl:text>
595 <xsl:apply-templates select="*[3]" mode="inline"/>
596 <xsl:text>)</xsl:text>
600 <xsl:when test="$name='beta_red1'">
601 <xsl:apply-templates select="*[2]" mode="inline"/>
603 <xsl:when test="$uri != ''">
605 <xsl:call-template name="mksymbol-1">
606 <xsl:with-param name="symbol" select="$name"/>
607 <xsl:with-param name="color" select="'green'"/>
608 <xsl:with-param name="size" select="'+0'"/>
611 <xsl:call-template name="mksymbol-1">
612 <xsl:with-param name="symbol" select="'beta'"/>
613 <xsl:with-param name="color" select="'green'"/>
614 <xsl:with-param name="size" select="'+0'"/>
620 <xsl:call-template name="mksymbol-1">
621 <xsl:with-param name="symbol" select="$name"/>
622 <xsl:with-param name="color" select="'green'"/>
623 <xsl:with-param name="size" select="'+0'"/>
626 <xsl:call-template name="mksymbol-1">
627 <xsl:with-param name="symbol" select="'beta'"/>
628 <xsl:with-param name="color" select="'green'"/>
629 <xsl:with-param name="size" select="'+0'"/>
634 <xsl:apply-templates select="*[3]" mode="inline"/>
637 <xsl:when test="$name='beta_red'">
638 <xsl:apply-templates select="*[2]" mode="inline"/>
640 <xsl:when test="$uri != ''">
642 <xsl:call-template name="mksymbol-1">
643 <xsl:with-param name="symbol" select="$name"/>
644 <xsl:with-param name="color" select="'green'"/>
645 <xsl:with-param name="size" select="'+0'"/>
648 <xsl:call-template name="mksymbol-1">
649 <xsl:with-param name="symbol" select="'beta'"/>
650 <xsl:with-param name="color" select="'green'"/>
651 <xsl:with-param name="size" select="'+0'"/>
653 <xsl:text>*</xsl:text>
658 <xsl:call-template name="mksymbol-1">
659 <xsl:with-param name="symbol" select="$name"/>
660 <xsl:with-param name="color" select="'green'"/>
661 <xsl:with-param name="size" select="'+0'"/>
664 <xsl:call-template name="mksymbol-1">
665 <xsl:with-param name="symbol" select="'beta'"/>
666 <xsl:with-param name="color" select="'green'"/>
667 <xsl:with-param name="size" select="'+0'"/>
669 <xsl:text>*</xsl:text>
673 <xsl:apply-templates select="*[3]" mode="inline"/>
676 <xsl:when test="$name='par_beta_red1'">
677 <xsl:apply-templates select="*[2]" mode="inline"/>
679 <xsl:when test="$uri != ''">
681 <xsl:call-template name="mksymbol-1">
682 <xsl:with-param name="symbol" select="$name"/>
683 <xsl:with-param name="color" select="'green'"/>
684 <xsl:with-param name="size" select="'+0'"/>
687 <xsl:call-template name="mksymbol-1">
688 <xsl:with-param name="symbol" select="'beta'"/>
689 <xsl:with-param name="color" select="'green'"/>
690 <xsl:with-param name="size" select="'+0'"/>
696 <xsl:call-template name="mksymbol-1">
697 <xsl:with-param name="symbol" select="$name"/>
698 <xsl:with-param name="color" select="'green'"/>
699 <xsl:with-param name="size" select="'+0'"/>
702 <xsl:call-template name="mksymbol-1">
703 <xsl:with-param name="symbol" select="'beta'"/>
704 <xsl:with-param name="color" select="'green'"/>
705 <xsl:with-param name="size" select="'+0'"/>
710 <xsl:apply-templates select="*[3]" mode="inline"/>
713 <xsl:when test="$name='par_beta_red'">
714 <xsl:apply-templates select="*[2]" mode="inline"/>
716 <xsl:when test="$uri != ''">
718 <xsl:call-template name="mksymbol-1">
719 <xsl:with-param name="symbol" select="$name"/>
720 <xsl:with-param name="color" select="'green'"/>
721 <xsl:with-param name="size" select="'+0'"/>
724 <xsl:call-template name="mksymbol-1">
725 <xsl:with-param name="symbol" select="'beta'"/>
726 <xsl:with-param name="color" select="'green'"/>
727 <xsl:with-param name="size" select="'+0'"/>
729 <xsl:text>*</xsl:text>
734 <xsl:call-template name="mksymbol-1">
735 <xsl:with-param name="symbol" select="$name"/>
736 <xsl:with-param name="color" select="'green'"/>
737 <xsl:with-param name="size" select="'+0'"/>
740 <xsl:call-template name="mksymbol-1">
741 <xsl:with-param name="symbol" select="'beta'"/>
742 <xsl:with-param name="color" select="'green'"/>
743 <xsl:with-param name="size" select="'+0'"/>
745 <xsl:text>*</xsl:text>
749 <xsl:apply-templates select="*[3]" mode="inline"/>
753 <xsl:when test="$name='forgetful'">
755 <xsl:when test="$uri != ''">
756 <a href="{$uri}">|</a>
762 <xsl:apply-templates select="*[2]" mode="inline"/>
764 <xsl:when test="$uri != ''">
765 <a href="{$uri}">|</a>
773 <!-- boolean algebra of redexes -->
776 <xsl:when test="$name='isomorphic'">
777 <xsl:apply-templates select="*[2]" mode="inline"/>
779 <xsl:when test="$uri != ''">
781 <xsl:call-template name="mksymbol-1">
782 <xsl:with-param name="symbol" select="$name"/>
783 <xsl:with-param name="color" select="'green'"/>
784 <xsl:with-param name="size" select="'+0'"/>
789 <xsl:call-template name="mksymbol-1">
790 <xsl:with-param name="symbol" select="$name"/>
791 <xsl:with-param name="color" select="'green'"/>
792 <xsl:with-param name="size" select="'+0'"/>
796 <xsl:apply-templates select="*[3]" mode="inline"/>
800 <xsl:when test="$name='interp'">
801 <font color="green">[</font>
802 <xsl:apply-templates select="*[2]"/>
803 <font color="green">]</font>
809 <xsl:template mode="inline" match="m:lambda">
810 <xsl:call-template name="mksymbol-1">
811 <xsl:with-param name="symbol" select="'lambda'"/>
812 <xsl:with-param name="color" select="'red'"/>
813 <xsl:with-param name="size" select="'+2'"/>
815 <xsl:apply-templates select="m:bvar/m:ci"/>
816 <xsl:text>:</xsl:text>
817 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
818 <xsl:text>.</xsl:text>
819 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
822 <!--*********************************************************************-->
823 <!-- COUNTING MODE -->
824 <!--*********************************************************************-->
826 <xsl:template match="m:apply[m:csymbol]">
827 <xsl:param name="current_indent" select="0"/>
828 <xsl:param name="width" select="$framewidth"/>
829 <xsl:variable name="name">
830 <xsl:value-of select="m:csymbol"/>
832 <xsl:variable name="charlength">
833 <xsl:apply-templates select="m:csymbol" mode="charcount"/>
835 <!-- <xsl:value-of select="$current_indent"/> -->
836 <!-- <xsl:value-of select="$charlength"/> -->
837 <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
840 <xsl:when test="$name='inst'">
841 <xsl:apply-templates select="." mode="inline"/>
844 <xsl:when test="$name='forall'">
846 <xsl:when test="$charlength > $framewidth">
848 <xsl:call-template name="mksymbol-1">
849 <xsl:with-param name="symbol" select="$name"/>
850 <xsl:with-param name="color" select="'blue'"/>
851 <xsl:with-param name="size" select="'+2'"/>
853 <xsl:apply-templates select="m:bvar/m:ci"/>
854 <xsl:text>:</xsl:text>
855 <xsl:apply-templates select="m:bvar/m:type">
856 <xsl:with-param name="current_indent"
857 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
858 </xsl:apply-templates>
860 <xsl:call-template name="make_indent">
861 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
863 <xsl:text>.</xsl:text>
864 <xsl:apply-templates select="*[position()=3]">
865 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
866 </xsl:apply-templates>
869 <xsl:apply-templates mode="inline" select="."/>
874 <xsl:when test="$name='prod'">
876 <xsl:when test="$charlength > $framewidth">
877 <xsl:call-template name="mksymbol-1">
878 <xsl:with-param name="symbol" select="$name"/>
879 <xsl:with-param name="color" select="'blue'"/>
880 <xsl:with-param name="size" select="'+2'"/>
882 <xsl:apply-templates select="m:bvar/m:ci"/>
883 <xsl:text>:</xsl:text>
884 <xsl:apply-templates select="m:bvar/m:type">
885 <xsl:with-param name="current_indent"
886 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
887 </xsl:apply-templates><br/>
888 <xsl:call-template name="make_indent">
889 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
891 <xsl:text>.</xsl:text>
892 <xsl:apply-templates select="*[position()=3]">
893 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
894 </xsl:apply-templates>
897 <xsl:apply-templates mode="inline" select="."/>
902 <xsl:when test="$name='arrow'">
904 <xsl:when test="$charlength > $framewidth">
905 <xsl:text>(</xsl:text>
906 <xsl:apply-templates select="*[position()=2]">
907 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
908 </xsl:apply-templates>
910 <xsl:call-template name="make_indent">
911 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
914 <xsl:call-template name="mksymbol-1">
915 <xsl:with-param name="symbol" select="$name"/>
916 <xsl:with-param name="color" select="'blue'"/>
917 <xsl:with-param name="size" select="'+0'"/>
919 <xsl:apply-templates select="*[position()=3]">
920 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
921 </xsl:apply-templates>
922 <xsl:text>)</xsl:text>
925 <xsl:apply-templates mode="inline" select="."/>
930 <xsl:when test="$name='iff'">
932 <xsl:when test="$charlength > $framewidth">
933 <xsl:text>(</xsl:text>
934 <xsl:apply-templates select="*[position()=2]">
935 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
936 </xsl:apply-templates>
938 <xsl:call-template name="make_indent">
939 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
942 <xsl:call-template name="mksymbol-1">
943 <xsl:with-param name="symbol" select="$name"/>
944 <xsl:with-param name="color" select="'blue'"/>
945 <xsl:with-param name="size" select="'+0'"/>
947 <xsl:apply-templates select="*[position()=3]">
948 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
949 </xsl:apply-templates>
950 <xsl:text>)</xsl:text>
953 <xsl:apply-templates mode="inline" select="."/>
958 <xsl:when test="$name='append'">
960 <xsl:when test="$charlength > $framewidth">
961 <xsl:text>(</xsl:text>
962 <xsl:apply-templates select="*[position()=2]">
963 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
964 </xsl:apply-templates>
966 <xsl:call-template name="make_indent">
967 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
970 <xsl:call-template name="mksymbol-1">
971 <xsl:with-param name="symbol" select="$name"/>
972 <xsl:with-param name="color" select="'blue'"/>
973 <xsl:with-param name="size" select="'+0'"/>
975 <xsl:apply-templates select="*[position()=3]">
976 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
977 </xsl:apply-templates>
978 <xsl:text>)</xsl:text>
981 <xsl:apply-templates mode="inline" select="."/>
986 <xsl:when test="$name='app'">
988 <xsl:when test="$charlength > $framewidth">
989 <xsl:text>(</xsl:text>
990 <xsl:apply-templates select="*[position()=2]">
991 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
992 </xsl:apply-templates>
993 <xsl:for-each select="*[position()>2]">
995 <xsl:call-template name="make_indent">
996 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
998 <xsl:apply-templates select=".">
999 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1000 </xsl:apply-templates>
1002 <xsl:text>)</xsl:text>
1005 <xsl:apply-templates mode="inline" select="."/>
1009 <xsl:when test="$name='cast'">
1011 <xsl:when test="$showcast = 1">
1013 <xsl:when test="$charlength > $framewidth">
1014 <xsl:text>(</xsl:text>
1015 <xsl:apply-templates select="*[position()=2]">
1016 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1017 </xsl:apply-templates><br/>
1018 <xsl:call-template name="make_indent">
1019 <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
1020 <xsl:text>:></xsl:text>
1021 <xsl:apply-templates select="*[position()=3]">
1022 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1023 </xsl:apply-templates>
1024 <xsl:text>)</xsl:text>
1027 <xsl:apply-templates mode="inline" select="."/>
1032 <xsl:apply-templates select="*[position()=2]">
1033 <xsl:with-param name="current_indent" select="$current_indent"/>
1034 </xsl:apply-templates>
1038 <xsl:when test="$name='Prop'">
1039 <xsl:text>Prop</xsl:text>
1041 <xsl:when test="$name='Set'">
1042 <xsl:text>Set</xsl:text>
1044 <xsl:when test="$name='Type'">
1045 <xsl:text>Type</xsl:text>
1047 <xsl:when test="$name='mutcase'">
1049 <xsl:when test="$charlength > $framewidth">
1050 <xsl:text><</xsl:text>
1051 <xsl:apply-templates select="*[position()=2]">
1052 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1053 </xsl:apply-templates>
1054 <xsl:text>> </xsl:text>
1056 <xsl:call-template name="make_indent">
1057 <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
1058 <xsl:text>CASE </xsl:text>
1059 <xsl:apply-templates select="*[position()=3]">
1060 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1061 </xsl:apply-templates>
1062 <xsl:text> OF </xsl:text>
1063 <xsl:for-each select="m:piecewise/m:piece">
1064 <!-- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
1066 <xsl:call-template name="make_indent">
1067 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1068 </xsl:call-template>
1070 <xsl:when test="position() = 1">
1071 <xsl:text>  </xsl:text>
1074 <xsl:text>| </xsl:text>
1077 <xsl:apply-templates select="./*[2]"/>
1078 <xsl:call-template name="mksymbol-1">
1079 <xsl:with-param name="symbol" select="'RightArrow'"/>
1080 <xsl:with-param name="color" select="'green'"/>
1081 <xsl:with-param name="size" select="'+0'"/>
1082 </xsl:call-template>
1083 <xsl:variable name="body_size">
1084 <xsl:apply-templates
1085 select="./*[1]/*[1]" mode="charcount"/>
1088 <xsl:when test="$body_size > $framewidth">
1090 <xsl:call-template name="make_indent">
1091 <xsl:with-param name="current_indent"
1092 select="$current_indent + 8"/>
1093 </xsl:call-template>
1094 <xsl:apply-templates
1096 <xsl:with-param name="current_indent"
1097 select="$current_indent + 8"/>
1098 </xsl:apply-templates>
1101 <xsl:apply-templates select="./*[1]"
1108 <xsl:apply-templates mode="inline" select="."/>
1113 <xsl:when test="$name='fix'">
1115 <xsl:when test="$charlength > $framewidth">
1116 <xsl:text>FIX</xsl:text>
1117 <xsl:value-of select="m:ci"/>
1118 <xsl:text>{</xsl:text>
1119 <xsl:for-each select="m:bvar">
1121 <xsl:call-template name="make_indent">
1122 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1123 </xsl:call-template>
1124 <xsl:value-of select="m:ci"/>
1125 <xsl:text>:</xsl:text>
1126 <xsl:apply-templates select="m:type">
1127 <xsl:with-param name="current_indent"
1128 select="$current_indent + 5 + string-length(m:ci)"/>
1129 </xsl:apply-templates>
1131 <xsl:call-template name="make_indent">
1132 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1133 </xsl:call-template>
1134 <xsl:text>:=</xsl:text>
1135 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1136 <xsl:with-param name="current_indent" select="$current_indent +2"/>
1137 </xsl:apply-templates>
1140 <xsl:call-template name="make_indent">
1141 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1142 </xsl:call-template>
1143 <xsl:text>}</xsl:text>
1146 <xsl:apply-templates mode="inline" select="."/>
1151 <xsl:when test="$name='cofix'">
1153 <xsl:when test="($charlength + 10) > $framewidth">
1154 <xsl:text>COFIX</xsl:text>
1155 <xsl:value-of select="m:ci"/>
1156 <xsl:text>{</xsl:text>
1158 <xsl:call-template name="make_indent">
1159 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1160 </xsl:call-template>
1161 <xsl:for-each select="m:bvar">
1162 <xsl:value-of select="m:ci"/>
1163 <xsl:text>:</xsl:text>
1164 <xsl:apply-templates select="m:type">
1165 <xsl:with-param name="current_indent"
1166 select="$current_indent + 5 + string-length(m:ci)"/>
1167 </xsl:apply-templates>
1169 <xsl:call-template name="make_indent">
1170 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1171 </xsl:call-template>
1172 <xsl:text>:=</xsl:text>
1173 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1174 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1175 </xsl:apply-templates>
1179 <xsl:call-template name="make_indent">
1180 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1181 </xsl:call-template>
1182 <xsl:text>}</xsl:text>
1185 <xsl:apply-templates mode="inline" select="m:type"/>
1189 <xsl:when test="$name='let_in'">
1190 <xsl:text>let </xsl:text>
1191 <xsl:apply-templates select="m:bvar/m:ci"/>
1192 <xsl:text> := </xsl:text>
1193 <xsl:apply-templates select="*[3]">
1194 <xsl:with-param name="current_indent" select="$current_indent+14"/>
1195 </xsl:apply-templates>
1197 <xsl:call-template name="make_indent">
1198 <xsl:with-param name="current_indent" select="$current_indent"/>
1199 </xsl:call-template>
1200 <xsl:text>in </xsl:text>
1201 <xsl:apply-templates select="*[4]">
1202 <xsl:with-param name="current_indent" select="$current_indent+5"/>
1203 </xsl:apply-templates>
1205 <!-- it then else -->
1206 <xsl:when test="$name='ite'">
1207 <xsl:text>if </xsl:text>
1208 <xsl:apply-templates select="*[2]">
1209 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1210 </xsl:apply-templates>
1212 <xsl:call-template name="make_indent">
1213 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1214 </xsl:call-template>
1215 <xsl:text> then </xsl:text>
1216 <xsl:apply-templates select="*[3]">
1217 <xsl:with-param name="current_indent" select="$current_indent + 12"/>
1218 </xsl:apply-templates>
1220 <xsl:call-template name="make_indent">
1221 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1222 </xsl:call-template>
1223 <xsl:text> else </xsl:text>
1224 <xsl:apply-templates select="*[4]">
1225 <xsl:with-param name="current_indent" select="$current_indent + 12"/>
1226 </xsl:apply-templates>
1229 <!-- ***************************************** -->
1230 <!-- *********** PROOF ELEMENTS ************** -->
1231 <!-- ***************************************** -->
1233 <xsl:when test="$name='proof'">
1234 <xsl:variable name="nonce" select="generate-id()"/>
1235 <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1236 <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1237 <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1238 <span ID="{$freshid1}">
1239 <xsl:apply-templates select="*[position()=2]">
1240 <xsl:with-param name="current_indent" select="$current_indent"/>
1241 </xsl:apply-templates>
1243 <xsl:if test="*[4]">
1245 <xsl:call-template name="make_indent">
1246 <xsl:with-param name="current_indent" select="$current_indent"/>
1247 </xsl:call-template>
1248 <FONT color="red">we proved </FONT>
1249 <xsl:apply-templates select="*[position()=3]">
1250 <xsl:with-param name="current_indent" select="$current_indent+16"/>
1251 </xsl:apply-templates>
1253 <xsl:call-template name="make_indent">
1254 <xsl:with-param name="current_indent" select="$current_indent"/>
1255 </xsl:call-template>
1256 <FONT color="red">and by delta equivalence</FONT>
1257 <xsl:apply-templates select="*[position()=5]">
1258 <xsl:with-param name="current_indent" select="$current_indent+16"/>
1259 </xsl:apply-templates>
1263 <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
1264 (preceding-sibling::*[1]/text()='rw_step') or
1265 (name(..)='m:lambda')">
1267 <xsl:call-template name="make_indent">
1268 <xsl:with-param name="current_indent" select="$current_indent"/>
1269 </xsl:call-template>
1270 <FONT color="red">we proved </FONT>
1274 if(document.getElementById) {
1276 <span ID="{$freshid2}">\
1277 <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));return (0==1);">Proof of</a>\
1279 <span ID="{$freshid3}">\
1281 <xsl:call-template name="make_indent">
1282 <xsl:with-param name="current_indent" select="$current_indent"/>
1283 </xsl:call-template>\
1284 <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we obtain</a>\
1287 document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1288 document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1289 document.write(' ');
1293 <xsl:call-template name="make_indent">
1294 <xsl:with-param name="current_indent" select="$current_indent"/>
1295 </xsl:call-template>\
1296 <FONT color="red">we proved </FONT>\
1302 <xsl:apply-templates select="*[position()=last()]">
1303 <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1304 </xsl:apply-templates>
1307 <xsl:when test="$name='side_proof'">
1308 <xsl:variable name="nonce" select="generate-id()"/>
1309 <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1310 <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1311 <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1312 <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
1313 <span ID="{$freshid1}">
1314 <xsl:apply-templates select="*[position()=2]">
1315 <xsl:with-param name="current_indent" select="$current_indent"/>
1316 </xsl:apply-templates>
1320 if(document.getElementById) {
1322 <span ID="{$freshid2}">\
1323 <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
1325 <span ID="{$freshid3}">\
1327 <xsl:call-template name="make_indent">
1328 <xsl:with-param name="current_indent" select="$current_indent"/>
1329 </xsl:call-template>\
1330 <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
1333 document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1334 document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1335 document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
1336 document.write(' ');
1340 <xsl:call-template name="make_indent">
1341 <xsl:with-param name="current_indent" select="$current_indent"/>
1342 </xsl:call-template>\
1343 <FONT color="red">we proved </FONT>\
1347 <span ID="{$freshid4}">
1348 <xsl:apply-templates select="*[position()=3]">
1349 <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1350 </xsl:apply-templates>
1354 <xsl:when test="$name='eq_chain'">
1355 <FONT color="red">We have the following equality chain:</FONT>
1356 <xsl:for-each select="*[position() mod 2 = 0]">
1357 <xsl:variable name="pos" select="position()"/>
1359 <xsl:call-template name="make_indent">
1360 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1361 </xsl:call-template>
1363 <xsl:when test="$pos=1">
1364 <xsl:apply-templates select=".">
1365 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1366 </xsl:apply-templates>
1367 <xsl:text> =</xsl:text>
1370 <xsl:text>= </xsl:text>
1371 <xsl:apply-templates select=".">
1372 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1373 </xsl:apply-templates>
1376 <xsl:if test="$pos != last()">
1378 <xsl:call-template name="make_indent">
1379 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1380 </xsl:call-template>
1381 <xsl:apply-templates select="../*[position()=2*$pos +1]">
1382 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1383 </xsl:apply-templates>
1387 <!-- diseq_chain -->
1388 <xsl:when test="$name='diseq_chain'">
1389 <FONT color="red">We have the following chain of disequalities:</FONT>
1390 <xsl:for-each select="*[position() mod 3 = 2]">
1391 <xsl:variable name="pos" select="position()"/>
1393 <xsl:call-template name="make_indent">
1394 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1395 </xsl:call-template>
1397 <xsl:when test="$pos=1">
1398 <xsl:apply-templates select=".">
1399 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1400 </xsl:apply-templates>
1401 <xsl:text> </xsl:text>
1402 <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
1405 <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
1406 <xsl:text> </xsl:text>
1407 <xsl:apply-templates select=".">
1408 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1409 </xsl:apply-templates>
1412 <xsl:if test="$pos != last()">
1414 <xsl:call-template name="make_indent">
1415 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1416 </xsl:call-template>
1417 <xsl:apply-templates select="../*[position()=3*$pos +1]">
1418 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1419 </xsl:apply-templates>
1424 <xsl:when test="$name='letin1'">
1425 <xsl:apply-templates select="*[position()=2]">
1426 <xsl:with-param name="current_indent" select="$current_indent"/>
1427 </xsl:apply-templates>
1429 <xsl:call-template name="make_indent">
1430 <xsl:with-param name="current_indent" select="$current_indent"/>
1431 </xsl:call-template>
1432 <xsl:apply-templates select="*[position()=3]">
1433 <xsl:with-param name="current_indent" select="$current_indent"/>
1434 </xsl:apply-templates>
1437 <xsl:when test="$name='letin'">
1438 <xsl:for-each select="*[position()>1 and last()>position()]">
1439 <xsl:apply-templates select=".">
1440 <xsl:with-param name="current_indent" select="$current_indent"/>
1441 </xsl:apply-templates>
1443 <xsl:call-template name="make_indent">
1444 <xsl:with-param name="current_indent" select="$current_indent"/>
1445 </xsl:call-template>
1447 <xsl:apply-templates select="*[position()=last()]">
1448 <xsl:with-param name="current_indent" select="$current_indent"/>
1449 </xsl:apply-templates>
1452 <xsl:when test="$name='let'">
1454 <xsl:apply-templates select="m:ci"/>
1456 <xsl:apply-templates select="*[3]">
1457 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1458 </xsl:apply-templates>
1461 <xsl:when test="$name='rw_step'">
1463 <xsl:when test="name(*[2])='m:apply'">
1464 <xsl:apply-templates select="*[2]">
1465 <xsl:with-param name="current_indent" select="$current_indent"/>
1466 </xsl:apply-templates>
1469 <FONT color="red">Consider </FONT>
1470 <xsl:apply-templates select="*[2]"/>
1473 <xsl:variable name="charlength_first">
1474 <xsl:apply-templates select="*[3]" mode="root_charcount"/>
1476 <xsl:variable name="charlength_second">
1477 <xsl:apply-templates select="*[4]" mode="root_charcount"/>
1479 <xsl:variable name="charlength_side_proof">
1480 <xsl:apply-templates select="*[5]" mode="root_charcount"/>
1482 <xsl:variable name="split1"
1483 select="($charlength_first + $charlength_second) > $framewidth"/>
1484 <xsl:variable name="split2"
1485 select="($charlength_second + $charlength_side_proof) > $framewidth"/>
1486 <!-- <xsl:value-of select="$current_indent"/> -->
1487 <!-- <xsl:value-of select="string($charlength_second)"/> -->
1488 <!-- <xsl:value-of select="$charlength_side_proof"/> -->
1489 <!-- <xsl:value-of select="$split2"/> -->
1491 <xsl:call-template name="make_indent">
1492 <xsl:with-param name="current_indent" select="$current_indent"/>
1493 </xsl:call-template>
1494 <FONT color="red">Rewrite </FONT>
1495 <xsl:apply-templates mode="inline" select="*[3]"/>
1496 <xsl:text> </xsl:text>
1497 <xsl:if test="$split1">
1499 <xsl:call-template name="make_indent">
1500 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1501 </xsl:call-template>
1503 <FONT color="red">with </FONT>
1504 <xsl:apply-templates mode="inline" select="*[4]"/>
1505 <xsl:text> </xsl:text>
1506 <xsl:if test="$split2">
1508 <xsl:call-template name="make_indent">
1509 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1510 </xsl:call-template>
1512 <FONT color="red">by </FONT>
1513 <xsl:apply-templates select="*[5]">
1514 <xsl:with-param name="current_indent" select="$current_indent+7"/>
1515 </xsl:apply-templates>
1517 <!-- rewrite and apply -->
1518 <xsl:when test="$name='rewrite_and_apply'">
1519 <xsl:apply-templates select="*[2]">
1520 <xsl:with-param name="current_indent" select="$current_indent"/>
1521 </xsl:apply-templates>
1523 <xsl:call-template name="make_indent">
1524 <xsl:with-param name="current_indent" select="$current_indent"/>
1525 </xsl:call-template>
1526 <FONT color="red">Then apply it to </FONT>
1527 <xsl:apply-templates select="*[position()>2]"/>
1529 <!-- by_induction -->
1530 <xsl:when test="$name='by_induction'">
1531 <FONT color="red">We prove </FONT>
1532 <xsl:apply-templates select="../*[3]">
1533 <xsl:with-param name="current_indent" select="$current_indent+18"/>
1534 </xsl:apply-templates>
1536 <xsl:call-template name="make_indent">
1537 <xsl:with-param name="current_indent" select="$current_indent"/>
1538 </xsl:call-template>
1539 <FONT color="red">by induction on </FONT>
1540 <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
1541 <xsl:with-param name="current_indent" select="$current_indent+30"/>
1542 </xsl:apply-templates>
1545 <xsl:call-template name="make_indent">
1546 <xsl:with-param name="current_indent" select="$current_indent"/>
1547 </xsl:call-template>
1548 <xsl:text>The induction property is</xsl:text>
1550 <xsl:call-template name="make_indent">
1551 <xsl:with-param name="current_indent" select="$current_indent"/>
1552 </xsl:call-template>
1553 <xsl:apply-templates select="*[3]">
1554 <xsl:with-param name="current_indent" select="$current_indent"/>
1555 </xsl:apply-templates>
1557 <xsl:apply-templates
1558 select="*[position()>3 and not(position()=last())]">
1559 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1560 </xsl:apply-templates>
1562 <xsl:call-template name="make_indent">
1563 <xsl:with-param name="current_indent" select="$current_indent"/>
1564 </xsl:call-template>
1565 <xsl:text>End induction</xsl:text> -->
1567 <!-- inductive_case -->
1568 <xsl:when test="$name='inductive_case'">
1570 <xsl:call-template name="make_indent">
1571 <xsl:with-param name="current_indent" select="$current_indent"/>
1572 </xsl:call-template>
1573 <FONT color="red">Case </FONT>
1574 <xsl:apply-templates select="*[2]">
1575 <xsl:with-param name="current_indent" select="$current_indent +10"/>
1576 </xsl:apply-templates>
1577 <xsl:if test="*[3]/*[position()>1]">
1579 <xsl:call-template name="make_indent">
1580 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1581 </xsl:call-template>
1582 <FONT color="red">By induction hypothesis, we have:</FONT>
1583 <xsl:for-each select="*[3]/*[position()>1]">
1585 <xsl:call-template name="make_indent">
1586 <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1587 </xsl:call-template>
1588 <xsl:text>(</xsl:text>
1589 <xsl:apply-templates select="m:ci"/>
1590 <xsl:text>) </xsl:text>
1591 <xsl:apply-templates select="m:type">
1592 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1593 </xsl:apply-templates>
1597 <xsl:call-template name="make_indent">
1598 <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1599 </xsl:call-template>
1600 <xsl:apply-templates select="*[4]">
1601 <xsl:with-param name="current_indent" select="$current_indent +4"/>
1602 </xsl:apply-templates>
1604 <xsl:call-template name="make_indent">
1605 <xsl:with-param name="current_indent" select="$current_indent"/>
1606 </xsl:call-template>
1607 <xsl:text>End Case</xsl:text> -->
1610 <xsl:when test="$name='case_lhs'">
1612 <xsl:when test="count(*)=2">
1613 <xsl:apply-templates mode="inline" select="*[2]"/>
1616 <xsl:text>(</xsl:text>
1617 <xsl:apply-templates mode="inline" select="*[2]"/>
1618 <xsl:for-each select="m:bvar">
1619 <xsl:text> </xsl:text>
1620 <xsl:apply-templates mode="inline" select="*[1]"/>
1621 <xsl:text>:</xsl:text>
1622 <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1624 <xsl:text>)</xsl:text>
1629 <xsl:when test="$name='false_ind'">
1630 <xsl:apply-templates select="*[3]">
1631 <xsl:with-param name="current_indent" select="$current_indent"/>
1632 </xsl:apply-templates>
1634 <xsl:call-template name="make_indent">
1635 <xsl:with-param name="current_indent" select="$current_indent"/>
1636 </xsl:call-template>
1637 <FONT color="red">Contradiction.</FONT>
1640 <xsl:when test="$name='and_ind'">
1642 <xsl:when test="name(*[2])='m:apply'">
1643 <xsl:apply-templates select="*[2]">
1644 <xsl:with-param name="current_indent" select="$current_indent"/>
1645 </xsl:apply-templates>
1648 <FONT color="red">Consider </FONT>
1649 <xsl:apply-templates select="*[2]"/>
1653 <xsl:call-template name="make_indent">
1654 <xsl:with-param name="current_indent" select="$current_indent"/>
1655 </xsl:call-template>
1656 <FONT color="red">In particular, we have</FONT>
1658 <xsl:call-template name="make_indent">
1659 <xsl:with-param name="current_indent" select="$current_indent"/>
1660 </xsl:call-template>
1662 <xsl:apply-templates select="*[3]"/>
1664 <xsl:apply-templates select="*[4]">
1665 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1666 </xsl:apply-templates>
1668 <xsl:call-template name="make_indent">
1669 <xsl:with-param name="current_indent" select="$current_indent"/>
1670 </xsl:call-template>
1672 <xsl:apply-templates select="*[5]"/>
1674 <xsl:apply-templates select="*[6]">
1675 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1676 </xsl:apply-templates>
1678 <xsl:call-template name="make_indent">
1679 <xsl:with-param name="current_indent" select="$current_indent"/>
1680 </xsl:call-template>
1681 <xsl:apply-templates select="*[7]">
1682 <xsl:with-param name="current_indent" select="$current_indent"/>
1683 </xsl:apply-templates>
1685 <!-- full_or_ind -->
1686 <xsl:when test="$name='full_or_ind'">
1688 <xsl:when test="name(*[2])='m:apply'">
1689 <xsl:apply-templates select="*[2]">
1690 <xsl:with-param name="current_indent" select="$current_indent"/>
1691 </xsl:apply-templates>
1694 <FONT color="red">Consider </FONT>
1695 <xsl:apply-templates select="*[2]"/>
1699 <xsl:call-template name="make_indent">
1700 <xsl:with-param name="current_indent" select="$current_indent"/>
1701 </xsl:call-template>
1702 <FONT color="red">We proceed by cases to prove </FONT>
1703 <xsl:apply-templates select="*[3]"/>
1705 <xsl:call-template name="make_indent">
1706 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1707 </xsl:call-template>
1708 <FONT color="red">Left: suppose </FONT>
1709 <xsl:text>(</xsl:text>
1710 <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1711 <xsl:text>) </xsl:text>
1712 <xsl:apply-templates
1713 select="*[4]/m:bvar/m:type/*[1]"/>
1715 <xsl:call-template name="make_indent">
1716 <xsl:with-param name="current_indent" select="$current_indent+15"/>
1717 </xsl:call-template>
1718 <xsl:apply-templates
1720 <xsl:with-param name="current_indent" select="$current_indent+15"/>
1721 </xsl:apply-templates>
1723 <xsl:call-template name="make_indent">
1724 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1725 </xsl:call-template>
1726 <FONT color="red">Right: suppose </FONT>
1727 <xsl:text>(</xsl:text>
1728 <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1729 <xsl:text>) </xsl:text>
1730 <xsl:apply-templates
1731 select="*[5]/m:bvar/m:type/*[1]"/>
1733 <xsl:call-template name="make_indent">
1734 <xsl:with-param name="current_indent" select="$current_indent+16"/>
1735 </xsl:call-template>
1736 <xsl:apply-templates
1738 <xsl:with-param name="current_indent" select="$current_indent+16"/>
1739 </xsl:apply-templates>
1742 <xsl:when test="$name='or_ind'">
1744 <xsl:when test="name(*[2])='m:apply'">
1745 <xsl:apply-templates select="*[2]">
1746 <xsl:with-param name="current_indent" select="$current_indent"/>
1747 </xsl:apply-templates>
1750 <FONT color="red">Consider </FONT>
1751 <xsl:apply-templates select="*[2]"/>
1755 <xsl:call-template name="make_indent">
1756 <xsl:with-param name="current_indent" select="$current_indent"/>
1757 </xsl:call-template>
1758 <FONT color="red">We prove </FONT>
1759 <xsl:apply-templates select="*[3]"/>
1760 <FONT color="red"> by cases:</FONT>
1762 <xsl:call-template name="make_indent">
1763 <xsl:with-param name="current_indent" select="$current_indent"/>
1764 </xsl:call-template>
1766 <xsl:apply-templates select="*[4]">
1767 <xsl:with-param name="current_indent" select="$current_indent"/>
1768 </xsl:apply-templates>
1770 <xsl:call-template name="make_indent">
1771 <xsl:with-param name="current_indent" select="$current_indent"/>
1772 </xsl:call-template>
1774 <xsl:apply-templates select="*[5]">
1775 <xsl:with-param name="current_indent" select="$current_indent"/>
1776 </xsl:apply-templates>
1779 <xsl:when test="$name='ex_ind'">
1781 <xsl:when test="name(*[2])='m:apply'">
1782 <xsl:apply-templates select="*[2]">
1783 <xsl:with-param name="current_indent" select="$current_indent"/>
1784 </xsl:apply-templates>
1787 <FONT color="red">Consider </FONT>
1788 <xsl:apply-templates select="*[2]">
1789 <xsl:with-param name="current_indent" select="$current_indent"/>
1790 </xsl:apply-templates>
1794 <xsl:call-template name="make_indent">
1795 <xsl:with-param name="current_indent" select="$current_indent"/>
1796 </xsl:call-template>
1797 <FONT color="red">Let </FONT>
1798 <xsl:apply-templates mode="inline" select="*[3]"/>
1800 <xsl:apply-templates mode="inline" select="*[4]"/>
1801 <FONT color="red"> such that</FONT>
1803 <xsl:call-template name="make_indent">
1804 <xsl:with-param name="current_indent" select="$current_indent"/>
1805 </xsl:call-template>
1807 <xsl:apply-templates mode="inline" select="*[5]"/>
1809 <xsl:apply-templates select="*[6]">
1810 <xsl:with-param name="current_indent" select="$current_indent +7"/>
1811 </xsl:apply-templates>
1813 <xsl:call-template name="make_indent">
1814 <xsl:with-param name="current_indent" select="$current_indent"/>
1815 </xsl:call-template>
1816 <xsl:apply-templates select="*[7]">
1817 <xsl:with-param name="current_indent" select="$current_indent"/>
1818 </xsl:apply-templates>
1820 <!-- ***************************************** -->
1821 <!-- *********** LAMBDA ELEMENTS ************** -->
1822 <!-- ***************************************** -->
1823 <xsl:when test="$name='subst'">
1824 <xsl:apply-templates select="*[3]"/>
1825 <xsl:text>[</xsl:text>
1826 <xsl:apply-templates select="*[4]"/>
1828 <xsl:when test="$uri != ''">
1830 <xsl:call-template name="mksymbol-1">
1831 <xsl:with-param name="symbol" select="$name"/>
1832 <xsl:with-param name="color" select="'blue'"/>
1833 <xsl:with-param name="size" select="'+0'"/>
1834 </xsl:call-template>
1838 <xsl:call-template name="mksymbol-1">
1839 <xsl:with-param name="symbol" select="$name"/>
1840 <xsl:with-param name="color" select="'blue'"/>
1841 <xsl:with-param name="size" select="'+0'"/>
1842 </xsl:call-template>
1845 <xsl:apply-templates select="*[2]"/>
1846 <xsl:text>]</xsl:text>
1849 <xsl:when test="$name='lift_with_base'">
1851 <xsl:apply-templates select="*[3]" mode="inline"/>
1854 <xsl:when test="$uri != ''">
1856 <xsl:call-template name="mksymbol-1">
1857 <xsl:with-param name="symbol" select="$name"/>
1858 <xsl:with-param name="color" select="'green'"/>
1859 <xsl:with-param name="size" select="'+0'"/>
1860 </xsl:call-template>
1864 <xsl:call-template name="mksymbol-1">
1865 <xsl:with-param name="symbol" select="$name"/>
1866 <xsl:with-param name="color" select="'green'"/>
1867 <xsl:with-param name="size" select="'+0'"/>
1868 </xsl:call-template>
1872 <xsl:apply-templates select="*[4]" mode="inline"/>
1874 <xsl:text>(</xsl:text>
1875 <xsl:apply-templates select="*[2]" mode="inline"/>
1876 <xsl:text>)</xsl:text>
1879 <xsl:when test="$name='lift'">
1881 <xsl:when test="$uri != ''">
1883 <xsl:call-template name="mksymbol-1">
1884 <xsl:with-param name="symbol" select="$name"/>
1885 <xsl:with-param name="color" select="'green'"/>
1886 <xsl:with-param name="size" select="'+0'"/>
1887 </xsl:call-template>
1891 <xsl:call-template name="mksymbol-1">
1892 <xsl:with-param name="symbol" select="$name"/>
1893 <xsl:with-param name="color" select="'green'"/>
1894 <xsl:with-param name="size" select="'+0'"/>
1895 </xsl:call-template>
1899 <xsl:apply-templates select="*[2]" mode="inline"/>
1901 <xsl:text>(</xsl:text>
1902 <xsl:apply-templates select="*[3]" mode="inline"/>
1903 <xsl:text>)</xsl:text>
1907 <xsl:when test="$name='beta_red1'">
1908 <xsl:apply-templates select="*[2]" mode="inline"/>
1910 <xsl:when test="$uri != ''">
1912 <xsl:call-template name="mksymbol-1">
1913 <xsl:with-param name="symbol" select="$name"/>
1914 <xsl:with-param name="color" select="'green'"/>
1915 <xsl:with-param name="size" select="'+0'"/>
1916 </xsl:call-template>
1918 <xsl:call-template name="mksymbol-1">
1919 <xsl:with-param name="symbol" select="'beta'"/>
1920 <xsl:with-param name="color" select="'green'"/>
1921 <xsl:with-param name="size" select="'+0'"/>
1922 </xsl:call-template>
1927 <xsl:call-template name="mksymbol-1">
1928 <xsl:with-param name="symbol" select="$name"/>
1929 <xsl:with-param name="color" select="'green'"/>
1930 <xsl:with-param name="size" select="'+0'"/>
1931 </xsl:call-template>
1933 <xsl:call-template name="mksymbol-1">
1934 <xsl:with-param name="symbol" select="'beta'"/>
1935 <xsl:with-param name="color" select="'green'"/>
1936 <xsl:with-param name="size" select="'+0'"/>
1937 </xsl:call-template>
1941 <xsl:apply-templates select="*[3]" mode="inline"/>
1944 <xsl:when test="$name='beta_red'">
1945 <xsl:apply-templates select="*[2]" mode="inline"/>
1947 <xsl:when test="$uri != ''">
1949 <xsl:call-template name="mksymbol-1">
1950 <xsl:with-param name="symbol" select="$name"/>
1951 <xsl:with-param name="color" select="'green'"/>
1952 <xsl:with-param name="size" select="'+0'"/>
1953 </xsl:call-template>
1955 <xsl:call-template name="mksymbol-1">
1956 <xsl:with-param name="symbol" select="'beta'"/>
1957 <xsl:with-param name="color" select="'green'"/>
1958 <xsl:with-param name="size" select="'+0'"/>
1959 </xsl:call-template>
1960 <xsl:text>*</xsl:text>
1965 <xsl:call-template name="mksymbol-1">
1966 <xsl:with-param name="symbol" select="$name"/>
1967 <xsl:with-param name="color" select="'green'"/>
1968 <xsl:with-param name="size" select="'+0'"/>
1969 </xsl:call-template>
1971 <xsl:call-template name="mksymbol-1">
1972 <xsl:with-param name="symbol" select="'beta'"/>
1973 <xsl:with-param name="color" select="'green'"/>
1974 <xsl:with-param name="size" select="'+0'"/>
1975 </xsl:call-template>
1976 <xsl:text>*</xsl:text>
1980 <xsl:apply-templates select="*[3]" mode="inline"/>
1983 <xsl:when test="$name='par_beta_red1'">
1984 <xsl:apply-templates select="*[2]" mode="inline"/>
1986 <xsl:when test="$uri != ''">
1988 <xsl:call-template name="mksymbol-1">
1989 <xsl:with-param name="symbol" select="$name"/>
1990 <xsl:with-param name="color" select="'green'"/>
1991 <xsl:with-param name="size" select="'+0'"/>
1992 </xsl:call-template>
1994 <xsl:call-template name="mksymbol-1">
1995 <xsl:with-param name="symbol" select="'beta'"/>
1996 <xsl:with-param name="color" select="'green'"/>
1997 <xsl:with-param name="size" select="'+0'"/>
1998 </xsl:call-template>
2003 <xsl:call-template name="mksymbol-1">
2004 <xsl:with-param name="symbol" select="$name"/>
2005 <xsl:with-param name="color" select="'green'"/>
2006 <xsl:with-param name="size" select="'+0'"/>
2007 </xsl:call-template>
2009 <xsl:call-template name="mksymbol-1">
2010 <xsl:with-param name="symbol" select="'beta'"/>
2011 <xsl:with-param name="color" select="'green'"/>
2012 <xsl:with-param name="size" select="'+0'"/>
2013 </xsl:call-template>
2017 <xsl:apply-templates select="*[3]" mode="inline"/>
2020 <xsl:when test="$name='par_beta_red'">
2021 <xsl:apply-templates select="*[2]" mode="inline"/>
2023 <xsl:when test="$uri != ''">
2025 <xsl:call-template name="mksymbol-1">
2026 <xsl:with-param name="symbol" select="$name"/>
2027 <xsl:with-param name="color" select="'green'"/>
2028 <xsl:with-param name="size" select="'+0'"/>
2029 </xsl:call-template>
2031 <xsl:call-template name="mksymbol-1">
2032 <xsl:with-param name="symbol" select="'beta'"/>
2033 <xsl:with-param name="color" select="'green'"/>
2034 <xsl:with-param name="size" select="'+0'"/>
2035 </xsl:call-template>
2036 <xsl:text>*</xsl:text>
2041 <xsl:call-template name="mksymbol-1">
2042 <xsl:with-param name="symbol" select="$name"/>
2043 <xsl:with-param name="color" select="'green'"/>
2044 <xsl:with-param name="size" select="'+0'"/>
2045 </xsl:call-template>
2047 <xsl:call-template name="mksymbol-1">
2048 <xsl:with-param name="symbol" select="'beta'"/>
2049 <xsl:with-param name="color" select="'green'"/>
2050 <xsl:with-param name="size" select="'+0'"/>
2051 </xsl:call-template>
2052 <xsl:text>*</xsl:text>
2056 <xsl:apply-templates select="*[3]" mode="inline"/>
2060 <xsl:when test="$name='forgetful'">
2062 <xsl:when test="$uri != ''">
2063 <a href="{$uri}">|</a>
2069 <xsl:apply-templates select="*[2]" mode="inline"/>
2071 <xsl:when test="$uri != ''">
2072 <a href="{$uri}">|</a>
2080 <!-- boolean algebra of redexes -->
2083 <xsl:when test="$name='isomorphic'">
2084 <xsl:apply-templates select="*[2]" mode="inline"/>
2086 <xsl:when test="$uri != ''">
2088 <xsl:call-template name="mksymbol-1">
2089 <xsl:with-param name="symbol" select="$name"/>
2090 <xsl:with-param name="color" select="'green'"/>
2091 <xsl:with-param name="size" select="'+0'"/>
2092 </xsl:call-template>
2096 <xsl:call-template name="mksymbol-1">
2097 <xsl:with-param name="symbol" select="$name"/>
2098 <xsl:with-param name="color" select="'green'"/>
2099 <xsl:with-param name="size" select="'+0'"/>
2100 </xsl:call-template>
2103 <xsl:apply-templates select="*[3]" mode="inline"/>
2107 <xsl:when test="$name='interp'">
2108 <font color="green">[</font>
2109 <xsl:apply-templates select="*[2]"/>
2110 <font color="green">]</font>
2118 <xsl:template match="m:lambda">
2119 <xsl:param name="current_indent" select="0"/>
2120 <xsl:variable name="charlength">
2121 <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
2122 <!-- <xsl:apply-templates select="." mode="charcount"/> -->
2124 <!-- <xsl:value-of select="$charlength"/> -->
2125 <!-- <xsl:value-of select="$current_indent"/> -->
2127 <xsl:when test="$charlength > $framewidth">
2129 <xsl:call-template name="mksymbol-1">
2130 <xsl:with-param name="symbol" select="'lambda'"/>
2131 <xsl:with-param name="color" select="'red'"/>
2132 <xsl:with-param name="size" select="'+2'"/>
2133 </xsl:call-template>
2134 <xsl:apply-templates select="m:bvar/m:ci"/>
2135 <xsl:text>:</xsl:text>
2136 <xsl:apply-templates select="m:bvar/m:type">
2137 <xsl:with-param name="current_indent"
2138 select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
2139 </xsl:apply-templates><br/>
2140 <xsl:call-template name="make_indent">
2141 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2142 </xsl:call-template>
2143 <xsl:text>.</xsl:text>
2144 <xsl:apply-templates select="*[position()=2]">
2145 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2146 </xsl:apply-templates>
2149 <xsl:apply-templates mode="inline" select="."/>
2155 <xsl:template match="m:ci">
2157 <xsl:when test="boolean(@definitionURL)">
2158 <a href="{@definitionURL}">
2159 <xsl:apply-templates/>
2163 <xsl:value-of select="."/>
2168 <!-- CHAR COUNTING -->
2170 <!-- enter this counting mode selecting the root -->
2171 <xsl:template match="*" mode="root_charcount">
2172 <xsl:param name="incurrent_length" select="0"/>
2174 <xsl:when test="count(*)=0">
2175 <xsl:value-of select="0"/>
2177 <xsl:when test="name()='m:ci'">
2178 <xsl:value-of select="string-length()"/>
2181 <xsl:apply-templates select="*[1]" mode="charcount">
2182 <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
2183 </xsl:apply-templates>
2188 <!-- enter this mode selecting the first child -->
2190 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2191 <xsl:param name="incurrent_length" select="0"/>
2193 <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
2194 <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>
2196 <xsl:when test="string($siblength) = """>
2197 <xsl:value-of select="$incurrent_length + string-length()"/>
2200 <xsl:value-of select="number($siblength)"/>
2205 <xsl:value-of select="$incurrent_length + string-length()"/>
2210 <xsl:template match="*" mode="charcount">
2211 <xsl:param name="incurrent_length" select="0"/>
2213 <xsl:when test="count(child::*) = 0">
2214 <xsl:value-of select="$incurrent_length"/>
2217 <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
2219 <xsl:when test="$framewidth >= number($childlength)">
2220 <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>
2222 <xsl:when test="string($siblength) = """>
2223 <xsl:value-of select="number($childlength)"/>
2226 <xsl:value-of select="number($siblength)"/>
2231 <xsl:value-of select="number($childlength)"/>
2239 <!--***********************************************************************-->
2241 <!--***********************************************************************-->
2245 <xsl:template match="Definition">
2246 <xsl:param name="current_indent" select="0"/>
2248 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2250 <xsl:call-template name="make_indent">
2251 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2252 </xsl:call-template>
2253 <xsl:apply-templates select="type/*[1]">
2254 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2255 </xsl:apply-templates><br/>
2257 <xsl:call-template name="make_indent">
2258 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2259 </xsl:call-template>
2260 <xsl:apply-templates select="body/*[1]">
2261 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2262 </xsl:apply-templates>
2268 <xsl:template match="Axiom">
2269 <xsl:param name="current_indent" select="0"/>
2271 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2273 <xsl:call-template name="make_indent">
2274 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2275 </xsl:call-template>
2276 <xsl:apply-templates select="type/*[1]">
2277 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2278 </xsl:apply-templates>
2282 <!-- UNFINISHED PROOF -->
2284 <xsl:template match="CurrentProof">
2285 <xsl:param name="current_indent" select="0"/>
2287 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2288 THESIS: <xsl:apply-templates select="type/*[1]">
2289 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2290 </xsl:apply-templates><br/>
2292 <xsl:for-each select="Conjecture">
2294 <xsl:call-template name="make_indent">
2295 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2296 </xsl:call-template>
2297 <xsl:for-each select="Decl|Def|Hidden">
2299 <xsl:when test="name(.)='Decl'">
2301 <xsl:when test="@name">
2302 <xsl:value-of select="@name"/>
2305 <xsl:text>_</xsl:text>
2308 <xsl:text> : </xsl:text>
2309 <xsl:apply-templates select="./*[1]">
2310 <xsl:with-param name="current_indent" select="$current_indent"/>
2311 </xsl:apply-templates>
2313 <xsl:when test="name(.)='Def'">
2315 <xsl:when test="@name">
2316 <xsl:value-of select="@name"/>
2319 <xsl:text>_</xsl:text>
2322 <xsl:text> := </xsl:text>
2323 <xsl:apply-templates select="./*[1]">
2324 <xsl:with-param name="current_indent" select="$current_indent"/>
2325 </xsl:apply-templates>
2328 <xsl:text> _ :? _ </xsl:text>
2332 |- <xsl:value-of select="./@no"/> :
2333 <xsl:apply-templates select="./Goal/*[1]">
2334 <xsl:with-param name="current_indent" select="$current_indent + 11"/>
2335 </xsl:apply-templates>
2339 <xsl:apply-templates select="body/*[1]">
2340 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2341 </xsl:apply-templates>
2345 <!-- MUTUAL INDUCTIVE DEFINITION -->
2347 <xsl:template match="InductiveDefinition">
2348 <xsl:param name="current_indent" select="0"/>
2350 <xsl:for-each select="InductiveType">
2352 <xsl:when test="position() = 1">
2354 <xsl:when test="string(./@inductive) = "true"">
2355 INDUCTIVE DEFINITION
2358 COINDUCTIVE DEFINITION
2366 <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != """><xsl:value-of select="../Params"/></xsl:if>)
2368 <xsl:if test="string(../Param) != """>
2369 <xsl:for-each select="../Param">
2370 <xsl:value-of select="./@name"/>
2372 <xsl:apply-templates select="*"/>
2377 <xsl:apply-templates select="./arity/*[1]">
2378 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2379 </xsl:apply-templates> <br/>
2381 <xsl:for-each select="./Constructor">
2383 <xsl:call-template name="make_indent">
2384 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
2385 </xsl:call-template>
2387 <xsl:when test="position() = 1">
2388 <xsl:text>  </xsl:text>
2391 <xsl:text>| </xsl:text>
2394 <xsl:value-of select="./@name"/>
2395 <xsl:text>: </xsl:text>
2396 <xsl:apply-templates select="./*[1]">
2397 <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
2398 </xsl:apply-templates>
2406 <xsl:template match="Variable">
2407 <xsl:param name="current_indent" select="0"/>
2409 VARIABLE <xsl:value-of select="@name"/><br/>
2410 TYPE = <xsl:apply-templates select="type/*[1]">
2411 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2412 </xsl:apply-templates>
2413 <xsl:if test="body">
2415 BODY = <xsl:apply-templates select="body/*[1]">
2416 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2417 </xsl:apply-templates>
2422 <!--***********************************************************************-->
2424 <!--***********************************************************************-->
2428 <xsl:template match="SECTION">
2429 <xsl:param name="current_indent" select="0"/>
2430 <h1>BEGIN OF SECTION</h1>
2431 <xsl:apply-templates/>
2432 <h1>END OF SECTION</h1>