From 3aa2fd56797217a73b59e25bbe961dbc8c08bb2f Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 5 Nov 2001 09:06:40 +0000
Subject: [PATCH] Algebra notation.

---
 helm/style/algebra.xsl         | 453 +++++++++++++++++++++++++++++++++
 helm/style/content_to_html.xsl |  88 ++++++-
 helm/style/drop_coercions.xsl  |  35 +++
 helm/style/headercontent.xsl   |   1 +
 helm/style/html_init.xsl       |  26 +-
 helm/style/html_reals.xsl      |  65 ++++-
 helm/style/proofs.xsl          |  64 ++++-
 helm/style/set.xsl             |  47 ++++
 8 files changed, 771 insertions(+), 8 deletions(-)
 create mode 100644 helm/style/algebra.xsl

diff --git a/helm/style/algebra.xsl b/helm/style/algebra.xsl
new file mode 100644
index 000000000..81eed377a
--- /dev/null
+++ b/helm/style/algebra.xsl
@@ -0,0 +1,453 @@
+<?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/.                                         -->
+
+<!--******************************************************************--> 
+<!-- Algebra                                                          -->
+<!-- First draft: October 2001                                        -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi          -->
+<!--******************************************************************-->
+
+<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">
+
+
+<!-- ************************* ALGEBRA *********************************-->
+
+
+
+<!-- 0 and 1 -->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSemiGroups/csg_unit.con']" mode="pure">
+ <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">0</m:ci>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_one.con']" mode="pure">
+ <m:ci definitionURL="{CONST/@uri}" helm:xref="{@id}">1</m:ci>
+</xsl:template>
+
+<!-- Unary Operations -->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CGroups/cg_inv.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="1"/>
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'minus'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'abs'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<!-- inv (uri errata)
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
+   <xsl:variable name="mbody1">
+      <xsl:apply-templates select="*[2]" mode="noannot"/>
+      <xsl:variable name="mbody2">
+         <m:cn>1</m:cn>
+      </xsl:variable>
+      <xsl:call-template name="out-mml-op">
+         <xsl:with-param name="arity" select="1"/>
+         <xsl:with-param name="c-tag" select="CONST"/>
+         <xsl:with-param name="m-tag" select="'minus'"/>
+         <xsl:with-param name="mbody" select="$mbody2"/>
+      </xsl:call-template>
+   </xsl:variable>
+   <xsl:call-template name="out-mml-op">
+      <xsl:with-param name="arity" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'power'"/>
+      <xsl:with-param name="mbody" select="$mbody1"/>
+   </xsl:call-template>
+</xsl:template>
+-->
+
+<!-- Binary Operations and Relations -->
+
+<!-- setoid equality -->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_eq.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'eq'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<!-- apart -->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CSetoids/cs_ap.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'neq'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/leEq.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'leq'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/cof_less.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'lt'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<!--
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'geq'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'gt'"/>
+   </xsl:call-template>
+</xsl:template>
+-->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_plus.con' or
+CONST/@uri='cic:/Algebra/CSemiGroups/csg_op.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'plus'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_minus.con' or
+ CONST/@uri='cic:/Algebra/CGroups/cg_minus.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'minus'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/cr_mult.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'times'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CFields/cf_div.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'divide'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/Ring_constructions/nzpro.con' and count(*)='4']" mode="pure">
+   <xsl:apply-templates select="*[3]" mode="pure"/>
+</xsl:template>
+
+<!-- 
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'min'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'max'"/>
+   </xsl:call-template>
+</xsl:template>
+-->
+
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp.con']" mode="pure">
+   <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+    </xsl:variable>
+   <xsl:call-template name="mk-mml-op-noannot">
+      <xsl:with-param name="hide" select="$no_params"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'power'"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CRings/exponentiation/nexp_op.con' or CONST/@uri='cic:/Algebra/Expon/Zexp_def/zexp.con']" mode="pure">
+   <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+   </xsl:variable>
+   <xsl:variable name="mbody">
+    <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
+    <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+   </xsl:variable>
+   <xsl:call-template name="out-mml-op">
+      <xsl:with-param name="hide" select="$no_params"/>
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'power'"/>
+      <xsl:with-param name="mbody" select="$mbody"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/COrdFields/absSmall.con']" mode="pure">
+   <xsl:variable name="mbody">
+      <m:apply helm:xref="{@id}">
+       <m:abs definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+       <xsl:apply-templates select="*[4]" mode="noannot"/>
+      </m:apply>
+      <xsl:apply-templates select="*[3]" mode="noannot"/>
+   </xsl:variable>
+   <xsl:call-template name="out-mml-op">
+      <xsl:with-param name="hide" select="1"/>
+      <xsl:with-param name="arity" select="2"/>
+      <xsl:with-param name="c-tag" select="CONST"/>
+      <xsl:with-param name="m-tag" select="'lt'"/>
+      <xsl:with-param name="mbody" select="$mbody"/>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST[
+ attribute::uri='cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con']]" mode="pure">
+    <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+    </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="count(child::*) = 3+$no_params">
+      <m:apply helm:xref="{@id}">
+       <m:eq definitionURL="{CONST/@uri}" helm:xref="{@id}" />
+       <xsl:choose>
+        <xsl:when test="name(*[2+$no_params]) = 'LAMBDA'">
+         <m:apply helm:xref="{CONST/@id}">
+          <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
+          </m:bvar>
+          <m:lowlimit>
+           <m:infinity/>
+          </m:lowlimit>
+          <xsl:apply-templates select="*[2+$no_params]/target/*[1]" mode="noannot"/>
+         </m:apply>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:apply helm:xref="{CONST/@id}">
+          <m:limit definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>$x</m:ci>
+          </m:bvar>
+          <m:lowlimit>
+           <m:infinity/>
+          </m:lowlimit>
+          <m:apply>
+           <m:csymbol>app</m:csymbol>
+           <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
+           <m:ci>$x</m:ci>
+          </m:apply>
+         </m:apply>
+        </xsl:otherwise>
+       </xsl:choose>
+       <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
+      </m:apply>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-imports/>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST[
+ attribute::uri='cic:/Algebra/CSums/Sums/sum0.con']]" mode="pure">
+    <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+    </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="count(child::*) = 3+$no_params">
+       <xsl:choose>
+        <xsl:when test="name(*[3+$no_params]) = 'LAMBDA'">
+         <m:apply helm:xref="{CONST/@id}">
+          <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
+          </m:bvar>
+          <m:condition>
+           <m:apply>
+            <m:lt/>
+            <m:ci>
+             <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
+            </m:ci>
+            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+           </m:apply>
+          </m:condition>
+          <xsl:apply-templates select="*[3+$no_params]/target/*[1]" mode="noannot"/>
+         </m:apply>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:apply helm:xref="{CONST/@id}">
+          <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>$x</m:ci>
+          </m:bvar>
+          <m:condition>
+           <m:apply>
+            <m:lt/>
+            <m:ci>$x</m:ci>
+            <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+           </m:apply>
+          </m:condition>
+          <m:apply>
+           <m:csymbol>app</m:csymbol>
+           <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
+           <m:ci>$x</m:ci>
+          </m:apply>
+         </m:apply>
+        </xsl:otherwise>
+       </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-imports/>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
+<!-- sum -->
+<xsl:template match="APPLY[CONST[
+ attribute::uri='cic:/Algebra/CSums/Sums/sum.con']]" mode="pure">
+    <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+    </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="count(child::*) = 4+$no_params">
+       <xsl:choose>
+        <xsl:when test="name(*[4+$no_params]) = 'LAMBDA'">
+         <m:apply helm:xref="{CONST/@id}">
+          <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
+          </m:bvar>
+          <m:lowlimit>
+           <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+          </m:lowlimit>
+          <m:uplimit>
+           <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
+          </m:uplimit>
+          <xsl:apply-templates select="*[4+$no_params]/target/*[1]" mode="noannot"/>
+         </m:apply>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:apply helm:xref="{CONST/@id}">
+          <m:sum definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
+          <m:bvar>
+           <m:ci>$x</m:ci>
+          </m:bvar>
+          <m:lowlimit>
+           <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+          </m:lowlimit>
+          <m:uplimit>
+           <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
+          </m:uplimit>
+          <m:apply>
+           <m:csymbol>app</m:csymbol>
+           <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
+           <m:ci>$x</m:ci>
+          </m:apply>
+         </m:apply>
+        </xsl:otherwise>
+       </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-imports/>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
+<!-- polynomials -->
+
+<xsl:template match="APPLY[CONST/@uri='cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con']" mode="pure">
+   <xsl:variable name="no_params">
+     <xsl:call-template name="get_no_params">
+      <xsl:with-param name="first_uri" select="$CICURI"/>
+      <xsl:with-param name="second_uri" select="CONST/@uri"/>
+     </xsl:call-template>
+    </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="count(child::*) = 3+$no_params">
+      <m:apply>
+       <m:csymbol>app</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[2+$no_params]"/>
+       <xsl:apply-templates mode="noannot" select="*[3+$no_params]"/>
+      </m:apply>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-imports/>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
+</xsl:stylesheet>
+
+
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 6e7ff7ca5..a9cc91a96 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -59,7 +59,7 @@
 	media-type="text/html"
 	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
 
