X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fstyle%2Fmmlextension.xsl;h=b9cd3165ef2bc2e4d1e98ed03d4fb4ce686950a6;hb=d1d5f6ee41209f05c072ba20e3cd50bc774ebff4;hp=698e8fce5f9a427cd5d22033960e8370e32447e6;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 698e8fce5..b9cd3165e 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1,5 +1,29 @@
 <?xml version="1.0"?>
 
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
 <!--***********************************************************************--> 
 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
@@ -8,11 +32,21 @@
 <!-- Revised: March 21 2000, Irene Schena                                  -->
 <!--***********************************************************************--> 
 
+<!-- NOTE: the namespace declaration has to be done in the stylesheets 
+which generates the toplevel element (see for instance xlink) -->
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
-                              xmlns:helm="http://www.cs.unibo.it/helm">
+                              xmlns:helm="http://www.cs.unibo.it/helm"
+                              xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
+
+<xsl:import href="mmlnotation.xsl"/>
+
+<xsl:import href="mmltheoryextension.xsl"/>
 
-<xsl:import href="mml2mmlv1_0.xsl"/>
+
+<xsl:param name="explodeall" select="false()"/>
 
 <!--***********************************************************************-->
 <!-- Parameter affecting line-breaking                                     -->
@@ -32,9 +66,19 @@
 <!--        OBJECTS       -->
 <!--**********************-->
 
+<xsl:param name="type" select="'standalone'"/>
+
 <xsl:template match="/">
- <xsl:processing-instruction name="cocoon-format">type="text/xhtml"</xsl:processing-instruction>
- <xsl:apply-templates select="*"/>
+ <xsl:choose>
+  <xsl:when test="$type = 'standalone'">
+   <xsl:apply-templates select="*"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <to_be_embedded>
+    <xsl:apply-templates select="*"/>
+   </to_be_embedded>
+  </xsl:otherwise> 
+ </xsl:choose>
 </xsl:template>
 
 <!-- DEFINITION -->
@@ -295,6 +339,23 @@
         </m:mrow>
        </m:mtd>
       </m:mtr>
+      <xsl:if test="name(*[1])='body'">
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mtext>AS</m:mtext>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+          <xsl:apply-templates select="body/*[1]"/>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+      </xsl:if>
      </m:mtable>
     </m:math>
 </xsl:template>
@@ -314,21 +375,27 @@
      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
       <m:mtr>
        <m:mtd>
-        <xsl:apply-templates select="m:ci"/>
-        <m:mo>:</m:mo>
+        <m:mrow>
+         <xsl:apply-templates select="m:ci"/>
+         <m:mo>:</m:mo>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
       <m:mtr>
        <m:mtd>
+        <m:mrow>
          <xsl:apply-templates select="m:type"/>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
      </m:mtable>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:apply-templates select="m:ci"/>
-     <m:mo>:</m:mo>
-     <xsl:apply-templates select="m:type"/>
+     <m:mrow>
+      <xsl:apply-templates select="m:ci"/>
+      <m:mo>:</m:mo>
+      <xsl:apply-templates select="m:type"/>
+     </m:mrow>
     </xsl:otherwise>
    </xsl:choose>
   </xsl:when>
@@ -342,21 +409,26 @@
 <!-- CSYMBOL -->
 
 <xsl:template match="m:apply[m:csymbol]">
+<xsl:param name="nopar" select="0"/>
     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
     <m:mrow>
-     <xsl:if test="@helm:xref">
-      <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
+     <xsl:if test="@id">
+      <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
      </xsl:if>
+     <xsl:variable name="id" select="m:csymbol/@id"/>
      <xsl:choose>
+      <!-- FORALL -->
       <xsl:when test="$name='forall'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+           <m:mrow>
