helm/style/proofs.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--******************************************************************-->
  28 <!-- Basic Logic                                                      -->
  29 <!-- (completely) Revisited: february 2001, Andrea Asperti            -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  35                               xmlns:helm="http://www.cs.unibo.it/helm">
  36
  37 <!-- ************************* LOGIC *********************************-->
  38
  39 <!-- Proof objects -->
  40
  41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  42
  43 <!-- ALL this elements does not have inner type -->
  44 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  45 <xsl:apply-templates select="." mode="pure"/>
  46 </xsl:template>
  47
  48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
  49
  50 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  51 <xsl:template match="LAMBDA" mode="noannot">
  52  <xsl:variable name="id" select="@id"/>
  53  <xsl:choose>
  54   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
  55    <m:apply helm:xref="{@id}">
  56     <m:csymbol>proof</m:csymbol>
  57     <xsl:apply-templates mode="proof_transform" select="."/>
  58     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  59    </m:apply>
  60   </xsl:when>
  61   <xsl:otherwise>
  62    <xsl:apply-templates select="." mode="pure"/>
  63   </xsl:otherwise>
  64  </xsl:choose>
  65 </xsl:template>
  66
  67 <!-- ALL these elements have inner type -->
  68 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  69  <xsl:variable name="id" select="@id"/>
  70  <xsl:choose>
  71   <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
  72    <m:apply helm:xref="{@id}">
  73     <m:csymbol>proof</m:csymbol>
  74     <xsl:apply-templates mode="proof_transform" select="."/>
  75     <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
  76     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
  77    </m:apply>
  78   </xsl:when>
  79   <xsl:otherwise>
  80    <xsl:choose>
  81     <xsl:when test="name()='APPLY'">
  82      <!-- This is the case of an applicative expression wich is not
  83           a proof but could contains proofs...
  84           MODE LETIN OR MODE PURE ??? Big question -->
  85      <xsl:apply-templates select="." mode="pure"/>
  86     </xsl:when>
  87     <xsl:otherwise>
  88      <xsl:apply-templates select="." mode="pure"/>
  89     </xsl:otherwise>
  90    </xsl:choose>
  91   </xsl:otherwise>
  92  </xsl:choose>
  93 </xsl:template>
  94
  95 <!-- si presuppone che il tipo induttivo non sia mutuamente
  96      induttivo. Bisognerebbe andare a vedere l'utlimo parametro
  97      del presunto "principio di induzione", tirare fuori il tipo induttivo
  98      e vedere se il suo nome coincide con il prefisso di _ind.
  99      Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
 100      parametro di nat_double_ind e' di tipo nat, e nat e' diverso
 101      da nat_double. Per ora, verifico solo l'esistenza di nat_double,
 102      ma questo, benche' non porti ad errore, non copre tutti i
 103      casi per quelli mutuamente induttivi -->
 104
 105 <xsl:template mode="try_inductive" match="APPLY">
 106    <xsl:variable name="id" select="@id"/>
 107    <xsl:choose>
 108     <xsl:when test="CONST[1]">
 109      <xsl:variable name="uri" select="CONST[1]/@uri"/>
 110      <xsl:choose>
 111       <xsl:when test="contains($uri,'_ind.con')">
 112        <xsl:variable name="ind_uri"
 113          select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
 114        <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
 115        <xsl:variable name="inductive_def"
 116      select="document($InductiveTypeUrl)/InductiveDefinition"/>
 117        <!-- check if the corresponding inductive definition actually
 118             exists -->
 119        <xsl:choose>
 120         <xsl:when test="$inductive_def">
 121          <xsl:variable name="ind_name">
 122           <xsl:call-template name="get_name">
 123            <xsl:with-param name="uri" select="$uri"/>
 124           </xsl:call-template>
 125          </xsl:variable>
 126          <xsl:variable name="no_params">
 127           <xsl:call-template name="get_no_params">
 128            <xsl:with-param name="first_uri" select="$CICURI"/>
 129            <xsl:with-param name="second_uri" select="$uri"/>
 130           </xsl:call-template>
 131          </xsl:variable>
 132          <xsl:apply-templates mode="inductive" select=".">
 133           <xsl:with-param name="inductive_def_uri"
 134            select="$ind_uri"/>
 135           <xsl:with-param name="inductive_def"
 136            select="$inductive_def"/>
 137           <xsl:with-param name="section_params" select="$no_params"/>
 138           <xsl:with-param name="inductive_def_index" select="1"/>
 139           <xsl:with-param name="inductive_def_name" select="$ind_name"/>
 140          </xsl:apply-templates>
 141         </xsl:when>
 142         <xsl:otherwise>
 143          <xsl:apply-templates mode="letin" select="."/>
 144         </xsl:otherwise>
 145        </xsl:choose>
 146       </xsl:when>
 147       <xsl:otherwise>
 148        <xsl:apply-templates mode="letin" select="."/>
 149       </xsl:otherwise>
 150      </xsl:choose>
 151     </xsl:when>
 152     <xsl:otherwise>
 153      <xsl:apply-templates mode="letin" select="."/>
 154     </xsl:otherwise>
 155    </xsl:choose>
 156 </xsl:template>
 157
 158 <xsl:template mode="eq_transitive" match="*">
 159  <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
 160  <xsl:choose>
 161   <xsl:when test="name()='APPLY'">
 162    <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
 163    <xsl:variable name="id" select="@id"/>
 164    <xsl:choose>
 165     <!-- ricordarsi di trattare il parametro -->
 166     <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
 167      <!-- <m:ci>eccomi-3</m:ci> -->
 168      <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
 169      <xsl:apply-templates mode="noannot" select="*[4]"/>
 170      <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
 171     </xsl:when>
 172     <xsl:otherwise>
 173      <xsl:call-template name="generate_side_proof">
 174       <xsl:with-param name="proof" select="."/>
 175       <xsl:with-param name="show_statement" select="0"/>
 176      </xsl:call-template>
 177     </xsl:otherwise>
 178    </xsl:choose>
 179   </xsl:when>
 180   <xsl:otherwise>
 181    <xsl:call-template name="generate_side_proof">
 182     <xsl:with-param name="proof" select="."/>
 183     <xsl:with-param name="show_statement" select="0"/>
 184    </xsl:call-template>
 185   </xsl:otherwise>
 186  </xsl:choose>
 187 </xsl:template>
 188
 189 <xsl:template mode="diseq" match="*">
 190   <xsl:param name="rel" select="'eq'"/>
 191   <xsl:choose>
 192   <xsl:when test="name()='APPLY'">
 193       <xsl:variable name="id" select="@id"/>
 194    <xsl:choose>
 195     <!-- ricordarsi di trattare il parametro -->
 196     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
 197        <xsl:apply-templates mode="diseq" select="*[6]">
 198         <xsl:with-param name="rel" select="'leq'"/>
 199        </xsl:apply-templates>
 200        <xsl:apply-templates mode="noannot" select="*[4]"/>
 201        <xsl:apply-templates mode="diseq" select="*[7]">
 202         <xsl:with-param name="rel" select="'leq'"/>
 203        </xsl:apply-templates>
 204     </xsl:when>
 205     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
 206        <m:eq/>
 207        <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
 208        <xsl:call-template name="generate_side_proof">
 209         <xsl:with-param name="proof" select="*[7]"/>
 210         <xsl:with-param name="show_statement" select="0"/>
 211        </xsl:call-template>
 212        <xsl:apply-templates mode="noannot" select="*[3]"/>
 213        <xsl:apply-templates mode="diseq" select="*[6]">
 214         <xsl:with-param name="rel" select="'leq'"/>
 215        </xsl:apply-templates>
 216     </xsl:when>
 217     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
 218        <xsl:apply-templates mode="diseq" select="*[6]">
 219         <xsl:with-param name="rel" select="'leq'"/>
 220        </xsl:apply-templates>
 221        <xsl:apply-templates mode="noannot" select="*[4]"/>
 222        <xsl:apply-templates mode="diseq" select="*[7]">
 223         <xsl:with-param name="rel" select="'lt'"/>
 224        </xsl:apply-templates>
 225     </xsl:when>
 226     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
 227        <xsl:apply-templates mode="diseq" select="*[6]">
 228         <xsl:with-param name="rel" select="'lt'"/>
 229        </xsl:apply-templates>
 230        <xsl:apply-templates mode="noannot" select="*[4]"/>
 231        <xsl:apply-templates mode="diseq" select="*[7]">
 232         <xsl:with-param name="rel" select="'leq'"/>
 233        </xsl:apply-templates>
 234     </xsl:when>
 235     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
 236        <xsl:apply-templates mode="diseq" select="*[6]">
 237         <xsl:with-param name="rel" select="'leq'"/>
 238        </xsl:apply-templates>
 239        <xsl:apply-templates mode="noannot" select="*[4]"/>
 240        <xsl:apply-templates mode="diseq" select="*[7]">
 241         <xsl:with-param name="rel" select="'eq'"/>
 242        </xsl:apply-templates>
 243     </xsl:when>
 244     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
 245       <xsl:apply-templates mode="diseq" select="*[6]">
 246         <xsl:with-param name="rel" select="'lt'"/>
 247        </xsl:apply-templates>
 248        <xsl:apply-templates mode="noannot" select="*[4]"/>
 249        <xsl:apply-templates mode="diseq" select="*[7]">
 250         <xsl:with-param name="rel" select="'lt'"/>
 251        </xsl:apply-templates>
 252      </xsl:when>
 253     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
 254        <xsl:apply-templates mode="diseq" select="*[6]">
 255         <xsl:with-param name="rel" select="'lt'"/>
 256        </xsl:apply-templates>
 257        <xsl:apply-templates mode="noannot" select="*[4]"/>
 258        <xsl:apply-templates mode="diseq" select="*[7]">
 259         <xsl:with-param name="rel" select="'eq'"/>
 260        </xsl:apply-templates>
 261      </xsl:when>
 262     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
 263        <m:eq/>
 264        <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
 265        <xsl:call-template name="generate_side_proof">
 266         <xsl:with-param name="proof" select="*[7]"/>
 267         <xsl:with-param name="show_statement" select="0"/>
 268        </xsl:call-template>
 269        <xsl:apply-templates mode="noannot" select="*[3]"/>
 270        <xsl:apply-templates mode="diseq" select="*[6]">
 271         <xsl:with-param name="rel" select="'lt'"/>
 272        </xsl:apply-templates>
 273     </xsl:when>
 274     <!--
 275     <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
 276      <xsl:apply-templates mode="diseq" select="*[6]"/>
 277      <m:eq/>
 278      <xsl:apply-templates mode="noannot" select="*[4]"/>
 279      <m:eq/>
 280      <xsl:apply-templates mode="diseq" select="*[7]"/>
 281     </xsl:when>
 282     -->
 283     <xsl:otherwise>
 284      <xsl:element name="{concat('m:',$rel)}"/>
 285      <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
 286      <xsl:call-template name="generate_side_proof">
 287       <xsl:with-param name="proof" select="."/>
 288       <xsl:with-param name="show_statement" select="0"/>
 289      </xsl:call-template>
 290     </xsl:otherwise>
 291    </xsl:choose>
 292   </xsl:when>
 293   <xsl:otherwise>
 294    <xsl:element name="{concat('m:',$rel)}"/>
 295    <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
 296    <xsl:call-template name="generate_side_proof">
 297     <xsl:with-param name="proof" select="."/>
 298     <xsl:with-param name="show_statement" select="0"/>
 299    </xsl:call-template>
 300   </xsl:otherwise>
 301  </xsl:choose>
 302 </xsl:template>
 303
 304 <xsl:template mode="proof_transform" match="*">
 305  <xsl:choose>
 306   <xsl:when test="name()='APPLY'">
 307    <xsl:variable name="id" select="@id"/>
 308    <xsl:choose>
 309     <!-- Algebra equality (eq_transitive_unfolded) -->
 310     <!-- It requires a special mode "eq_transitive"-->
 311     <!-- togliere il parametro -->
 312     <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
 313      <m:apply>
 314        <m:csymbol>eq_chain</m:csymbol>
 315        <xsl:apply-templates mode="noannot" select="*[3]"/>
 316        <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
 317        <xsl:apply-templates mode="noannot" select="*[4]"/>
 318        <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
 319        <xsl:apply-templates mode="noannot" select="*[5]"/>
 320      </m:apply>
 321     </xsl:when>
 322     <!-- Algebra disequalities -->
 323     <!-- It requires a special mode "diseq"-->
 324     <!-- togliere il parametro -->
 325     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
 326      <m:apply>
 327        <m:csymbol>diseq_chain</m:csymbol>
 328        <xsl:apply-templates mode="noannot" select="*[3]"/>
 329        <xsl:apply-templates mode="diseq" select="*[6]">
 330         <xsl:with-param name="rel" select="'leq'"/>
 331        </xsl:apply-templates>
 332        <xsl:apply-templates mode="noannot" select="*[4]"/>
 333        <xsl:apply-templates mode="diseq" select="*[7]">
 334         <xsl:with-param name="rel" select="'leq'"/>
 335        </xsl:apply-templates>
 336        <xsl:apply-templates mode="noannot" select="*[5]"/>
 337      </m:apply>
 338     </xsl:when>
 339      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
 340      <m:apply>
 341        <m:csymbol>diseq_chain</m:csymbol>
 342        <xsl:apply-templates mode="noannot" select="*[5]"/>
 343        <m:eq/>
 344        <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
 345        <xsl:call-template name="generate_side_proof">
 346         <xsl:with-param name="proof" select="*[7]"/>
 347         <xsl:with-param name="show_statement" select="0"/>
 348        </xsl:call-template>
 349        <xsl:apply-templates mode="noannot" select="*[3]"/>
 350        <xsl:apply-templates mode="diseq" select="*[6]">
 351         <xsl:with-param name="rel" select="'leq'"/>
 352        </xsl:apply-templates>
 353        <xsl:apply-templates mode="noannot" select="*[4]"/>
 354      </m:apply>
 355     </xsl:when>
 356     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
 357      <m:apply>
 358        <m:csymbol>diseq_chain</m:csymbol>
 359        <xsl:apply-templates mode="noannot" select="*[3]"/>
 360        <xsl:apply-templates mode="diseq" select="*[6]">
 361         <xsl:with-param name="rel" select="'leq'"/>
 362        </xsl:apply-templates>
 363        <xsl:apply-templates mode="noannot" select="*[4]"/>
 364        <xsl:apply-templates mode="diseq" select="*[7]">
 365         <xsl:with-param name="rel" select="'lt'"/>
 366        </xsl:apply-templates>
 367        <xsl:apply-templates mode="noannot" select="*[5]"/>
 368      </m:apply>
 369     </xsl:when>
 370     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
 371      <m:apply>
 372        <m:csymbol>diseq_chain</m:csymbol>
 373        <xsl:apply-templates mode="noannot" select="*[3]"/>
 374        <xsl:apply-templates mode="diseq" select="*[6]">
 375         <xsl:with-param name="rel" select="'lt'"/>
 376        </xsl:apply-templates>
 377        <xsl:apply-templates mode="noannot" select="*[4]"/>
 378        <xsl:apply-templates mode="diseq" select="*[7]">
 379         <xsl:with-param name="rel" select="'leq'"/>
 380        </xsl:apply-templates>
 381        <xsl:apply-templates mode="noannot" select="*[5]"/>
 382      </m:apply>
 383     </xsl:when>
 384     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
 385      <m:apply>
 386        <m:csymbol>diseq_chain</m:csymbol>
 387        <xsl:apply-templates mode="noannot" select="*[3]"/>
 388        <xsl:apply-templates mode="diseq" select="*[6]">
 389         <xsl:with-param name="rel" select="'leq'"/>
 390        </xsl:apply-templates>
 391        <xsl:apply-templates mode="noannot" select="*[4]"/>
 392        <xsl:apply-templates mode="diseq" select="*[7]">
 393         <xsl:with-param name="rel" select="'eq'"/>
 394        </xsl:apply-templates>
 395        <xsl:apply-templates mode="noannot" select="*[5]"/>
 396      </m:apply>
 397     </xsl:when>
 398     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
 399      <m:apply>
 400        <m:csymbol>diseq_chain</m:csymbol>
 401        <xsl:apply-templates mode="noannot" select="*[3]"/>
 402        <xsl:apply-templates mode="diseq" select="*[6]">
 403         <xsl:with-param name="rel" select="'lt'"/>
 404        </xsl:apply-templates>
 405        <xsl:apply-templates mode="noannot" select="*[4]"/>
 406        <xsl:apply-templates mode="diseq" select="*[7]">
 407         <xsl:with-param name="rel" select="'lt'"/>
 408        </xsl:apply-templates>
 409        <xsl:apply-templates mode="noannot" select="*[5]"/>
 410      </m:apply>
 411     </xsl:when>
 412     <!-- togliere il parametro -->
 413     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
 414      <m:apply>
 415        <m:csymbol>diseq_chain</m:csymbol>
 416        <xsl:apply-templates mode="noannot" select="*[3]"/>
 417        <xsl:apply-templates mode="diseq" select="*[6]">
 418         <xsl:with-param name="rel" select="'lt'"/>
 419        </xsl:apply-templates>
 420        <xsl:apply-templates mode="noannot" select="*[4]"/>
 421        <xsl:apply-templates mode="diseq" select="*[7]">
 422         <xsl:with-param name="rel" select="'eq'"/>
 423        </xsl:apply-templates>
 424        <xsl:apply-templates mode="noannot" select="*[5]"/>
 425      </m:apply>
 426     </xsl:when>
 427     <!-- togliere il parametro -->
 428     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
 429      <m:apply>
 430        <m:csymbol>diseq_chain</m:csymbol>
 431        <xsl:apply-templates mode="noannot" select="*[5]"/>
 432        <m:eq/>
 433        <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
 434        <xsl:call-template name="generate_side_proof">
 435         <xsl:with-param name="proof" select="*[7]"/>
 436         <xsl:with-param name="show_statement" select="0"/>
 437        </xsl:call-template>
 438        <xsl:apply-templates mode="noannot" select="*[3]"/>
 439        <xsl:apply-templates mode="diseq" select="*[6]">
 440         <xsl:with-param name="rel" select="'lt'"/>
 441        </xsl:apply-templates>
 442        <xsl:apply-templates mode="noannot" select="*[4]"/>
 443      </m:apply>
 444     </xsl:when>
 445     <!-- EQUALITY -->
 446     <xsl:when test="CONST[
 447  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 448  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 449  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 450  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 451  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 452       <m:apply>
 453        <m:csymbol>rw_step</m:csymbol>
 454        <xsl:apply-templates mode="noannot" select="*[5]"/>
 455        <xsl:apply-templates mode="pure" select="*[3]"/>
 456        <xsl:apply-templates mode="pure" select="*[6]"/>
 457        <xsl:call-template name="generate_side_proof">
 458         <xsl:with-param name="proof" select="*[7]"/>
 459        </xsl:call-template>
 460        <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
 461       </m:apply>
 462     </xsl:when>
 463     <!-- EQUALITY with extra-parameters -->
 464     <xsl:when test="CONST[
 465  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 466  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 467  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 468  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 469  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
 470       <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 471       <xsl:choose>
 472        <xsl:when test="$no_extraproofs=0">
 473         <m:apply>
 474          <m:csymbol>rewrite_and_apply</m:csymbol>
 475          <m:apply>
 476           <m:csymbol>rw_step</m:csymbol>
 477           <xsl:apply-templates mode="noannot" select="*[5]"/>
 478           <xsl:apply-templates mode="pure" select="*[3]"/>
 479           <xsl:apply-templates mode="pure" select="*[6]"/>
 480           <xsl:call-template name="generate_side_proof">
 481            <xsl:with-param name="proof" select="*[7]"/>
 482            </xsl:call-template>
 483           <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 484          </m:apply>
 485          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 486         </m:apply>
 487        </xsl:when>
 488        <xsl:otherwise>
 489         <xsl:choose>
 490          <xsl:when test="*[5]/@sort='Prop'">
 491           <m:apply helm:xref="{@id}">
 492            <m:csymbol>letin</m:csymbol>
 493            <m:apply>
 494             <m:csymbol>let</m:csymbol>
 495             <m:ci>
 496              <xsl:call-template name="insert_subscript">
 497               <xsl:with-param name="node_value" select="'h1'"/>
 498              </xsl:call-template>
 499             </m:ci>
 500             <xsl:apply-templates mode="noannot" select="*[5]"/>
 501            </m:apply>
 502            <xsl:call-template name="gen_let">
 503             <xsl:with-param name="init_pos" select="1"/>
 504             <xsl:with-param name="from" select="7"/>
 505            </xsl:call-template>
 506            <m:apply>
 507             <m:csymbol>rewrite_and_apply</m:csymbol>
 508             <m:apply>
 509              <m:csymbol>rw_step</m:csymbol>
 510              <m:ci>
 511               <xsl:call-template name="insert_subscript">
 512                <xsl:with-param name="node_value" select="'h1'"/>
 513               </xsl:call-template>
 514              </m:ci>
 515              <xsl:apply-templates mode="pure" select="*[3]"/>
 516              <xsl:apply-templates mode="pure" select="*[6]"/>
 517              <xsl:call-template name="generate_side_proof">
 518               <xsl:with-param name="proof" select="*[7]"/>
 519              </xsl:call-template>
 520              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 521             </m:apply>
 522             <xsl:apply-templates mode="flat" select="*[8]">
 523              <xsl:with-param name="n">
 524               <xsl:value-of select="2"/>
 525              </xsl:with-param>
 526             </xsl:apply-templates>
 527            </m:apply>
 528           </m:apply>
 529          </xsl:when>
 530          <xsl:otherwise>
 531           <m:apply helm:xref="{@id}">
 532            <m:csymbol>letin</m:csymbol>
 533            <xsl:call-template name="gen_let">
 534             <xsl:with-param name="init_pos" select="0"/>
 535             <xsl:with-param name="form" select="7"/>
 536            </xsl:call-template>
 537            <m:apply>
 538             <m:csymbol>rewrite_and_apply</m:csymbol>
 539             <m:apply>
 540              <m:csymbol>rw_step</m:csymbol>
 541              <xsl:apply-templates mode="pure" select="*[5]"/>
 542              <xsl:apply-templates mode="pure" select="*[3]"/>
 543              <xsl:apply-templates mode="pure" select="*[6]"/>
 544              <xsl:call-template name="generate_side_proof">
 545               <xsl:with-param name="proof" select="*[7]"/>
 546              </xsl:call-template>
 547              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 548             </m:apply>
 549             <xsl:apply-templates mode="flat" select="*[8]">
 550              <xsl:with-param name="n">
 551               <xsl:value-of select="1"/>
 552              </xsl:with-param>
 553             </xsl:apply-templates>
 554            </m:apply>
 555           </m:apply>
 556          </xsl:otherwise>
 557         </xsl:choose>
 558        </xsl:otherwise>
 559       </xsl:choose>
 560     </xsl:when>
 561     <!-- False_ind -->
 562     <xsl:when test="CONST[
 563      attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
 564      count(child::*) = 3">
 565      <m:apply helm:xref="{@id}">
 566        <m:csymbol>false_ind</m:csymbol>
 567        <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
 568        <xsl:apply-templates mode="noannot" select="*[3]"/>
 569      </m:apply>
 570     </xsl:when>
 571     <!-- gestire meglio il caso di and_ind quando la prova
 572          non e' della forma \x.\y.M -->
 573     <xsl:when test="CONST[
 574  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 575  and count(child::*) = 6
 576  and name(*[5])='LAMBDA'
 577  and name(*[5]/target/*[1])='LAMBDA'">
 578       <m:apply helm:xref="{@id}">
 579        <m:csymbol>and_ind</m:csymbol>
 580        <xsl:apply-templates mode="noannot" select="*[6]"/>
 581        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 582        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 583        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 584        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 585        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 586       </m:apply>
 587     </xsl:when>
 588     <xsl:when test="CONST[
 589  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 590  and count(child::*) = 7">
 591       <xsl:choose>
 592        <xsl:when test="name(*[5])='LAMBDA'
 593                  and name(*[6])='LAMBDA'">
 594         <xsl:variable name="definition_url"
 595             select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
 596         <m:apply helm:xref="{@id}">
 597          <m:csymbol>full_or_ind</m:csymbol>
 598          <xsl:apply-templates mode="noannot" select="*[7]"/>
 599          <xsl:apply-templates mode="pure"
 600               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 601          <m:apply>
 602           <m:csymbol>left_case</m:csymbol>
 603           <m:bvar>
 604            <m:ci>
 605             <xsl:value-of select="*[5]/target/@binder"/>
 606            </m:ci>
 607            <m:type>
 608             <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
 609            </m:type>
 610           </m:bvar>
 611           <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
 612          </m:apply>
 613          <m:apply>
 614           <m:csymbol>right_case</m:csymbol>
 615           <m:bvar>
 616            <m:ci>
 617             <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
 618            </m:ci>
 619            <m:type>
 620             <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
 621            </m:type>
 622           </m:bvar>
 623           <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
 624          </m:apply>
 625         </m:apply>
 626        </xsl:when>
 627        <xsl:otherwise>
 628         <m:apply helm:xref="{@id}">
 629          <m:csymbol>or_ind</m:csymbol>
 630          <xsl:apply-templates mode="noannot" select="*[7]"/>
 631          <xsl:apply-templates mode="pure"
 632               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 633          <xsl:apply-templates mode="pure" select="*[5]"/>
 634          <xsl:apply-templates mode="pure" select="*[6]"/>
 635         </m:apply>
 636        </xsl:otherwise>
 637       </xsl:choose>
 638     </xsl:when>
 639     <!-- ex_ind, exT_ind -->
 640       <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 641       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 642  and count(child::*) = 6
 643  and name(*[5])='LAMBDA'
 644  and name(*[5]/target/*[1])='LAMBDA'">
 645       <m:apply helm:xref="{@id}">
 646        <m:csymbol>ex_ind</m:csymbol>
 647        <xsl:apply-templates mode="noannot" select="*[6]"/>
 648        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 649        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 650        <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 651        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 652        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 653       </m:apply>
 654     </xsl:when>
 655     <xsl:when test="name(*[1])='CONST'">
 656      <xsl:apply-templates mode="try_inductive" select="."/>
 657     </xsl:when>
 658     <!-- patch temporanea per la gestione di redex -->
 659     <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
 660          and *[2]/@sort='Prop'">
 661      <m:apply helm:xref="{@id}">
 662       <m:csymbol>letin</m:csymbol>
 663       <m:apply>
 664        <m:csymbol>let</m:csymbol>
 665        <m:ci>
 666         <xsl:call-template name="insert_subscript">
 667          <xsl:with-param name="node_value">
 668           <xsl:value-of select="*[1]/target/@binder"/>
 669          </xsl:with-param>
 670         </xsl:call-template>
 671        </m:ci>
 672        <xsl:apply-templates mode="noannot" select="*[2]"/>
 673       </m:apply>
 674       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
 675      </m:apply>
 676     </xsl:when>
 677     <xsl:otherwise>
 678      <xsl:apply-templates select="." mode="letin"/>
 679     </xsl:otherwise>
 680    </xsl:choose>
 681   </xsl:when>
 682   <xsl:when test="name()='LAMBDA'">
 683    <xsl:choose>
 684      <xsl:when test="(name(target/*[1])='APPLY'  and
 685       name(target/*[1]/*[1])='CONST' and
 686       (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 687        target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 688        target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
 689       and count(target/*[1]/*) = 8
 690       and name(target/*[1]/*[8])='REL'
 691       and target/@binder = target/*[1]/*[8]/@binder )">
 692       <m:apply>
 693        <m:csymbol>rw_step</m:csymbol>
 694        <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
 695        <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
 696        <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
 697        <xsl:call-template name="generate_side_proof">
 698         <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
 699        </xsl:call-template>
 700        <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
 701       </m:apply>
 702      </xsl:when>
 703      <xsl:otherwise>
 704       <xsl:apply-templates mode="pure" select="."/>
 705      </xsl:otherwise>
 706     </xsl:choose>
 707    </xsl:when>
 708   <xsl:otherwise>
 709    <xsl:apply-templates select="." mode="pure"/>
 710   </xsl:otherwise>
 711  </xsl:choose>
 712 </xsl:template>
 713
 714 <xsl:template name="is_simple">
 715  <xsl:param name="proof" select="/.."/>
 716  <xsl:value-of select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
 717 </xsl:template>
 718
 719 <xsl:template name="generate_side_proof">
 720  <xsl:param name="proof" select="/.."/>
 721  <xsl:param name="show_statement" select="1"/>
 722 <!--
 723  <xsl:variable name="is_simple">
 724   <xsl:call-template name="is_simple">
 725    <xsl:with-param name="proof" select="$proof"/>
 726   </xsl:call-template>
 727  </xsl:variable> -->
 728 <xsl:variable name="is_simple" select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
 729  <xsl:choose>
 730   <xsl:when test="$is_simple">
 731    <xsl:choose>
 732     <xsl:when test="name($proof)='APPLY'">
 733      <xsl:apply-templates select="$proof" mode="letin"/>
 734     </xsl:when>
 735     <xsl:otherwise>
 736      <xsl:apply-templates select="$proof" mode="pure"/>
 737     </xsl:otherwise>
 738    </xsl:choose>
 739   </xsl:when>
 740   <xsl:otherwise>
 741    <xsl:variable name="id" select="@id"/>
 742    <m:apply helm:xref="{@id}">
 743     <xsl:choose>
 744      <xsl:when test="$show_statement = 1">
 745       <m:csymbol>proof</m:csymbol>
 746      </xsl:when>
 747      <xsl:otherwise>
 748       <m:csymbol>side_proof</m:csymbol>
 749      </xsl:otherwise>
 750     </xsl:choose>
 751     <xsl:apply-templates mode="proof_transform" select="$proof"/>
 752     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$proof/@id]/*"/>
 753    </m:apply>
 754    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
 755   </xsl:otherwise>
 756  </xsl:choose>
 757 </xsl:template>
 758
 759 <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 760
 761 <xsl:template match="APPLY" mode="letin">
 762    <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 763    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 764    <xsl:choose>
 765     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 766      <m:apply helm:xref="{@id}">
 767       <m:csymbol>letin1</m:csymbol>
 768       <xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 769       <!-- now re-process the application -->
 770       <m:apply helm:xref="{@id}">
 771        <m:csymbol>app</m:csymbol>
 772        <!-- mode previous looks for siblings:
 773             call with the first child -->
 774        <xsl:apply-templates mode="previous" select="*[1]"/>
 775       </m:apply>
 776      </m:apply>
 777     </xsl:when>
 778     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 779      <m:apply helm:xref="{@id}">
 780       <m:csymbol>letin</m:csymbol>
 781       <!-- first process all subproofs (let-in) -->
 782       <xsl:call-template name="gen_let"/>
 783       <!-- now re-process the application  -->
 784       <m:apply helm:xref="{@id}">
 785        <m:csymbol>app</m:csymbol>
 786        <!-- mode flat looks for siblings: call with the first child -->
 787        <xsl:apply-templates mode="flat" select="*[1]"/>
 788       </m:apply>
 789      </m:apply>
 790     </xsl:when>
 791     <xsl:otherwise>
 792      <xsl:choose>
 793      <xsl:when test="@sort='Prop'">
 794       <m:apply>
 795        <m:csymbol>app</m:csymbol>
 796        <xsl:apply-templates mode="erase" select="*[1]"/>
 797       </m:apply>
 798      </xsl:when>
 799      <xsl:otherwise>
 800       <xsl:apply-templates mode="pure" select="."/>
 801      </xsl:otherwise>
 802      </xsl:choose>
 803     </xsl:otherwise>
 804    </xsl:choose>
 805 </xsl:template>
 806
 807 <xsl:template name="gen_let">
 808  <xsl:param name="init_pos" select="0"/>
 809  <xsl:param name="from" select="0"/>
 810       <xsl:for-each select="*[position()>$from and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
 811        <m:apply>
 812         <m:csymbol>let</m:csymbol>
 813         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
 814         <xsl:apply-templates mode="noannot" select="."/>
 815        </m:apply>
 816       </xsl:for-each>
 817 </xsl:template>
 818
 819 <xsl:template match="*" mode="erase">
 820   <xsl:choose>
 821    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 822     <xsl:apply-templates mode="pure" select="."/>
 823    </xsl:when>
 824    <xsl:otherwise>
 825     <m:ci>.</m:ci>
 826    </xsl:otherwise>
 827    </xsl:choose>
 828  <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
 829 </xsl:template>
 830
 831 <xsl:template match="*" mode="previous">
 832  <xsl:choose>
 833   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 834    <m:ci>previous</m:ci>
 835   </xsl:when>
 836   <xsl:otherwise>
 837    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
 838    <xsl:choose>
 839    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 840     <xsl:apply-templates mode="pure" select="."/>
 841    </xsl:when>
 842    <xsl:otherwise>
 843     <m:ci>.</m:ci>
 844    </xsl:otherwise>
 845    </xsl:choose>
 846    <!-- <xsl:apply-templates select="." mode="pure"/> -->
 847   </xsl:otherwise>
 848  </xsl:choose>
 849  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 850 </xsl:template>
 851
 852 <xsl:template match="*" mode="flat">
 853  <xsl:param name="n" select="1"/>
 854  <xsl:variable name="id" select="@id"/>
 855  <xsl:choose>
 856   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 857    <m:ci>
 858     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
 859    </m:ci>
 860    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 861     <xsl:with-param name="n" select="$n+1"/>
 862    </xsl:apply-templates>
 863   </xsl:when>
 864   <xsl:otherwise>
 865    <xsl:choose>
 866     <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
 867      <xsl:apply-templates mode="pure" select="."/>
 868     </xsl:when>
 869     <xsl:otherwise>
 870      <m:ci>.</m:ci>
 871     </xsl:otherwise>
 872    </xsl:choose>
 873    <!-- <xsl:apply-templates mode="pure" select="."/> -->
 874    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 875     <xsl:with-param name="n" select="$n"/>
 876    </xsl:apply-templates>
 877   </xsl:otherwise>
 878  </xsl:choose>
 879 </xsl:template>
 880
 881 <!-- Auxiliary functions -->
 882 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
 883 <!-- can replace the next template                                    -->
 884 <xsl:template name="get_name">
 885  <xsl:param name="uri" select="''"/>
 886  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 887  <xsl:choose>
 888   <xsl:when test="contains($sub_after,'/')">
 889    <xsl:call-template name="get_name">
 890     <xsl:with-param name="uri" select="$sub_after"/>
 891    </xsl:call-template>
 892   </xsl:when>
 893   <xsl:otherwise>
 894    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 895   </xsl:otherwise>
 896  </xsl:choose>
 897 </xsl:template>
 898
 899 <!-- <xsl:template match="APPLY[CONST[
 900  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 901     <xsl:choose>
 902      <xsl:when test="count(child::*) > 4">
 903       <m:apply helm:xref="{@id}">
 904        <m:csymbol>app</m:csymbol>
 905        <xsl:apply-templates mode="pure" select="*[1]"/>
 906        <m:ci>*</m:ci>
 907        <m:ci>*</m:ci>
 908        <m:ci>*</m:ci>
 909        <xsl:apply-templates mode="flat" select="*[5]"/>
 910       </m:apply>
 911      </xsl:when>
 912      <xsl:otherwise>
 913       <m:apply helm:xref="{@id}">
 914        <m:csymbol>app</m:csymbol>
 915        <xsl:apply-templates mode="flat" select="*[1]"/>
 916       </m:apply>
 917      </xsl:otherwise>
 918     </xsl:choose>
 919 </xsl:template>  -->
 920
 921
 922 </xsl:stylesheet>