-<xsl:variable name="framewidth" select="45"/>
+<xsl:variable name="framewidth" select="55"/>
 
 <xsl:template name="mksymbol-1">
  <xsl:param name="symbol" select="''"/>
@@ -408,11 +408,14 @@
      </xsl:for-each>
     </xsl:when>
     <!-- proof -->
-    <xsl:when test="$name='proof'">
+    <xsl:when test="$name='proof' or $name='side_proof'">
        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
     </xsl:when>
+    <xsl:when test="$name='letin1'">
+     <xsl:text>letin1 (inline error)</xsl:text>
+    </xsl:when>
     <!-- false_ind -->
     <xsl:when test="$name='false_ind'">
     <xsl:apply-templates mode="inline" select="*[3]"/>
@@ -1126,6 +1129,87 @@
         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
        </xsl:apply-templates>
       </xsl:when>
+      <!-- side_proof -->
+      <xsl:when test="$name='side_proof'">
+       <xsl:variable name="nonce" select="generate-id()"/>
+       <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
+       <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
+       <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
+       <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
+       <span ID="{$freshid1}">
+        <xsl:apply-templates select="*[position()=2]">
+         <xsl:with-param name="current_indent" select="$current_indent"/>
+        </xsl:apply-templates>
+        &#x00a0;
+       </span>
+         <script>
+          if(document.getElementById) {
+           document.write('\
+            <span ID="{$freshid2}">\
+             <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
+            </span>\
+            <span ID="{$freshid3}">\
+             <br/>\
+             <xsl:call-template name="make_indent">
+              <xsl:with-param name="current_indent" select="$current_indent"/>
+             </xsl:call-template>\
+             <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
+            </span>\
+           ');
+           document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
+           document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
+           document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
+           document.write('&#x00a0;');
+          } else {
+           document.write('\
+            <br/>\
+            <xsl:call-template name="make_indent">
+             <xsl:with-param name="current_indent" select="$current_indent"/>
+            </xsl:call-template>\
+            <FONT color="red">we proved&#x00a0;</FONT>\
+           ');
+          }
+         </script>
+       <span ID="{$freshid4}">
+        <xsl:apply-templates select="*[position()=3]">
+         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
+        </xsl:apply-templates>
+       </span>
+      </xsl:when> 
+      <!-- eq_chain -->
+      <xsl:when test="$name='eq_chain'">
+       <FONT color="red">We have the following equality chain:</FONT>
+       <xsl:for-each select="*[position() mod 2 = 0]">
+        <xsl:variable name="pos" select="position()"/>
+        <br/>
+        <xsl:call-template name="make_indent">
+         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+        </xsl:call-template>
+        <xsl:choose>
+         <xsl:when test="$pos=1">
+          <xsl:apply-templates select=".">
+           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+          </xsl:apply-templates>
+          <xsl:text>&#x00a0;=</xsl:text>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:text>=&#x00a0;</xsl:text>
+          <xsl:apply-templates select=".">
+           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+          </xsl:apply-templates>
+         </xsl:otherwise>
+        </xsl:choose>
+        <xsl:if test="$pos != last()">
+         <br/>
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+         </xsl:call-template>
+         <xsl:apply-templates select="../*[position()=2*$pos +1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+         </xsl:apply-templates>
+        </xsl:if>
+       </xsl:for-each>
+      </xsl:when> 
       <!-- letin1 -->
       <xsl:when test="$name='letin1'">
        <xsl:apply-templates select="*[position()=2]">
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index 9731d6601..f2bc44d0d 100644
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -118,6 +118,41 @@
     </xsl:choose>
 </xsl:template>
 
+<xsl:template match="APPLY[CONST[position()='1' and 
+   @uri='cic:/Algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
+     <xsl:variable name="no_params">
+      <xsl:call-template name="get_no_params">
+       <xsl:with-param name="first_uri" select="$CICURI"/>
+       <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
+      </xsl:call-template>
+     </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="(count(child::*) - number($no_params)) = 4">
+      <xsl:choose>
+       <xsl:when test="name(*[2+$no_params])='APPLY'">
+        <APPLY id="{@id}" sort="{@sort}">
+         <xsl:apply-templates select="*[2+$no_params]/*"/>
+         <xsl:apply-templates select="*[3+$no_params]"/>
+         <xsl:apply-templates select="*[4+$no_params]"/>
+        </APPLY>
+       </xsl:when>
+       <xsl:otherwise>
+        <APPLY id="{@id}" sort="{@sort}">
+         <xsl:apply-templates select="*[2+$no_params]"/>
+         <xsl:apply-templates select="*[3+$no_params]"/>
+         <xsl:apply-templates select="*[4+$no_params]"/>
+        </APPLY>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <APPLY id="{@id}" sort="{@sort}">
+       <xsl:apply-templates select="*"/>
+      </APPLY>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
 
 <xsl:template match = "/|*">
   <xsl:copy>
diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl
index a46023db5..f60883079 100644
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -37,6 +37,7 @@
 <xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>
 <xsl:include href="ring.xsl"/>        <!-- FG -->
+<xsl:include href="algebra.xsl"/> 
 <xsl:include href="lambda.xsl"/>
 
 </xsl:stylesheet>
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 06e23deca..d3c9d1992 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -62,6 +62,9 @@
       </xsl:when>
       <xsl:when test="$symbol = 'times'">
        <xsl:value-of select="'&#42;'"/>
+      </xsl:when> 
+      <xsl:when test="$symbol = 'divide'">
+       <xsl:value-of select="'&#47;'"/>
       </xsl:when>
       <xsl:when test="$symbol = 'minus'">
        <xsl:value-of select="'&#45;'"/>
@@ -114,6 +117,9 @@
       <xsl:when test="$symbol = 'times'">
        <xsl:value-of select="'&#8727;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'divide'">
+       <xsl:value-of select="'&#47;'"/>
+      </xsl:when>
       <xsl:when test="$symbol = 'minus'">
        <xsl:value-of select="'&#8722;'"/>
       </xsl:when>
@@ -143,8 +149,24 @@
 
 <!-- INLINE MODE : BASIC OPERATORS -->
 
+<xsl:template mode="inline" match="m:infinity">
+ <xsl:choose>
+  <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
+   <FONT FACE="symbol" color="'blue'">
+    <xsl:value-of select="'&#165;'"/>
+   </FONT>
+  </xsl:when>
+  <xsl:otherwise>
+   <FONT color="'blue'">
+    <!-- VERIFICARE -->
+    <xsl:value-of select="'&#165;'"/>
+   </FONT>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
  <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
-       |m:geq|m:gt|m:plus|m:times]">
+       |m:geq|m:gt|m:plus|m:times|m:divide]">
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
@@ -262,7 +284,7 @@
 <!-- BASIC OPERATORS -->
 
  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