+            <m:mo mathcolor="Blue">&#8704;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -370,7 +442,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+        <m:mo mathcolor="Blue">&#8704;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -379,14 +451,63 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <!-- LET-IN -->
+      <xsl:when test="$name='let_in'">
+       <xsl:choose>
+       <xsl:when test="$charlength >= $framewidth">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>LET</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>=</m:mo>
+            <xsl:apply-templates select="*[position()=3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>IN</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[position()=4]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:mo>LET</m:mo>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="m:bvar/m:ci"/>
+        <m:mo>=</m:mo>
+        <xsl:apply-templates select="*[position()=3]"/>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <m:mtext>IN</m:mtext>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="*[position()=4]"/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when> 
+      <!-- PROD -->
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue">&#x03a0;</m:mo>
+           <m:mrow>
+            <m:mo mathcolor="Blue">&#x03a0;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -400,7 +521,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue">&#x03a0;</m:mo>
+        <m:mo mathcolor="Blue">&#x03a0;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -409,6 +530,7 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <!-- ARROW -->
       <xsl:when test="$name='arrow'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -416,7 +538,9 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo stretchy="false">(</m:mo>
+            <xsl:if test="$nopar=0">
+             <m:mo stretchy="false">(</m:mo>
+            </xsl:if>
             <xsl:apply-templates select="*[position()=2]"/>
            </m:mrow>
           </m:mtd>
@@ -424,11 +548,27 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Blue">&#x2192;</m:mo>
-            <xsl:apply-templates select="*[position()=3]"/>
+            <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
+            <xsl:choose>
+            <xsl:when test="*[position()=3]/m:csymbol">
+             <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
+             <xsl:choose>
+             <xsl:when test="$nextp='arrow'">
+              <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
+             </xsl:when>
+             <xsl:otherwise>
+              <xsl:apply-templates select="*[position()=3]"/>
+             </xsl:otherwise>
+             </xsl:choose>
+            </xsl:when>
+            <xsl:otherwise>
+             <xsl:apply-templates select="*[position()=3]"/>
+            </xsl:otherwise>
+            </xsl:choose>
            </m:mrow>
           </m:mtd>
          </m:mtr>
+         <xsl:if test="$nopar=0">
          <m:mtr>
           <m:mtd>
            <m:mrow>
@@ -436,17 +576,38 @@
            </m:mrow>
           </m:mtd>
          </m:mtr>
+         </xsl:if>
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo stretchy="false">(</m:mo>
+        <xsl:if test="$nopar=0">
+         <m:mo stretchy="false">(</m:mo>
+        </xsl:if>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Blue">&#x2192;</m:mo>
-        <xsl:apply-templates select="*[position()=3]"/>
-        <m:mo stretchy="false">)</m:mo>
+        <m:mo mathcolor="Blue">&#x2192;</m:mo>
+        <xsl:choose>
+        <xsl:when test="*[position()=3]/m:csymbol">
+         <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
+         <xsl:choose>
+         <xsl:when test="$nextp='arrow'">
+          <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:apply-templates select="*[position()=3]"/>
+         </xsl:otherwise>
+         </xsl:choose>
+        </xsl:when>
+        <xsl:otherwise>
+         <xsl:apply-templates select="*[position()=3]"/>
+        </xsl:otherwise>
+        </xsl:choose>
+        <xsl:if test="$nopar=0">
+         <m:mo stretchy="false">)</m:mo>
+        </xsl:if>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- APP -->
       <xsl:when test="$name='app'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -455,7 +616,10 @@
           <m:mtd>
            <m:mrow>
             <m:mo stretchy="false">(</m:mo>
-            <xsl:apply-templates select="*[position()=2]"/>
+<!-- added precedence to app = FUNCTION_PREC (99) -->
+            <xsl:apply-templates select="*[position()=2]">
+             <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
+            </xsl:apply-templates>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -464,7 +628,10 @@
           <m:mtd>
            <m:mrow>
             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
-            <xsl:apply-templates select="."/>
+<!-- added precedence to app = FUNCTION_PREC (99) -->
+            <xsl:apply-templates select=".">
+             <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
+            </xsl:apply-templates>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -480,15 +647,22 @@
        </xsl:when>
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
-        <xsl:apply-templates select="*[position()=2]"/>
+<!-- added precedence to app = FUNCTION_PREC (99) -->
+        <xsl:apply-templates select="*[position()=2]">
+         <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
+        </xsl:apply-templates>
         <xsl:for-each select="*[position()>2]">
          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-         <xsl:apply-templates select="."/>
+<!-- added precedence to app = FUNCTION_PREC (99) -->
+         <xsl:apply-templates select=".">
+          <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
+         </xsl:apply-templates>
         </xsl:for-each>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- CAST -->
       <xsl:when test="$name='cast'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -504,7 +678,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Maroon">:></m:mo>
+            <m:mo mathcolor="Maroon">:></m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -521,21 +695,25 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Maroon">:></m:mo>
+        <m:mo mathcolor="Maroon">:></m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- PROP -->
       <xsl:when test="$name='Prop'">
        <m:mo>Prop</m:mo>
       </xsl:when>
+      <!-- SET -->
       <xsl:when test="$name='Set'">
        <m:mo>Set</m:mo>
       </xsl:when>
+      <!-- TYPE -->
       <xsl:when test="$name='Type'">
        <m:mo>Type</m:mo>
       </xsl:when>
+      <!-- MUTCASE -->
       <xsl:when test="$name='mutcase'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -574,8 +752,8 @@
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
-         <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
+         <xsl:for-each select="piecewise/piece">
+         <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
          <m:mtr>
           <m:mtd>
            <m:mrow>
@@ -588,10 +766,10 @@
             </xsl:otherwise>
             </xsl:choose>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="."/>
+            <xsl:apply-templates select="./*[2]"/>
             <xsl:if test="$framewidth > $charlength">
-             <m:mo color="Green">&#x21d2;</m:mo>
-             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+             <m:mo mathcolor="Green">&#x21d2;</m:mo>
+             <xsl:apply-templates select="./*[1]"/>
             </xsl:if>
            </m:mrow>
           </m:mtd>
@@ -601,8 +779,8 @@
           <m:mtd>
            <m:mrow>
             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
-            <m:mo color="Green">&#x21d2;</m:mo>
-            <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+            <m:mo mathcolor="Green">&#x21d2;</m:mo>
+            <xsl:apply-templates select="./*[1]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -624,21 +802,22 @@
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>OF</m:mo>
-        <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+        <xsl:for-each select="piecewise/piece">
          <xsl:choose>
          <xsl:when test="position() != 1">
           <m:mo stretchy="false">|</m:mo>
          </xsl:when> 
          </xsl:choose>
-         <xsl:apply-templates select="."/>
-         <m:mo color="Green">&#x21d2;</m:mo>
-         <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+         <xsl:apply-templates select="./*[2]"/>
+         <m:mo mathcolor="Green">&#x21d2;</m:mo>
+         <xsl:apply-templates select="./*[1]"/>
         </xsl:for-each>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>END</m:mo>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- FIX -->
       <xsl:when test="$name='fix'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -728,6 +907,7 @@
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- COFIX -->
       <xsl:when test="$name='cofix'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -820,7 +1000,140 @@
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
+      <!-- PROOF -->
       <xsl:when test="$name='proof'">
+        <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
+        <xsl:variable name="test" select="(not($explodeall)) and
+	   (not(preceding-sibling::*[1]/text()='letin1')) and
+	   (not(preceding-sibling::*[1]/text()='rw_step')) and
+	   (not(name(..)='m:lambda'))"/>
+        <xsl:variable name="hidden_details">
+         <xsl:if test="$test">
+          <!-- Details hided (default) -->
+          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=3]"/>
+              <m:mrow>
+               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+               <m:mtext mathcolor="Green">(explain)</m:mtext>
+              </m:mrow>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </m:mtable>
+         </xsl:if>
+        </xsl:variable>
+        <xsl:variable name="shown_details">
+         <!-- Show details -->
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[position()=2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <xsl:apply-templates select="*[position()=3]"/>
+             <m:mrow>
+              <m:mphantom>
+               <m:mtext>_</m:mtext>
+              </m:mphantom>
+              <xsl:if test="$test">
+               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+              </xsl:if>
+             </m:mrow>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:variable>
+        <xsl:choose>
+         <xsl:when test="$test">
+          <m:maction actiontype="toggle">
+           <xsl:copy-of select="$hidden_details"/>
+           <xsl:copy-of select="$shown_details"/>
+          </m:maction>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:copy-of select="$shown_details"/>
+         </xsl:otherwise>
+        </xsl:choose>
+      </xsl:when>
+      <!-- SIDE_PROOF -->
+      <xsl:when test="$name='side_proof'">
+        <xsl:variable name="test" select="(not($explodeall))"/>
+        <xsl:variable name="hidden_details">
+         <xsl:if test="$test">
+          <!-- Details hided (default) -->
+          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=3]"/>
+              <m:mrow>
+               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+               <m:mtext mathcolor="Green">(explain)</m:mtext>
+              </m:mrow>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </m:mtable>
+         </xsl:if>
+        </xsl:variable>
+        <xsl:variable name="shown_details">
+         <!-- Show details -->
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[position()=2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <xsl:apply-templates select="*[position()=3]"/>
+             <m:mrow>
+              <m:mphantom>
+               <m:mtext>_</m:mtext>
+              </m:mphantom>
+              <xsl:if test="$test">
+               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+              </xsl:if>
+             </m:mrow>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:variable>
+        <xsl:choose>
+         <xsl:when test="$test">
+          <m:maction actiontype="toggle">
+           <xsl:copy-of select="$hidden_details"/>
+           <xsl:copy-of select="$shown_details"/>
+          </m:maction>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:copy-of select="$shown_details"/>
+         </xsl:otherwise>
+        </xsl:choose>
+      </xsl:when>
+      <!-- LETIN1 -->
+      <xsl:when test="$name='letin1'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
@@ -832,14 +1145,146 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we proved </m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <xsl:when test="$name='by_induction'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">We&#x00a0;prove</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="../*[3]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">by&#x00a0;induction&#x00a0;on</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates 
+            select="*[position()=last()]/*[position()=last()]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+            <xsl:for-each select="*[position()>3 and not(position()=last())]">
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <xsl:apply-templates select="."/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:for-each>
+           </m:mtable>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- inductive_case -->
+      <xsl:when test="$name='inductive_case'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">Case</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[2]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+            <xsl:if test="*[3]/*[position()>1]">
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <m:mtext mathcolor="Red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:for-each select="*[3]/*[position()>1]">
+                 <m:mo stretchy="false">(</m:mo>
+                 <xsl:apply-templates select="m:ci"/>
+                 <m:mo stretchy="false">) </m:mo>
+                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                 <xsl:apply-templates select="m:type"/>
+                </xsl:for-each>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:if>
+            <m:mtr>
+             <m:mtd>
+              <m:mrow>
+               <xsl:apply-templates select="*[4]"/>
+              </m:mrow>
+             </m:mtd>
+            </m:mtr>
+           </m:mtable>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- case_lhs  -->
+      <xsl:when test="$name='case_lhs'">
+       <m:mrow>
+        <xsl:choose>
+         <xsl:when test="count(*)=2">
+          <xsl:apply-templates select="*[2]"/>
+         </xsl:when>
+         <xsl:otherwise>
+          <m:mo stretchy="false">(</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+          <xsl:for-each select="m:bvar">
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[1]"/>
+           <m:mtext>:</m:mtext>
+           <xsl:apply-templates select="m:type/*[1]"/>
+          </xsl:for-each>
+          <m:mo stretchy="false">)</m:mo>
+         </xsl:otherwise>
+        </xsl:choose>
+       </m:mrow>
+      </xsl:when>
+      <!-- false_ind  -->
+      <xsl:when test="$name='false_ind'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <xsl:apply-templates select="*[3]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">Contradiction.</m:mtext>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- LET-IN -->
       <xsl:when test="$name='letin'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
@@ -861,103 +1306,141 @@
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- LET -->
       <xsl:when test="$name='let'">
        <m:mtext>(</m:mtext>
        <xsl:apply-templates select="m:ci"/>
        <m:mtext>) </m:mtext>
        <xsl:apply-templates select="*[3]"/>
       </xsl:when>
-      <xsl:when test="$name='thread'">
+      <!-- RW_STEP -->
+      <xsl:when test="$name='rw_step'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
            <m:mrow>
             <xsl:choose>
-             <xsl:when test="name(*[last()])='m:apply'">
-              <xsl:apply-templates select="*[last()]"/>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
              </xsl:when>
              <xsl:otherwise>
-              <m:mtext>Consider </m:mtext>
-              <xsl:apply-templates select="*[last()]"/>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[2]"/>
              </xsl:otherwise>
             </xsl:choose>
            </m:mrow>
           </m:mtd>
          </m:mtr>
-	 <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
-        </m:mtable>
-      </xsl:when> 
-      <xsl:when test="$name='rewrite_and_apply'">
-        <m:mtable>
          <m:mtr>
           <m:mtd>
            <m:mrow>
             <m:mtext>Rewrite</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[2]/*[2]"/>
+            <xsl:apply-templates select="*[3]"/>
 	    <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 	    <m:mtext>with</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[2]/*[3]"/>
+            <xsl:apply-templates select="*[4]"/>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mtext>by</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[2]/*[4]"/>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>in</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[3]"/>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>and apply to</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[position()>3]"/>
+            <xsl:apply-templates select="*[5]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
-       </m:mtable>
-      </xsl:when> 
-      <xsl:when test="$name='and_ind'">
+        </m:mtable>
+      </xsl:when>
+      <!-- not existing any more
+      <xsl:when test="$name='thread'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
            <m:mrow>
             <xsl:choose>
-             <xsl:when test="name(*[2])='m:apply'">
-              <xsl:apply-templates select="*[2]"/>
+             <xsl:when test="name(*[last()])='m:apply'">
+              <xsl:apply-templates select="*[last()]"/>
              </xsl:when>
              <xsl:otherwise>
-              <m:mtext>Consider </m:mtext>
-              <xsl:apply-templates select="*[2]"/>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[last()]"/>
              </xsl:otherwise>
             </xsl:choose>
            </m:mrow>
           </m:mtd>
          </m:mtr>
+	 <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
+        </m:mtable>
+      </xsl:when>
+      --> 
+      <!-- REWRITE_AND_APPLY -->
+      <xsl:when test="$name='rewrite_and_apply'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-           <m:mtext>In particular, we have</m:mtext>
+           <m:mrow>
+            <xsl:apply-templates select="*[2]"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>(</m:mtext>
-            <xsl:apply-templates select="*[3]"/>
-            <m:mtext>)</m:mtext>
+            <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[4]"/>
-            </m:mrow>
+            <xsl:apply-templates select="*[position()>2]"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- AND_IND -->
+      <xsl:when test="$name='and_ind'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>(</m:mtext>
-            <xsl:apply-templates select="*[5]"/>
-            <m:mtext>)</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[6]"/>
-            </m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>(</m:mtext>
+            <xsl:apply-templates select="*[3]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[4]"/>
+            </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>(</m:mtext>
+            <xsl:apply-templates select="*[5]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[6]"/>
+            </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -969,6 +1452,78 @@
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- full_or_ind -->
+      <xsl:when test="$name='full_or_ind'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>Left:&#x00a0;suppose</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mo stretchy="false">(</m:mo>
+            <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
+            <m:mo stretchy="false">)</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[4]/*[3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>Right:&#x00a0;suppose</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mo stretchy="false">(</m:mo>
+            <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
+            <m:mo stretchy="false">)</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:apply-templates select="*[5]/*[3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+      </xsl:when>
+      <!-- OR_IND -->
       <xsl:when test="$name='or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -989,17 +1544,19 @@
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mtext>We prove</m:mtext>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates select="*[3]"/>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <m:mtext>by cases:</m:mtext>
+           <m:mrow>
+            <m:mtext>We&#x00a0;prove</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>by&#x00a0;cases:</m:mtext>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>*</m:mtext>
+            <m:mtext>Left</m:mtext>
             <xsl:apply-templates select="*[4]"/>
            </m:mrow>
           </m:mtd>
@@ -1007,20 +1564,280 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>*</m:mtext>
+            <m:mtext>Right</m:mtext>
             <xsl:apply-templates select="*[5]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- EX_IND -->
+      <xsl:when test="$name='ex_ind'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>Let</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
+            <m:mtext>:</m:mtext>
+            <xsl:apply-templates select="*[4]"/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>such&#x00a0;that</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>(</m:mtext>
+             <xsl:apply-templates select="*[5]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[6]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:apply-templates select="*[7]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+      </xsl:when>
+      <!-- EQ_CHAIN -->
+      <xsl:when test="$name='eq_chain'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;equality&#x00a0;chain:</m:mtext>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <xsl:for-each select="*[position() mod 2 = 0]">
+        <xsl:variable name="pos" select="position()"/>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <xsl:choose>
+           <xsl:when test="$pos = 1">
+            <xsl:apply-templates select="."/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mo>=</m:mo>
+           </xsl:when>
+           <xsl:otherwise>
+            <m:mo>=</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="."/>
+           </xsl:otherwise>
+           </xsl:choose>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <xsl:if test="$pos != last()">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+           <xsl:apply-templates select="../*[position()=2*$pos +1]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        </xsl:if>
+        </xsl:for-each>
+       </m:mtable>
+      </xsl:when>
+      <!-- DISEQ_CHAIN -->
+      <xsl:when test="$name='diseq_chain'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;disequality&#x00a0;chain:</m:mtext>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <xsl:for-each select="*[position() mod 3 = 2]">
+        <xsl:variable name="pos" select="position()"/>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <xsl:choose>
+           <xsl:when test="$pos = 1">
+            <xsl:apply-templates select="."/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <mo><xsl:apply-templates select="../*[position()=3*$pos]"/></mo>
+           </xsl:when>
+           <xsl:otherwise>
+            <mo><xsl:apply-templates select="../*[position()=3*($pos - 1)]"/></mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="."/>
+           </xsl:otherwise>
+           </xsl:choose>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <xsl:if test="$pos != last()">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+           <xsl:apply-templates select="../*[position()=3*$pos +1]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        </xsl:if>
+        </xsl:for-each>
+       </m:mtable>
+      </xsl:when>
+      <!-- ***************************************** -->
+      <!-- *********** NOTATIONS ******************* -->
+      <!-- ***************************************** -->
+      <!-- subst -->
+      <xsl:when test="$name='subst'">
+        <xsl:apply-templates select="*[3]"/>
+<!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
+        <m:mo stretchy="false">[</m:mo>
+        <xsl:apply-templates select="*[4]"/>
+        <m:mo mathcolor="Green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8592;</m:mo>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">]</m:mo>
+      </xsl:when>
+      <!-- lift -->
+      <xsl:when test="$name='lift'">
+        <m:msup>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[2]"/>
+        </m:msup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[3]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>
+      </xsl:when>
+      <!-- lift_with_base -->
+      <xsl:when test="$name='lift_with_base'">
+        <m:msubsup>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[3]"/>
+	 <xsl:apply-templates select="*[4]"/>
+        </m:msubsup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[2]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>	
+      </xsl:when>
+      <!-- beta_red1 -->
+      <xsl:when test="$name='beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="Green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- beta_red -->
+      <xsl:when test="$name='beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="Green">&#946;</m:mi>
+          <m:mi mathcolor="Green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red1 -->
+      <xsl:when test="$name='par_beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="Green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red -->
+      <xsl:when test="$name='par_beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="Green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="Green">&#946;</m:mi>
+          <m:mi mathcolor="Green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- forgetful -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="|" close="|">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when>
+      <!-- isomorphic -->
+      <xsl:when test="$name='isomorphic'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo mathcolor="Green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8773;</m:mo>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- interp -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="[" close="]">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when> 
+
+      <!-- ERROR -->
       <xsl:otherwise>
-       <m:ci>ERROR</m:ci>
+       <m:mi>ERROR</m:mi>
       </xsl:otherwise>
      </xsl:choose>
     </m:mrow>
 </xsl:template>
 
+<!-- Il modo Thread non esiste piu' 
 <xsl:template match="*" mode="thread">
  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
  <xsl:choose>
@@ -1045,7 +1862,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1063,7 +1880,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1073,20 +1890,27 @@
    </xsl:choose>
          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
 </xsl:template>
-
+-->
 
 <!-- LAMBDA -->
 
 <xsl:template match="m:lambda">
     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
-    <m:mrow helm:xref="{@helm:xref}">
+    <m:mrow>
+     <xsl:if test="@id">
+      <xsl:attribute name="xref">
+       <xsl:value-of select="@id"/>
+      </xsl:attribute>
+     </xsl:if>
      <xsl:choose>
      <xsl:when test="$charlength >= $framewidth">
       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
           <m:mtd>
-            <m:mo color="Red">&#x03bb;</m:mo>
+           <m:mrow>
+            <m:mo mathcolor="Red">&#x03bb;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
        <m:mtr>
@@ -1100,7 +1924,7 @@
       </m:mtable>
      </xsl:when>
      <xsl:otherwise>
-      <m:mo color="Red">&#x03bb;</m:mo>
+      <m:mo mathcolor="Red">&#x03bb;</m:mo>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <m:mo>:</m:mo>
       <xsl:apply-templates select="m:bvar/m:type"/>
@@ -1111,229 +1935,6 @@
     </m:mrow>
 </xsl:template>
 
-<!-- *********************************** -->
-<!-- BASE SET OF MATHML CONTENT ELEMENTS -->
-<!-- *********************************** -->
-
-<!-- Logic -->
-
-<xsl:template match = "m:apply[m:eq[1]]">
- <xsl:variable name="charlength">
-  <xsl:apply-templates select="*[1]" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
-  <xsl:when test="$charlength >= $framewidth">
-   <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
-     <xsl:attribute name="helm:xref">
-      <xsl:value-of select="@helm:xref"/>
-     </xsl:attribute>
-    </xsl:if>    
-    <m:mtr>
-     <m:mtd>
-      <m:mo stretchy="false">(</m:mo>
-      <xsl:apply-templates select="*[position()=2]"/>
-     </m:mtd>
-    </m:mtr>
-    <xsl:for-each select = "*[position()>2]">
-     <m:mtr>
-      <m:mtd>
-       <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="m:in/@helm:xref"> 
-        =
-       </m:mo>
-       <xsl:apply-templates select="."/>
-      </m:mtd>
-     </m:mtr>
-    </xsl:for-each>
-    <m:mtr>
-     <m:mtd>
-      <m:mo stretchy="false">)</m:mo>
-     </m:mtd>
-    </m:mtr>
-   </m:mtable>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:apply-imports/>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-
-<xsl:template match = "m:apply[m:and[1]|m:or[1]
-          |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
-          |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
-          |m:prsubset|m:setdiff[1]]">
- <xsl:variable name="symbol">
-  <xsl:choose>
-   <xsl:when test="m:and[1]">
-    <xsl:value-of select="'wedge'"/>
-   </xsl:when>
-   <xsl:when test="m:or[1]">
-    <xsl:value-of select="'vee'"/>
-   </xsl:when>
-   <xsl:when test="m:geq[1]">
-    <xsl:value-of select="'geq'"/>
-   </xsl:when>
-   <xsl:when test="m:leq[1]">
-    <xsl:value-of select="'leq'"/>
-   </xsl:when>
-   <xsl:when test="m:gt[1]">
-    <xsl:value-of select="'gt'"/>
-   </xsl:when>
-   <xsl:when test="m:lt[1]">
-    <xsl:value-of select="'lt'"/>
-   </xsl:when>
-   <xsl:when test="m:eq[1]">
-    <xsl:value-of select="'Equal'"/>
-   </xsl:when>
-   <xsl:when test="m:in[1]">
-    <xsl:value-of select="'Element'"/>
-   </xsl:when>
-   <xsl:when test="m:subset[1]">
-    <xsl:value-of select="'SubsetEqual'"/>
-   </xsl:when>
-   <xsl:when test="m:prsubset[1]">
-    <xsl:value-of select="'subset'"/>
-   </xsl:when>
-   <xsl:when test="m:intersect[1]">
-    <xsl:value-of select="'Intersection'"/>
-   </xsl:when>
-   <xsl:when test="m:union[1]">
-    <xsl:value-of select="'Union'"/>
-   </xsl:when>
-   <xsl:when test="m:setdiff[1]">
-    <xsl:value-of select="'Backslash'"/>
-   </xsl:when>
-  </xsl:choose>
- </xsl:variable>
- <xsl:variable name="charlength">
-  <xsl:apply-templates select="*[1]" mode="charcount"/>
- </xsl:variable>
- <xsl:choose>
-  <xsl:when test="$charlength >= $framewidth">
-   <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
-     <xsl:attribute name="helm:xref">
-      <xsl:value-of select="@helm:xref"/>
-     </xsl:attribute>
-    </xsl:if>    
-    <m:mtr>
-     <m:mtd>
-      <m:mo stretchy="false">(</m:mo>
-      <xsl:apply-templates select="*[position()=2]"/>
-     </m:mtd>
-    </m:mtr>
-    <xsl:for-each select = "*[position()>2]">
-     <m:mtr>
-      <m:mtd>
-       <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="{*[1]/@helm:xref}"> 
-        <m:mchar name="{$symbol}"/>
-       </m:mo>
-       <xsl:apply-templates select="."/>
-      </m:mtd>
-     </m:mtr>
-    </xsl:for-each>
-    <m:mtr>
-     <m:mtd>
-      <m:mo stretchy="false">)</m:mo>
-     </m:mtd>
-    </m:mtr>
-   </m:mtable>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:apply-imports/>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template match = "m:set">
- <xsl:choose>
-  <xsl:when test="count(child::*) = 0">
-   <m:mi> 
-    <m:mchar name="emptyset"/>
-   </m:mi>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:variable name="charlength">
-    <xsl:apply-templates select="*[1]" mode="charcount"/>
-   </xsl:variable>
-   <xsl:choose>
-    <xsl:when test="$charlength >= $framewidth">
-     <xsl:choose>
-      <xsl:when test="name(*[1]) = 'm:bvar'">
-       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-        <m:mtr>
-         <m:mtd>
-          <m:mo stretchy="false">{</m:mo>
-          <xsl:apply-templates select="*[position()=1]"/>
-         </m:mtd>
-        </m:mtr>
-        <m:mtr>
-         <m:mtd>
-          <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
-          <m:mo stretchy="false">|</m:mo>
-          <xsl:apply-templates select="m:condition/*[1]"/>
-         </m:mtd>
-        </m:mtr>
-        <m:mtr>
-         <m:mtd>
-          <m:mo stretchy="false">}</m:mo>
-         </m:mtd>
-        </m:mtr>
-       </m:mtable>
-      </xsl:when>
-      <xsl:otherwise>
-       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-        <m:mtr>
-         <m:mtd>
-          <m:mo stretchy="false">{</m:mo>
-          <xsl:apply-templates select="*[position()=1]"/>
-          <xsl:if test="position() != last()">
-           <mo>,</mo>
-          </xsl:if>
-         </m:mtd>
-        </m:mtr>
-        <xsl:for-each select = "*[position()>2]">
-         <m:mtr>
-          <m:mtd>
-           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
-           <xsl:apply-templates select="."/>
-           <xsl:if test="position() != last()">
-            <mo>,</mo>
-           </xsl:if>
-          </m:mtd>
-         </m:mtr>
-        </xsl:for-each>
-        <m:mtr>
-         <m:mtd>
-          <m:mo stretchy="false">}</m:mo>
-         </m:mtd>
-        </m:mtr>
-       </m:mtable>
-      </xsl:otherwise>
-     </xsl:choose>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:apply-imports/>
-    </xsl:otherwise>
-   </xsl:choose>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>      
-
-<xsl:template match = "m:apply[m:card[1]]">
- <m:mo stretchy="false">|</m:mo>
-  <xsl:apply-templates select="*[2]"/>
- <m:mo stretchy="false">|</m:mo>
-</xsl:template>
-
-<!-- *********************************** -->
-<!--          PROOF ELEMENTS             -->
-<!-- *********************************** -->
-
-
 
 <!--**********************-->
 <!--       COUNTING       -->
@@ -1405,7 +2006,7 @@
      <xsl:otherwise>
       <xsl:value-of select="number($siblength)"/>
      </xsl:otherwise>
-     </xsl:choose>>
+     </xsl:choose>
     </xsl:when>
     <xsl:otherwise>
      <xsl:value-of select="number($childlength)"/>