helm/style/set.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 Set Theory                                                 -->
  29 <!-- First draft: April 3 2000                                        -->
  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
  38 <!-- ************************* LOGIC *********************************-->
  39
  40
  41 <xsl:template match="*" mode="set">
  42     <xsl:choose>
  43      <xsl:when test="name() = 'LAMBDA'">
  44       <m:set>
  45        <m:bvar>
  46         <m:ci>
  47          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[1]/@binder"/></xsl:with-param></xsl:call-template>
  48         </m:ci>
  49         <m:type>
  50          <xsl:apply-templates select="*[1]" mode="noannot"/>
  51         </m:type>
  52        </m:bvar>
  53        <m:condition>
  54         <xsl:apply-templates select="*[2]" mode="lambda"/>
  55        </m:condition>
  56       </m:set>
  57      </xsl:when>
  58      <xsl:otherwise>
  59       <xsl:apply-templates select="." mode="noannot"/>
  60      </xsl:otherwise>
  61     </xsl:choose>
  62 </xsl:template>
  63
  64 <!-- IN -->
  65
  66 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]" mode="pure">
  67     <xsl:variable name="no_params">
  68      <xsl:call-template name="get_no_params">
  69       <xsl:with-param name="first_uri" select="$CICURI"/>
  70       <xsl:with-param name="second_uri" select="CONST/@uri"/>
  71      </xsl:call-template>
  72     </xsl:variable>
  73     <xsl:choose>
  74      <xsl:when test="(count(child::*) - number($no_params)) = 3">
  75       <m:apply helm:xref="{@id}">
  76        <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
  77        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
  78        <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
  79        <xsl:apply-templates select="*[2+$no_params]" mode="set" />
  80       </m:apply>
  81      </xsl:when>
  82      <xsl:otherwise>
  83       <xsl:apply-imports/>
  84      </xsl:otherwise>
  85     </xsl:choose>
  86 </xsl:template>
  87
  88
  89 <!-- NOT-IN -->
  90 <!-- NOT ha no parameters -->
  91 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
  92 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]]" mode="pure">
  93     <xsl:variable name="no_params">
  94      <xsl:call-template name="get_no_params">
  95       <xsl:with-param name="first_uri" select="$CICURI"/>
  96       <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
  97      </xsl:call-template>
  98     </xsl:variable>
  99     <xsl:choose>
 100      <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
 101       <m:apply helm:xref="{@id}">
 102        <m:notin/>
 103        <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
 104   <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
 105        <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
 106       </m:apply>
 107      </xsl:when>
 108      <xsl:otherwise>
 109       <xsl:apply-imports/>
 110      </xsl:otherwise>
 111     </xsl:choose>
 112 </xsl:template>
 113
 114 <!-- EMPTY SET -->
 115
 116 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Empty_set.ind']]" mode="pure">
 117     <xsl:variable name="no_params">
 118      <xsl:call-template name="get_no_params">
 119       <xsl:with-param name="first_uri" select="$CICURI"/>
 120       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 121      </xsl:call-template>
 122     </xsl:variable>
 123     <xsl:choose>
 124      <xsl:when test="(count(child::*) - number($no_params)) = 1">
 125       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 126       </m:set>
 127      </xsl:when>
 128      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 129       <m:apply helm:xref="{@id}">
 130        <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 131        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 132        <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 133        </m:set>
 134       </m:apply>
 135      </xsl:when>
 136      <xsl:otherwise>
 137       <xsl:apply-imports/>
 138      </xsl:otherwise>
 139     </xsl:choose>
 140 </xsl:template>
 141
 142 <!-- SINGLETON -->
 143
 144 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Singleton.ind']]" mode="pure">
 145     <xsl:variable name="no_params">
 146      <xsl:call-template name="get_no_params">
 147       <xsl:with-param name="first_uri" select="$CICURI"/>
 148       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 149      </xsl:call-template>
 150     </xsl:variable>
 151     <xsl:choose>
 152      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 153       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 154        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 155       </m:set>
 156      </xsl:when>
 157      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 158       <m:apply helm:xref="{@id}">
 159        <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 160        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 161        <m:set definitionURL="{MUTIND/@uri}">
 162         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 163        </m:set>
 164       </m:apply>
 165      </xsl:when>
 166      <xsl:otherwise>
 167       <xsl:apply-imports/>
 168      </xsl:otherwise>
 169     </xsl:choose>
 170 </xsl:template>
 171
 172 <!-- COUPLE -->
 173
 174 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Couple.ind']]" mode="pure">
 175     <xsl:variable name="no_params">
 176      <xsl:call-template name="get_no_params">
 177       <xsl:with-param name="first_uri" select="$CICURI"/>
 178       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 179      </xsl:call-template>
 180     </xsl:variable>
 181     <xsl:choose>
 182      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 183       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 184        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 185        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 186       </m:set>
 187      </xsl:when>
 188      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 189       <m:apply helm:xref="{@id}">
 190        <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 191        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 192        <m:set definitionURL="{MUTIND/@uri}">
 193         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 194         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 195        </m:set>
 196       </m:apply>
 197      </xsl:when>
 198      <xsl:otherwise>
 199       <xsl:apply-imports/>
 200      </xsl:otherwise>
 201     </xsl:choose>
 202 </xsl:template>
 203
 204 <!-- TRIPLE -->
 205
 206 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
 207     <xsl:variable name="no_params">
 208      <xsl:call-template name="get_no_params">
 209       <xsl:with-param name="first_uri" select="$CICURI"/>
 210       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 211      </xsl:call-template>
 212     </xsl:variable>
 213     <xsl:choose>
 214      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 215       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 216        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 217        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 218        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 219       </m:set>
 220      </xsl:when>
 221      <xsl:when test="(count(child::*) - number($no_params)) = 5">
 222       <m:apply helm:xref="{@id}">
 223        <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 224        <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
 225        <m:set definitionURL="{MUTIND/@uri}">
 226         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 227         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 228         <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 229        </m:set>
 230       </m:apply>
 231      </xsl:when>
 232      <xsl:otherwise>
 233       <xsl:apply-imports/>
 234      </xsl:otherwise>
 235     </xsl:choose>
 236 </xsl:template>
 237
 238 <!-- INTERSECTION -->
 239
 240 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Intersection.ind']]" mode="pure">
 241     <xsl:variable name="no_params">
 242      <xsl:call-template name="get_no_params">
 243       <xsl:with-param name="first_uri" select="$CICURI"/>
 244       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 245      </xsl:call-template>
 246     </xsl:variable>
 247     <xsl:choose>
 248      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 249       <m:apply helm:xref="{@id}">
 250        <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 251        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 252        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 253       </m:apply>
 254      </xsl:when>
 255      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 256       <m:apply helm:xref="{@id}">
 257        <m:in/>
 258        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 259        <m:apply>
 260         <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 261         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 262         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 263        </m:apply>
 264       </m:apply>
 265      </xsl:when>
 266      <xsl:otherwise>
 267       <xsl:apply-imports/>
 268      </xsl:otherwise>
 269     </xsl:choose>
 270 </xsl:template>
 271
 272
 273 <!-- UNION -->
 274
 275 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Union.ind']]" mode="pure">
 276     <xsl:variable name="no_params">
 277      <xsl:call-template name="get_no_params">
 278       <xsl:with-param name="first_uri" select="$CICURI"/>
 279       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 280      </xsl:call-template>
 281     </xsl:variable>
 282     <xsl:choose>
 283      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 284       <m:apply helm:xref="{@id}">
 285        <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 286        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 287        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 288       </m:apply>
 289      </xsl:when>
 290      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 291       <m:apply helm:xref="{@id}">
 292        <m:in/>
 293        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 294        <m:apply>
 295         <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 296         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 297         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 298        </m:apply>
 299       </m:apply>
 300      </xsl:when>
 301      <xsl:otherwise>
 302       <xsl:apply-imports/>
 303      </xsl:otherwise>
 304     </xsl:choose>
 305 </xsl:template>
 306
 307 <!-- INCLUDED -->
 308
 309 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Included.con']]" mode="pure">
 310     <xsl:variable name="no_params">     <xsl:call-template name="get_no_params">
 311       <xsl:with-param name="first_uri" select="$CICURI"/>
 312       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 313      </xsl:call-template>
 314     </xsl:variable>
 315     <xsl:choose>
 316      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 317       <m:apply helm:xref="{@id}">
 318        <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 319        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 320        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 321       </m:apply>
 322      </xsl:when>
 323      <xsl:otherwise>
 324       <xsl:apply-imports/>
 325      </xsl:otherwise>
 326     </xsl:choose>
 327 </xsl:template>
 328
 329 <!-- STRICTLY INCLUDED -->
 330
 331 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Strict_Included.con']]" mode="pure">
 332     <xsl:variable name="no_params">
 333      <xsl:call-template name="get_no_params">
 334       <xsl:with-param name="first_uri" select="$CICURI"/>
 335       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 336      </xsl:call-template>
 337     </xsl:variable>
 338     <xsl:choose>
 339      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 340       <m:apply helm:xref="{@id}">
 341        <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 342        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 343        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 344       </m:apply>
 345      </xsl:when>
 346      <xsl:otherwise>
 347       <xsl:apply-imports/>
 348      </xsl:otherwise>
 349     </xsl:choose>
 350 </xsl:template>
 351
 352 <!-- SET-DIFF -->
 353
 354 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Setminus.con']]" mode="pure">
 355     <xsl:variable name="no_params">
 356      <xsl:call-template name="get_no_params">
 357       <xsl:with-param name="first_uri" select="$CICURI"/>
 358       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 359      </xsl:call-template>
 360     </xsl:variable>
 361     <xsl:choose>
 362      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 363       <m:apply helm:xref="{@id}">
 364        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 365        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 366        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 367       </m:apply>
 368      </xsl:when>
 369      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 370       <m:apply helm:xref="{@id}">
 371        <m:in/>
 372        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 373        <m:apply>
 374         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 375         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 376         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 377        </m:apply>
 378       </m:apply>
 379      </xsl:when>
 380      <xsl:otherwise>
 381       <xsl:apply-imports/>
 382      </xsl:otherwise>
 383     </xsl:choose>
 384 </xsl:template>
 385
 386 <!-- ADD-ELEM -->
 387
 388 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Add.con']]" mode="pure">
 389     <xsl:variable name="no_params">
 390      <xsl:call-template name="get_no_params">
 391       <xsl:with-param name="first_uri" select="$CICURI"/>
 392       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 393      </xsl:call-template>
 394     </xsl:variable>
 395     <xsl:choose>
 396      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 397       <m:apply helm:xref="{@id}">
 398        <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 399        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 400        <m:set>
 401         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 402        </m:set>
 403       </m:apply>
 404      </xsl:when>
 405      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 406       <m:apply helm:xref="{@id}">
 407        <m:in/>
 408        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 409        <m:apply>
 410         <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 411         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 412         <m:set>
 413          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 414         </m:set>
 415        </m:apply>
 416       </m:apply>
 417      </xsl:when>
 418      <xsl:otherwise>
 419       <xsl:apply-imports/>
 420      </xsl:otherwise>
 421     </xsl:choose>
 422 </xsl:template>
 423
 424 <!-- SUBTRACT-ELEM -->
 425
 426 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Subtract.con']]" mode="pure">
 427     <xsl:variable name="no_params">
 428      <xsl:call-template name="get_no_params">
 429       <xsl:with-param name="first_uri" select="$CICURI"/>
 430       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 431      </xsl:call-template>
 432     </xsl:variable>
 433     <xsl:choose>
 434      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 435       <m:apply helm:xref="{@id}">
 436        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 437        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 438        <m:set>
 439         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 440        </m:set>
 441       </m:apply>
 442      </xsl:when>
 443      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 444       <m:apply helm:xref="{@id}">
 445        <m:in/>
 446        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 447        <m:apply>
 448         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 449         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 450         <m:set>
 451          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 452         </m:set>
 453        </m:apply>
 454       </m:apply>
 455      </xsl:when>
 456      <xsl:otherwise>
 457       <xsl:apply-imports/>
 458      </xsl:otherwise>
 459     </xsl:choose>
 460 </xsl:template>
 461
 462 <!-- CARD -->
 463
 464 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/cardinal.ind']]" mode="pure">
 465     <xsl:variable name="no_params">
 466      <xsl:call-template name="get_no_params">
 467       <xsl:with-param name="first_uri" select="$CICURI"/>
 468       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 469      </xsl:call-template>
 470     </xsl:variable>
 471     <xsl:choose>
 472      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 473       <m:apply helm:xref="{@id}">
 474        <m:eq/>
 475        <m:apply>
 476         <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 477         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 478        </m:apply>
 479        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 480       </m:apply>
 481      </xsl:when>
 482      <xsl:otherwise>
 483       <xsl:apply-imports/>
 484      </xsl:otherwise>
 485     </xsl:choose>
 486 </xsl:template>
 487
 488 <!-- *******************  SIGMA TYPES  **************************** -->
 489
 490
 491 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/sig.ind']]" mode="pure">
 492  <xsl:choose>
 493   <xsl:when test="count(child::*) = 3">
 494    <xsl:choose>
 495     <xsl:when test="name(*[3]) = 'LAMBDA'">
 496      <m:set>
 497        <m:bvar>
 498         <m:ci>
 499          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/*[1]/@binder"/></xsl:with-param></xsl:call-template>
 500         </m:ci>
 501         <m:type>
 502          <xsl:apply-templates select="*[3]/*[1]/*[1]" mode="noannot"/>
 503         </m:type>
 504        </m:bvar>
 505        <m:condition>
 506         <xsl:apply-templates select="*[3]/*[2]" mode="lambda"/>
 507        </m:condition>
 508      </m:set>
 509     </xsl:when>
 510     <xsl:otherwise>
 511      <m:set>
 512        <m:bvar>
 513         <m:ci>$x</m:ci>
 514         <m:type>
 515          <xsl:apply-templates select="*[2]" mode="noannot"/>
 516         </m:type>
 517        </m:bvar>
 518        <m:condition>
 519         <m:apply>
 520          <m:csymbol>app</m:csymbol>
 521          <xsl:apply-templates select="*[3]" mode="noannot"/>
 522          <m:ci>$x</m:ci>
 523         </m:apply>
 524        </m:condition>
 525      </m:set>
 526     </xsl:otherwise>
 527    </xsl:choose>
 528   </xsl:when>
 529   <xsl:otherwise>
 530    <xsl:apply-imports/>
 531   </xsl:otherwise>
 532  </xsl:choose>
 533 </xsl:template>
 534
 535
 536
 537 </xsl:stylesheet>