-       |m:geq|m:gt|m:plus|m:times]">
+       |m:geq|m:gt|m:plus|m:times|m:divide]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl
index 15071579a..a78f454bd 100644
--- a/helm/style/html_reals.xsl
+++ b/helm/style/html_reals.xsl
@@ -41,6 +41,9 @@
       <xsl:when test="$symbol = 'leadsto'">
        <xsl:value-of select="'&#174;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'sum'">
+       <xsl:value-of select="'&#229;'"/>
+      </xsl:when>
       <xsl:otherwise>
        <xsl:text>???</xsl:text>
       </xsl:otherwise>
@@ -56,6 +59,9 @@
       <xsl:when test="$symbol = 'leadsto'">
        <xsl:value-of select="'&#8594;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'sum'">
+       <xsl:value-of select="'&#x02211;'"/>
+      </xsl:when>
       <xsl:otherwise>
        <xsl:text>???</xsl:text>
       </xsl:otherwise>
@@ -72,6 +78,58 @@
 <!--                   INLINE MODE                                    -->
 <!-- **************************************************************** -->
 
+<!-- SUM -->
+
+<xsl:template mode="inline" match="m:apply[m:sum]">
+     <xsl:variable name="uri">
+      <xsl:value-of select="m:sum/@definitionURL"/>
+     </xsl:variable>
+     <xsl:choose>
+      <xsl:when test="$uri != ''">
+       <a href="{$uri}">
+       <!-- 
+       <FONT FACE="symbol" color="'blue'">
+        <xsl:value-of select="'&#229;'"/>
+       </FONT> -->
+       <xsl:call-template name="mksymbol-reals">
+        <xsl:with-param name="symbol" select="'sum'"/>
+      </xsl:call-template>
+       </a>
+      </xsl:when>
+      <xsl:otherwise>
+       <!-- 
+       <FONT FACE="symbol" color="'blue'">
+        <xsl:value-of select="'&#229;'"/>
+       </FONT> -->
+       <xsl:call-template name="mksymbol-reals">
+        <xsl:with-param name="symbol" select="'sum'"/>
+       </xsl:call-template>
+      </xsl:otherwise>
+     </xsl:choose>
+     <xsl:choose>
+      <xsl:when test="m:condition">
+       <SUB>
+        <xsl:apply-templates select="m:condition"/>
+       </SUB>
+      </xsl:when>
+      <xsl:otherwise>
+       <SUB>
+        <xsl:apply-templates select="m:lowlimit/*[1]"/>
+        <xsl:call-template name="mksymbol-init">
+         <xsl:with-param name="symbol" select="'leq'"/>
+        </xsl:call-template>
+        <xsl:apply-templates select="m:bvar/*[1]"/>
+        <xsl:call-template name="mksymbol-init">
+         <xsl:with-param name="symbol" select="'leq'"/>
+        </xsl:call-template>
+        <xsl:apply-templates select="m:uplimit/*[1]"/>
+       </SUB>
+      </xsl:otherwise>
+     </xsl:choose>
+     <xsl:apply-templates mode="inline" select="*[position()=last()]"/>
+ </xsl:template>
+
+
 <!-- LIMIT -->
 
 
