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 <!--***********************************************************************-->
28 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
29 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena -->
30 <!-- Revised: March 3 2000, Irene Schena -->
31 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena -->
32 <!-- Revised: March 21 2000, Irene Schena -->
33 <!--***********************************************************************-->
35 <!-- NOTE: the namespace declaration has to be done in the stylesheets
36 which generates the toplevel element (see for instance xlink) -->
37 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
38 xmlns:m="http://www.w3.org/1998/Math/MathML"
39 xmlns:helm="http://www.cs.unibo.it/helm"
40 xmlns:xlink="http://www.w3.org/1999/xlink">
42 <!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
44 <xsl:import href="mmlnotation.xsl"/>
46 <xsl:import href="mmltheoryextension.xsl"/>
49 <xsl:param name="explodeall" select="false()"/>
51 <!--***********************************************************************-->
52 <!-- Parameter affecting line-breaking -->
53 <!--***********************************************************************-->
55 <xsl:variable name="framewidth" select="35"/>
57 <!--***********************************************************************-->
58 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
59 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti -->
60 <!-- sono i termini: la presentation per un termine e' generata come primo -->
61 <!-- figlio di un semantics e l'originario content viene inserito nel -->
62 <!-- nel secondo figlio di semantics, annotation-xml -->
63 <!--***********************************************************************-->
65 <!--**********************-->
67 <!--**********************-->
69 <xsl:param name="type" select="'standalone'"/>
71 <xsl:template match="/">
73 <xsl:when test="$type = 'standalone'">
74 <xsl:apply-templates select="*"/>
78 <xsl:apply-templates select="*"/>
86 <xsl:template match="Definition">
88 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
92 <m:mtext>DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
99 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
100 <xsl:apply-templates select="type/*[1]"/>
107 <m:mtext>AS</m:mtext>
114 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
115 <xsl:apply-templates select="body/*[1]"/>
125 <xsl:template match="Axiom">
127 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
131 <m:mtext>AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
138 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
139 <xsl:apply-templates select="type/*[1]"/>
147 <!-- UNFINISHED PROOF -->
149 <xsl:template match="CurrentProof">
151 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
155 <m:mtext>UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)</m:mtext>
162 <m:mtext>THESIS:</m:mtext>
169 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
170 <xsl:apply-templates select="type/*[1]"/>
177 <m:mtext>CONJECTURES:</m:mtext>
181 <xsl:for-each select="Conjecture">
185 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
186 <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
188 <xsl:apply-templates select="./*[1]"/>
196 <m:mtext>PROOF:</m:mtext>
203 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
204 <xsl:apply-templates select="body/*[1]"/>
212 <!-- MUTUAL INDUCTIVE DEFINITION -->
214 <xsl:template match="InductiveDefinition">
216 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
217 <xsl:for-each select="InductiveType">
222 <xsl:when test="position() = 1">
224 <xsl:when test="string(./@inductive) = "true"">
225 <m:mtext>INDUCTIVE DEFINITION</m:mtext>
228 <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
233 <m:mtext>AND</m:mtext>
236 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
237 <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != """><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
244 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
247 <xsl:when test="string(../Param) != """>
248 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
249 <xsl:for-each select="../Param">
253 <m:mi><xsl:value-of select="./@name"/></m:mi>
255 <xsl:apply-templates select="*"/>
279 <m:mtext>OF ARITY</m:mtext>
286 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
287 <xsl:apply-templates select="./arity/*[1]"/>
294 <m:mtext>BUILT FROM</m:mtext>
298 <xsl:for-each select="./Constructor">
303 <xsl:when test="position() = 1">
304 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
308 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
311 <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
312 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
313 <xsl:apply-templates select="./*[1]"/>
325 <xsl:template match="Variable">
327 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
331 <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
338 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
339 <xsl:apply-templates select="type/*[1]"/>
343 <xsl:if test="name(*[1])='body'">
347 <m:mtext>AS</m:mtext>
354 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
355 <xsl:apply-templates select="body/*[1]"/>
366 <xsl:template match="Sequent">
368 <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
369 <xsl:for-each select="Declaration|Definition">
373 <m:mi><xsl:value-of select="@name"/></m:mi>
375 <xsl:when test="name(.) = 'Declaration'">
382 <xsl:apply-templates select="*[1]"/>
390 <m:mtext>========================================</m:mtext>
397 <xsl:apply-templates select="Goal/*[1]"/>
405 <!--**********************-->
407 <!--**********************-->
409 <xsl:template match="m:bvar">
411 <xsl:when test="m:type">
412 <xsl:variable name="charlength">
413 <xsl:apply-templates select="m:ci" mode="charcount"/>
416 <xsl:when test="$charlength >= $framewidth">
417 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
421 <xsl:apply-templates select="m:ci"/>
429 <xsl:apply-templates select="m:type"/>
437 <xsl:apply-templates select="m:ci"/>
439 <xsl:apply-templates select="m:type"/>
445 <xsl:apply-templates select="m:ci"/>
453 <xsl:template match="m:apply[m:csymbol]">
454 <xsl:param name="nopar" select="0"/>
455 <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
456 <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
459 <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
461 <xsl:variable name="id" select="m:csymbol/@id"/>
464 <xsl:when test="$name='forall'">
466 <xsl:when test="$charlength >= $framewidth">
467 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
471 <m:mo mathcolor="Blue">∀</m:mo>
472 <xsl:apply-templates select="m:bvar"/>
480 <xsl:apply-templates select="*[position()=3]"/>
487 <m:mo mathcolor="Blue">∀</m:mo>
488 <xsl:apply-templates select="m:bvar/m:ci"/>
490 <xsl:apply-templates select="m:bvar/m:type"/>
492 <xsl:apply-templates select="*[position()=3]"/>
497 <xsl:when test="$name='let_in'">
499 <xsl:when test="$charlength >= $framewidth">
500 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
505 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
506 <xsl:apply-templates select="m:bvar"/>
514 <xsl:apply-templates select="*[position()=3]"/>
522 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
523 <xsl:apply-templates select="*[position()=4]"/>
531 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
532 <xsl:apply-templates select="m:bvar/m:ci"/>
534 <xsl:apply-templates select="*[position()=3]"/>
535 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
536 <m:mtext>IN</m:mtext>
537 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
538 <xsl:apply-templates select="*[position()=4]"/>
543 <xsl:when test="$name='prod'">
545 <xsl:when test="$charlength >= $framewidth">
546 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
550 <m:mo mathcolor="Blue">Π</m:mo>
551 <xsl:apply-templates select="m:bvar"/>
559 <xsl:apply-templates select="*[position()=3]"/>
566 <m:mo mathcolor="Blue">Π</m:mo>
567 <xsl:apply-templates select="m:bvar/m:ci"/>
569 <xsl:apply-templates select="m:bvar/m:type"/>
571 <xsl:apply-templates select="*[position()=3]"/>
576 <xsl:when test="$name='arrow'">
578 <xsl:when test="$charlength >= $framewidth">
579 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
583 <xsl:if test="$nopar=0">
584 <m:mo stretchy="false">(</m:mo>
586 <xsl:apply-templates select="*[position()=2]"/>
593 <m:mo mathmathcolor="Blue">→</m:mo>
595 <xsl:when test="*[position()=3]/m:csymbol">
596 <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
598 <xsl:when test="$nextp='arrow'">
599 <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
602 <xsl:apply-templates select="*[position()=3]"/>
607 <xsl:apply-templates select="*[position()=3]"/>
613 <xsl:if test="$nopar=0">
617 <m:mo stretchy="false">)</m:mo>
625 <xsl:if test="$nopar=0">
626 <m:mo stretchy="false">(</m:mo>
628 <xsl:apply-templates select="*[position()=2]"/>
629 <m:mo mathcolor="Blue">→</m:mo>
631 <xsl:when test="*[position()=3]/m:csymbol">
632 <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
634 <xsl:when test="$nextp='arrow'">
635 <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
638 <xsl:apply-templates select="*[position()=3]"/>
643 <xsl:apply-templates select="*[position()=3]"/>
646 <xsl:if test="$nopar=0">
647 <m:mo stretchy="false">)</m:mo>
653 <xsl:when test="$name='app'">
655 <xsl:when test="$charlength >= $framewidth">
656 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
660 <m:mo stretchy="false">(</m:mo>
661 <!-- added precedence to app = FUNCTION_PREC (99) -->
662 <xsl:apply-templates select="*[position()=2]">
663 <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
664 </xsl:apply-templates>
668 <xsl:for-each select="*[position()>2]">
672 <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
673 <!-- added precedence to app = FUNCTION_PREC (99) -->
674 <xsl:apply-templates select=".">
675 <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
676 </xsl:apply-templates>
684 <m:mo stretchy="false">)</m:mo>
691 <m:mo stretchy="false">(</m:mo>
692 <!-- added precedence to app = FUNCTION_PREC (99) -->
693 <xsl:apply-templates select="*[position()=2]">
694 <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
695 </xsl:apply-templates>
696 <xsl:for-each select="*[position()>2]">
697 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
698 <!-- added precedence to app = FUNCTION_PREC (99) -->
699 <xsl:apply-templates select=".">
700 <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
701 </xsl:apply-templates>
703 <m:mo stretchy="false">)</m:mo>
708 <xsl:when test="$name='cast'">
710 <xsl:when test="$charlength >= $framewidth">
711 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
715 <m:mo stretchy="false">(</m:mo>
716 <xsl:apply-templates select="*[position()=2]"/>
723 <m:mo mathcolor="Maroon">:></m:mo>
724 <xsl:apply-templates select="*[position()=3]"/>
731 <m:mo stretchy="false">)</m:mo>
738 <m:mo stretchy="false">(</m:mo>
739 <xsl:apply-templates select="*[position()=2]"/>
740 <m:mo mathcolor="Maroon">:></m:mo>
741 <xsl:apply-templates select="*[position()=3]"/>
742 <m:mo stretchy="false">)</m:mo>
747 <xsl:when test="$name='Prop'">
751 <xsl:when test="$name='Set'">
755 <xsl:when test="$name='Type'">
759 <xsl:when test="$name='mutcase'">
761 <xsl:when test="$charlength >= $framewidth">
762 <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
763 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
768 <xsl:apply-templates select="*[position()=2]"/>
769 <xsl:if test="$framewidth > $charlength">
772 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
773 <xsl:apply-templates select="*[position()=3]"/>
778 <xsl:if test="$charlength >= $framewidth">
784 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
785 <xsl:apply-templates select="*[position()=3]"/>
797 <xsl:for-each select="piecewise/piece">
798 <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
803 <xsl:when test="position() = 1">
804 <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
807 <m:mo stretchy="false">|</m:mo>
810 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
811 <xsl:apply-templates select="./*[2]"/>
812 <xsl:if test="$framewidth > $charlength">
813 <m:mo mathcolor="Green">⇒</m:mo>
814 <xsl:apply-templates select="./*[1]"/>
819 <xsl:if test="$charlength >= $framewidth">
823 <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
824 <m:mo mathcolor="Green">⇒</m:mo>
825 <xsl:apply-templates select="./*[1]"/>
841 <m:mo><</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>></m:mo>
843 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
844 <xsl:apply-templates select="*[position()=3]"/>
845 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
847 <xsl:for-each select="piecewise/piece">
849 <xsl:when test="position() != 1">
850 <m:mo stretchy="false">|</m:mo>
853 <xsl:apply-templates select="./*[2]"/>
854 <m:mo mathcolor="Green">⇒</m:mo>
855 <xsl:apply-templates select="./*[1]"/>
857 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
863 <xsl:when test="$name='fix'">
865 <xsl:when test="$charlength >= $framewidth">
866 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
871 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
872 <m:mi><xsl:value-of select="m:ci"/></m:mi>
873 <m:mo stretchy="false">{</m:mo>
880 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
881 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
882 <xsl:for-each select="m:bvar">
883 <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
887 <m:mi><xsl:value-of select="m:ci"/></m:mi>
889 <xsl:if test="$framewidth > $charlength">
890 <xsl:apply-templates select="m:type"/>
895 <xsl:if test="$charlength >= $framewidth">
899 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
900 <xsl:apply-templates select="m:type"/>
909 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
921 <m:mo stretchy="false">}</m:mo>
929 <m:mi><xsl:value-of select="m:ci"/></m:mi>
930 <m:mo stretchy="false">{</m:mo>
931 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
932 <xsl:for-each select="m:bvar">
936 <m:mi><xsl:value-of select="m:ci"/></m:mi>
938 <xsl:apply-templates select="m:type"/>
940 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
941 <xsl:if test="position()=last()">
942 <m:mo stretchy="false">}</m:mo>
953 <xsl:when test="$name='cofix'">
955 <xsl:when test="$charlength >= $framewidth">
956 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
961 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
962 <m:mi><xsl:value-of select="m:ci"/></m:mi>
963 <m:mo stretchy="false">{</m:mo>
970 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
971 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
972 <xsl:for-each select="m:bvar">
973 <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
977 <m:mi><xsl:value-of select="m:ci"/></m:mi>
979 <xsl:if test="$framewidth > $charlength">
980 <xsl:apply-templates select="m:type"/>
985 <xsl:if test="$charlength >= $framewidth">
989 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
990 <xsl:apply-templates select="m:type"/>
999 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1011 <m:mo stretchy="false">}</m:mo>
1019 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1020 <m:mo stretchy="false">{</m:mo>
1021 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1022 <xsl:for-each select="m:bvar">
1026 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1028 <xsl:apply-templates select="m:type"/>
1030 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1031 <xsl:if test="position()=last()">
1032 <m:mo stretchy="false">}</m:mo>
1042 <!-- ***************************************** -->
1043 <!-- *********** PROOF ELEMENTS ************** -->
1044 <!-- ***************************************** -->
1046 <xsl:when test="$name='proof'">
1047 <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
1048 <xsl:variable name="test" select="(not($explodeall)) and
1049 (not(preceding-sibling::*[1]/text()='letin1')) and
1050 (not(preceding-sibling::*[1]/text()='rw_step')) and
1051 (not(name(..)='m:lambda'))"/>
1052 <xsl:variable name="hidden_details">
1053 <xsl:if test="$test">
1054 <!-- Details hided (default) -->
1055 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1059 <m:mtext mathcolor="Red">We can prove</m:mtext>
1060 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1061 <xsl:apply-templates select="*[position()=3]"/>
1063 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1064 <m:mtext mathcolor="Green">(explain)</m:mtext>
1072 <xsl:variable name="shown_details">
1073 <!-- Show details -->
1074 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1078 <xsl:apply-templates select="*[position()=2]"/>
1085 <m:mtext mathcolor="Red">we proved</m:mtext>
1086 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1087 <xsl:apply-templates select="*[position()=3]"/>
1090 <m:mtext>_</m:mtext>
1092 <xsl:if test="$test">
1093 <m:mtext mathcolor="Green">(hide details)</m:mtext>
1102 <xsl:when test="$test">
1103 <m:maction actiontype="toggle">
1104 <xsl:copy-of select="$hidden_details"/>
1105 <xsl:copy-of select="$shown_details"/>
1109 <xsl:copy-of select="$shown_details"/>
1114 <xsl:when test="$name='side_proof'">
1115 <xsl:variable name="test" select="(not($explodeall))"/>
1116 <xsl:variable name="hidden_details">
1117 <xsl:if test="$test">
1118 <!-- Details hided (default) -->
1119 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1123 <m:mtext mathcolor="Red">We can prove</m:mtext>
1124 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1125 <xsl:apply-templates select="*[position()=3]"/>
1127 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1128 <m:mtext mathcolor="Green">(explain)</m:mtext>
1136 <xsl:variable name="shown_details">
1137 <!-- Show details -->
1138 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1142 <xsl:apply-templates select="*[position()=2]"/>
1149 <m:mtext mathcolor="Red">we proved</m:mtext>
1150 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1151 <xsl:apply-templates select="*[position()=3]"/>
1154 <m:mtext>_</m:mtext>
1156 <xsl:if test="$test">
1157 <m:mtext mathcolor="Green">(hide details)</m:mtext>
1166 <xsl:when test="$test">
1167 <m:maction actiontype="toggle">
1168 <xsl:copy-of select="$hidden_details"/>
1169 <xsl:copy-of select="$shown_details"/>
1173 <xsl:copy-of select="$shown_details"/>
1178 <xsl:when test="$name='letin1'">
1179 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1183 <xsl:apply-templates select="*[position()=2]"/>
1190 <xsl:apply-templates select="*[position()=3]"/>
1196 <xsl:when test="$name='by_induction'">
1197 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1201 <m:mtext mathcolor="Red">We prove</m:mtext>
1202 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1203 <xsl:apply-templates select="../*[3]"/>
1210 <m:mtext mathcolor="Red">by induction on</m:mtext>
1211 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1212 <xsl:apply-templates
1213 select="*[position()=last()]/*[position()=last()]"/>
1220 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1221 <xsl:for-each select="*[position()>3 and not(position()=last())]">
1225 <xsl:apply-templates select="."/>
1236 <!-- inductive_case -->
1237 <xsl:when test="$name='inductive_case'">
1238 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1242 <m:mtext mathcolor="Red">Case</m:mtext>
1243 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1244 <xsl:apply-templates select="*[2]"/>
1251 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1252 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1253 <xsl:if test="*[3]/*[position()>1]">
1257 <m:mtext mathcolor="Red">By induction hypothesis, we have:</m:mtext>
1264 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1265 <xsl:for-each select="*[3]/*[position()>1]">
1266 <m:mo stretchy="false">(</m:mo>
1267 <xsl:apply-templates select="m:ci"/>
1268 <m:mo stretchy="false">) </m:mo>
1269 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1270 <xsl:apply-templates select="m:type"/>
1279 <xsl:apply-templates select="*[4]"/>
1290 <xsl:when test="$name='case_lhs'">
1293 <xsl:when test="count(*)=2">
1294 <xsl:apply-templates select="*[2]"/>
1297 <m:mo stretchy="false">(</m:mo>
1298 <xsl:apply-templates select="*[2]"/>
1299 <xsl:for-each select="m:bvar">
1300 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1301 <xsl:apply-templates select="*[1]"/>
1302 <m:mtext>:</m:mtext>
1303 <xsl:apply-templates select="m:type/*[1]"/>
1305 <m:mo stretchy="false">)</m:mo>
1311 <xsl:when test="$name='false_ind'">
1312 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1316 <xsl:apply-templates select="*[3]"/>
1323 <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1330 <xsl:when test="$name='letin'">
1331 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1332 <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1333 <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1337 <xsl:apply-templates select="."/>
1345 <xsl:apply-templates select="*[position()=last()]"/>
1352 <xsl:when test="$name='let'">
1353 <m:mtext>(</m:mtext>
1354 <xsl:apply-templates select="m:ci"/>
1355 <m:mtext>) </m:mtext>
1356 <xsl:apply-templates select="*[3]"/>
1359 <xsl:when test="$name='rw_step'">
1360 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1365 <xsl:when test="name(*[2])='m:apply'">
1366 <xsl:apply-templates select="*[2]"/>
1369 <m:mtext>Consider</m:mtext>
1370 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1371 <xsl:apply-templates select="*[2]"/>
1380 <m:mtext>Rewrite</m:mtext>
1381 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1382 <xsl:apply-templates select="*[3]"/>
1383 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1384 <m:mtext>with</m:mtext>
1385 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1386 <xsl:apply-templates select="*[4]"/>
1387 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1388 <m:mtext>by</m:mtext>
1389 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1390 <xsl:apply-templates select="*[5]"/>
1396 <!-- not existing any more
1397 <xsl:when test="$name='thread'">
1398 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1403 <xsl:when test="name(*[last()])='m:apply'">
1404 <xsl:apply-templates select="*[last()]"/>
1407 <m:mtext>Consider</m:mtext>
1408 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1409 <xsl:apply-templates select="*[last()]"/>
1415 <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1419 <!-- REWRITE_AND_APPLY -->
1420 <xsl:when test="$name='rewrite_and_apply'">
1421 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1425 <xsl:apply-templates select="*[2]"/>
1432 <m:mtext>Then apply it to</m:mtext>
1433 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1434 <xsl:apply-templates select="*[position()>2]"/>
1441 <xsl:when test="$name='and_ind'">
1442 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1447 <xsl:when test="name(*[2])='m:apply'">
1448 <xsl:apply-templates select="*[2]"/>
1451 <m:mtext>Consider</m:mtext>
1452 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1453 <xsl:apply-templates select="*[2]"/>
1462 <m:mtext>In particular, we have</m:mtext>
1469 <m:mtext>(</m:mtext>
1470 <xsl:apply-templates select="*[3]"/>
1471 <m:mtext>)</m:mtext>
1472 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1473 <xsl:apply-templates select="*[4]"/>
1480 <m:mtext>(</m:mtext>
1481 <xsl:apply-templates select="*[5]"/>
1482 <m:mtext>)</m:mtext>
1483 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1484 <xsl:apply-templates select="*[6]"/>
1491 <xsl:apply-templates select="*[7]"/>
1497 <!-- full_or_ind -->
1498 <xsl:when test="$name='full_or_ind'">
1499 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1504 <xsl:when test="name(*[2])='m:apply'">
1505 <xsl:apply-templates select="*[2]"/>
1508 <m:mtext>Consider</m:mtext>
1509 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1510 <xsl:apply-templates select="*[2]"/>
1519 <m:mtext>We proceed by cases to prove</m:mtext>
1520 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1521 <xsl:apply-templates select="*[3]"/>
1528 <m:mtext>Left: suppose</m:mtext>
1529 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1530 <m:mo stretchy="false">(</m:mo>
1531 <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1532 <m:mo stretchy="false">)</m:mo>
1533 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1534 <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1541 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1542 <xsl:apply-templates select="*[4]/*[3]"/>
1549 <m:mtext>Right: suppose</m:mtext>
1550 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1551 <m:mo stretchy="false">(</m:mo>
1552 <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1553 <m:mo stretchy="false">)</m:mo>
1554 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1555 <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1562 <xsl:apply-templates select="*[5]/*[3]"/>
1569 <xsl:when test="$name='or_ind'">
1570 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1575 <xsl:when test="name(*[2])='m:apply'">
1576 <xsl:apply-templates select="*[2]"/>
1579 <m:mtext>Consider</m:mtext>
1580 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1581 <xsl:apply-templates select="*[2]"/>
1590 <m:mtext>We prove</m:mtext>
1591 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1592 <xsl:apply-templates select="*[3]"/>
1593 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1594 <m:mtext>by cases:</m:mtext>
1601 <m:mtext>Left</m:mtext>
1602 <xsl:apply-templates select="*[4]"/>
1609 <m:mtext>Right</m:mtext>
1610 <xsl:apply-templates select="*[5]"/>
1617 <xsl:when test="$name='ex_ind'">
1618 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1623 <xsl:when test="name(*[2])='m:apply'">
1624 <xsl:apply-templates select="*[2]"/>
1627 <m:mtext>Consider</m:mtext>
1628 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1629 <xsl:apply-templates select="*[2]"/>
1638 <m:mtext>Let</m:mtext>
1639 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1640 <xsl:apply-templates select="*[3]"/>
1641 <m:mtext>:</m:mtext>
1642 <xsl:apply-templates select="*[4]"/>
1643 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1644 <m:mtext>such that</m:mtext>
1645 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1646 <m:mtext>(</m:mtext>
1647 <xsl:apply-templates select="*[5]"/>
1648 <m:mtext>)</m:mtext>
1649 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1650 <xsl:apply-templates select="*[6]"/>
1657 <xsl:apply-templates select="*[7]"/>
1664 <xsl:when test="$name='eq_chain'">
1665 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1669 <m:mtext mathcolor="Red">We have the following equality chain:</m:mtext>
1673 <xsl:for-each select="*[position() mod 2 = 0]">
1674 <xsl:variable name="pos" select="position()"/>
1679 <xsl:when test="$pos = 1">
1680 <xsl:apply-templates select="."/>
1681 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1686 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1687 <xsl:apply-templates select="."/>
1693 <xsl:if test="$pos != last()">
1697 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1698 <xsl:apply-templates select="../*[position()=2*$pos +1]"/>
1706 <!-- DISEQ_CHAIN -->
1707 <xsl:when test="$name='diseq_chain'">
1708 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1712 <m:mtext mathcolor="Red">We have the following disequality chain:</m:mtext>
1716 <xsl:for-each select="*[position() mod 3 = 2]">
1717 <xsl:variable name="pos" select="position()"/>
1722 <xsl:when test="$pos = 1">
1723 <xsl:apply-templates select="."/>
1724 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1725 <mo><xsl:apply-templates select="../*[position()=3*$pos]"/></mo>
1728 <mo><xsl:apply-templates select="../*[position()=3*($pos - 1)]"/></mo>
1729 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1730 <xsl:apply-templates select="."/>
1736 <xsl:if test="$pos != last()">
1740 <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1741 <xsl:apply-templates select="../*[position()=3*$pos +1]"/>
1749 <!-- ***************************************** -->
1750 <!-- *********** NOTATIONS ******************* -->
1751 <!-- ***************************************** -->
1753 <xsl:when test="$name='subst'">
1754 <xsl:apply-templates select="*[3]"/>
1755 <!-- no font for ApplyFunction: <m:mo></m:mo> -->
1756 <m:mo stretchy="false">[</m:mo>
1757 <xsl:apply-templates select="*[4]"/>
1758 <m:mo mathcolor="Green">
1759 <xsl:if test="$id != ''">
1760 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1761 </xsl:if>←</m:mo>
1762 <xsl:apply-templates select="*[2]"/>
1763 <m:mo stretchy="false">]</m:mo>
1766 <xsl:when test="$name='lift'">
1768 <m:mo mathcolor="Green">
1769 <xsl:if test="$id != ''">
1770 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1771 </xsl:if>↑</m:mo>
1772 <xsl:apply-templates select="*[2]"/>
1775 <m:mo stretchy="false">(</m:mo>
1776 <xsl:apply-templates select="*[3]"/>
1777 <m:mo stretchy="false">)</m:mo>
1780 <!-- lift_with_base -->
1781 <xsl:when test="$name='lift_with_base'">
1783 <m:mo mathcolor="Green">
1784 <xsl:if test="$id != ''">
1785 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1786 </xsl:if>↑</m:mo>
1787 <xsl:apply-templates select="*[3]"/>
1788 <xsl:apply-templates select="*[4]"/>
1791 <m:mo stretchy="false">(</m:mo>
1792 <xsl:apply-templates select="*[2]"/>
1793 <m:mo stretchy="false">)</m:mo>
1797 <xsl:when test="$name='beta_red1'">
1798 <xsl:apply-templates select="*[2]"/>
1800 <m:mo mathcolor="Green">
1801 <xsl:if test="$id != ''">
1802 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1803 </xsl:if>→</m:mo>
1804 <m:mi mathcolor="Green">β</m:mi>
1806 <xsl:apply-templates select="*[3]"/>
1809 <xsl:when test="$name='beta_red'">
1810 <xsl:apply-templates select="*[2]"/>
1812 <m:mo mathcolor="Green">
1813 <xsl:if test="$id != ''">
1814 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1815 </xsl:if>→</m:mo>
1816 <m:mi mathcolor="Green">β</m:mi>
1817 <m:mi mathcolor="Green">*</m:mi>
1819 <xsl:apply-templates select="*[3]"/>
1821 <!-- par_beta_red1 -->
1822 <xsl:when test="$name='par_beta_red1'">
1823 <xsl:apply-templates select="*[2]"/>
1825 <m:mo mathcolor="Green">
1826 <xsl:if test="$id != ''">
1827 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1828 </xsl:if>⇒</m:mo>
1829 <m:mi mathcolor="Green">β</m:mi>
1831 <xsl:apply-templates select="*[3]"/>
1833 <!-- par_beta_red -->
1834 <xsl:when test="$name='par_beta_red'">
1835 <xsl:apply-templates select="*[2]"/>
1837 <m:mo mathcolor="Green">
1838 <xsl:if test="$id != ''">
1839 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1840 </xsl:if>⇒</m:mo>
1841 <m:mi mathcolor="Green">β</m:mi>
1842 <m:mi mathcolor="Green">*</m:mi>
1844 <xsl:apply-templates select="*[3]"/>
1847 <xsl:when test="$name='forgetful'">
1848 <m:mfenced open="|" close="|">
1849 <xsl:if test="$id != ''">
1850 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1852 <xsl:apply-templates select="*[2]"/>
1856 <xsl:when test="$name='isomorphic'">
1857 <xsl:apply-templates select="*[2]"/>
1858 <m:mo mathcolor="Green">
1859 <xsl:if test="$id != ''">
1860 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1861 </xsl:if>≅</m:mo>
1862 <xsl:apply-templates select="*[3]"/>
1865 <xsl:when test="$name='forgetful'">
1866 <m:mfenced open="[" close="]">
1867 <xsl:if test="$id != ''">
1868 <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1870 <xsl:apply-templates select="*[2]"/>
1882 <!-- Il modo Thread non esiste piu'
1883 <xsl:template match="*" mode="thread">
1884 <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1886 <xsl:when test="$name='rw_step'">
1890 <m:mtext>Rewrite</m:mtext>
1891 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1892 <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1893 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1894 <m:mtext>with</m:mtext>
1895 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1896 <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1897 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1898 <m:mtext>by</m:mtext>
1899 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1900 <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1907 <m:mtext mathcolor="Red">we get</m:mtext>
1908 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1909 <xsl:apply-templates select="."/>
1918 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1925 <m:mtext mathcolor="Red">we get</m:mtext>
1926 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1927 <xsl:apply-templates select="."/>
1933 <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1939 <xsl:template match="m:lambda">
1940 <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1943 <xsl:attribute name="xref">
1944 <xsl:value-of select="@id"/>
1948 <xsl:when test="$charlength >= $framewidth">
1949 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1953 <m:mo mathcolor="Red">λ</m:mo>
1954 <xsl:apply-templates select="m:bvar"/>
1962 <xsl:apply-templates select="*[position()=2]"/>
1969 <m:mo mathcolor="Red">λ</m:mo>
1970 <xsl:apply-templates select="m:bvar/m:ci"/>
1972 <xsl:apply-templates select="m:bvar/m:type"/>
1974 <xsl:apply-templates select="*[position()=2]"/>
1981 <!--**********************-->
1983 <!--**********************-->
1985 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1986 |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1987 |m:plus|m:minus|m:times" mode="charcount">
1988 <xsl:param name="incurrent_length" select="0"/>
1990 <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1991 <xsl:variable name="siblength">
1992 <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1993 <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1994 </xsl:apply-templates>
1997 <xsl:when test="string($siblength) = """>
1998 <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2001 <xsl:value-of select="number($siblength)"/>
2006 <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2011 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2012 <xsl:param name="incurrent_length" select="0"/>
2013 <xsl:param name="nosibling" select="0"/>
2015 <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2016 <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>
2018 <xsl:when test="string($siblength) = """>
2019 <xsl:value-of select="$incurrent_length + string-length()"/>
2022 <xsl:value-of select="number($siblength)"/>
2027 <xsl:value-of select="$incurrent_length + string-length()"/>
2032 <xsl:template match="*" mode="charcount">
2033 <xsl:param name="incurrent_length" select="0"/>
2034 <xsl:param name="nosibling" select="0"/>
2036 <xsl:when test="count(child::*) = 0">
2037 <xsl:value-of select="$incurrent_length"/>
2040 <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>
2042 <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
2043 <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>
2045 <xsl:when test="string($siblength) = """>
2046 <xsl:value-of select="number($childlength)"/>
2049 <xsl:value-of select="number($siblength)"/>
2054 <xsl:value-of select="number($childlength)"/>