@@ -202,6 +260,9 @@
 <!--                   COUNTING MODE                                    -->
 <!-- **************************************************************** -->
 
+<xsl:template match="m:apply[m:sum]">
+ <xsl:apply-templates mode="inline" select="."/>
+</xsl:template>
 
 <xsl:template match="m:apply[m:limit]">
   <xsl:param name="current_indent" select="0"/> 
@@ -384,8 +445,8 @@
 
 <!-- COUNTING -->
 
-<xsl:template match="m:abs|m:fact|m:root
-           |m:limit|m:diff|m:min|m:max" mode="charcount">
+<xsl:template match="m:abs|m:fact|m:root|
+           m:sum|m:limit|m:diff|m:min|m:max" mode="charcount">
 <xsl:param name="incurrent_length" select="0"/> 
     <xsl:choose>
     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 0651f65ec..4c207e482 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -79,7 +79,10 @@
   <xsl:otherwise>
    <xsl:choose>
     <xsl:when test="name()='APPLY'">
-     <xsl:apply-templates select="." mode="letin"/>
+     <!-- This is the case of an applicative expression wich is not
+          a proof but could contains proofs...
+          MODE LETIN OR MODE PURE ??? Big question -->
+     <xsl:apply-templates select="." mode="pure"/>
     </xsl:when>
     <xsl:otherwise>
      <xsl:apply-templates select="." mode="pure"/>
@@ -152,12 +155,55 @@
    </xsl:choose>
 </xsl:template>
 
+<xsl:template mode="eq_transitive" match="*">
+ <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+ <xsl:choose>
+  <xsl:when test="name()='APPLY'">
+   <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
+   <xsl:variable name="id" select="@id"/>
+   <xsl:choose>
+    <!-- ricordarsi di trattare il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+     <!-- <m:ci>eccomi-3</m:ci> -->
+     <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+     <xsl:apply-templates mode="noannot" select="*[4]"/>
+     <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:call-template name="generate_side_proof">
+      <xsl:with-param name="proof" select="."/>
+      <xsl:with-param name="show_statement" select="0"/>
+     </xsl:call-template> 
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:call-template name="generate_side_proof">
+    <xsl:with-param name="proof" select="."/>
+    <xsl:with-param name="show_statement" select="0"/>
+   </xsl:call-template>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
 
 <xsl:template mode="proof_transform" match="*">
  <xsl:choose>
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
+    <!-- Algebra equality (eq_transitive_unfolded) -->
+    <!-- It requires a special mode "eq_transitive"-->
+    <!-- togliere il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>eq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>
     <!-- EQUALITY -->
     <xsl:when test="CONST[
  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
@@ -434,6 +480,7 @@
 
 <xsl:template name="generate_side_proof">
  <xsl:param name="proof" select="/.."/>
+ <xsl:param name="show_statement" select="1"/>
 <!-- 
  <xsl:variable name="is_simple">
   <xsl:call-template name="is_simple">
@@ -453,7 +500,20 @@
    </xsl:choose>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-templates select="$proof" mode="noannot"/>
+   <xsl:variable name="id" select="@id"/>
+   <m:apply helm:xref="{@id}">
+    <xsl:choose>
+     <xsl:when test="$show_statement = 1">
+      <m:csymbol>proof</m:csymbol>
+     </xsl:when>
+     <xsl:otherwise>
+      <m:csymbol>side_proof</m:csymbol>
+     </xsl:otherwise>
+    </xsl:choose>
+    <xsl:apply-templates mode="proof_transform" select="."/>
+    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+   </m:apply>
+   <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
   </xsl:otherwise>
  </xsl:choose>
 </xsl:template>
diff --git a/helm/style/set.xsl b/helm/style/set.xsl
index 5ff4fce0b..f1f7b7e50 100644
--- a/helm/style/set.xsl
+++ b/helm/style/set.xsl
@@ -488,4 +488,51 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
     </xsl:choose>
 </xsl:template>
 
+<!-- *******************  SIGMA TYPES  **************************** -->
+
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/Subsets/sig.ind']]" mode="pure">
+ <xsl:choose>
+  <xsl:when test="count(child::*) = 3">
+   <xsl:choose>
+    <xsl:when test="name(*[3]) = 'LAMBDA'">
+     <m:set>
+       <m:bvar>
+        <m:ci>
+         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template>
+        </m:ci>
+        <m:type>
+         <xsl:apply-templates select="*[3]/source/*[1]" mode="noannot"/>
+        </m:type>
+       </m:bvar>
+       <m:condition>
+        <xsl:apply-templates select="*[3]/target/*[1]" mode="noannot"/>
+       </m:condition>
+     </m:set>
+    </xsl:when>
+    <xsl:otherwise>
+     <m:set>
+       <m:bvar>
+        <m:ci>$x</m:ci>
+        <m:type>
+         <xsl:apply-templates select="*[2]" mode="noannot"/>
+        </m:type>
+       </m:bvar>
+       <m:condition>
+        <m:apply>
+         <m:csymbol>app</m:csymbol>
+         <xsl:apply-templates select="*[3]" mode="noannot"/>
+         <m:ci>$x</m:ci>
+        </m:apply>
+       </m:condition>
+     </m:set>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-imports/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
 </xsl:stylesheet>
-- 
2.39.2