helm/nuprl_stylesheets/nuprl_rules.xsl

   1 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
   2                               xmlns:m="http://www.w3.org/1998/Math/MathML"
   3                               xmlns:cn="http://www.......">
   4
   5 <xsl:template match="level-expression">
   6   <m:apply>
   7     <m:ci>level-exp</m:ci>
   8     <m:ci>
   9       <xsl:value-of select="@level"/>
  10     </m:ci>
  11   </m:apply>
  12 </xsl:template>
  13
  14 <xsl:template match="parameter-substitution-list">
  15   <m:apply>
  16     <m:ci>parameter-substitution-list</m:ci>
  17     <m:ci>
  18       <xsl:value-of select="@val"/>
  19     </m:ci>
  20   </m:apply>
  21 </xsl:template>
  22
  23
  24 <xsl:template match="tag">
  25   <m:apply>
  26     <m:ci>tag <xsl:value-of select="@step"/>:</m:ci>
  27     <xsl:apply-templates/>
  28   </m:apply>
  29 </xsl:template>
  30
  31 <xsl:template match="dependent_functionFormation">
  32   <m:apply>
  33     <m:ci>dependent_functionFormation</m:ci>
  34     <xsl:apply-templates/>
  35   </m:apply>
  36 </xsl:template>
  37
  38 <xsl:template match="independent_functionFormation">
  39   <m:ci>independent_functionFormation</m:ci>
  40 </xsl:template>
  41
  42 <xsl:template match="functionEquality">
  43   <m:apply>
  44     <m:ci>functionEquality</m:ci>
  45     <xsl:apply-templates/>
  46   </m:apply>
  47 </xsl:template>
  48
  49 <xsl:template match="independent_functionEquality">
  50   <m:ci>independent_functionEquality</m:ci>
  51 </xsl:template>
  52
  53 <xsl:template match="lambdaEquality">
  54   <m:apply>
  55     <m:ci>lambdaEquality</m:ci>
  56     <xsl:apply-templates/>
  57   </m:apply>
  58 </xsl:template>
  59
  60 <xsl:template match="lambdaFormation">
  61   <m:apply>
  62     <m:ci>lambdaFormation</m:ci>
  63     <xsl:apply-templates/>
  64   </m:apply>
  65 </xsl:template>
  66
  67 <xsl:template match="applyEquality">
  68   <m:apply>
  69     <m:ci>applyEquality</m:ci>
  70     <xsl:apply-templates/>
  71   </m:apply>
  72 </xsl:template>
  73
  74 <xsl:template match="independent_functionElimination">
  75   <m:apply>
  76     <m:ci>independent_functionElimination</m:ci>
  77     <m:cn>
  78       <xsl:value-of select="@number_hyp"/>
  79     </m:cn>
  80     <xsl:apply-templates/>
  81   </m:apply>
  82 </xsl:template>
  83
  84 <xsl:template match="dependent_functionElimination">
  85   <m:apply>
  86     <m:ci>dependent_functionElimination</m:ci>
  87     <m:cn>
  88       <xsl:value-of select="@number_hyp"/>
  89     </m:cn>
  90     <xsl:apply-templates/>
  91   </m:apply>
  92 </xsl:template>
  93
  94 <xsl:template match="applyReduce">
  95   <m:ci>functionEquality</m:ci>
  96 </xsl:template>
  97
  98 <xsl:template match="functionExtensionality">
  99   <m:apply>
 100     <m:ci>functionExtensionality</m:ci>
 101     <xsl:apply-templates/>
 102   </m:apply>
 103 </xsl:template>
 104
 105 <xsl:template match="dependent_productFormation">
 106   <m:apply>
 107     <m:ci>dependent_productFormation</m:ci>
 108     <xsl:apply-templates/>
 109   </m:apply>
 110 </xsl:template>
 111
 112 <xsl:template match="independent_productFormation">
 113   <m:ci>independent_productFormation</m:ci>
 114 </xsl:template>
 115
 116 <xsl:template match="productEquality">
 117   <m:apply>
 118     <m:ci>productEquality</m:ci>
 119     <xsl:apply-templates/>
 120   </m:apply>
 121 </xsl:template>
 122
 123 <xsl:template match="independent_productEquality">
 124   <m:ci>independent_productEquality</m:ci>
 125 </xsl:template>
 126
 127 <xsl:template match="dependent_pairEquality">
 128   <m:apply>
 129     <m:ci>dependent_pairEquality</m:ci>
 130     <xsl:apply-templates/>
 131   </m:apply>
 132 </xsl:template>
 133
 134 <xsl:template match="dependent_pairFormation">
 135   <m:apply>
 136     <m:ci>dependent_pairFormation</m:ci>
 137     <xsl:apply-templates/>
 138   </m:apply>
 139 </xsl:template>
 140
 141 <xsl:template match="independent_pairEquality">
 142   <m:ci>independent_pairEquality</m:ci>
 143 </xsl:template>
 144
 145 <xsl:template match="independent_pairFormation">
 146   <m:ci>independent_pairFormation</m:ci>
 147 </xsl:template>
 148
 149 <xsl:template match="spreadEquality">
 150   <m:apply>
 151     <m:ci>spreadEquality</m:ci>
 152     <m:cn>
 153       <xsl:value-of select="@number_hyp"/>
 154     </m:cn>
 155     <xsl:apply-templates/>
 156   </m:apply>
 157 </xsl:template>
 158
 159 <xsl:template match="productElimination">
 160   <m:apply>
 161     <m:ci>productElimination</m:ci>
 162     <xsl:apply-templates/>
 163   </m:apply>
 164 </xsl:template>
 165
 166 <xsl:template match="spreadReduce">
 167   <m:ci>spreadReduce</m:ci>
 168 </xsl:template>
 169
 170 <xsl:template match="unionFormation">
 171   <m:ci>unionFormation</m:ci>
 172 </xsl:template>
 173
 174 <xsl:template match="unionEquality">
 175   <m:ci>unionEquality</m:ci>
 176 </xsl:template>
 177
 178 <xsl:template match="inlEquality">
 179   <m:apply>
 180     <m:ci>inlEquality</m:ci>
 181     <xsl:apply-templates/>
 182   </m:apply>
 183 </xsl:template>
 184
 185 <xsl:template match="inlFormation">
 186   <m:apply>
 187     <m:ci>inlFormation</m:ci>
 188     <xsl:apply-templates/>
 189   </m:apply>
 190 </xsl:template>
 191
 192 <xsl:template match="inrEquality">
 193   <m:apply>
 194     <m:ci>inrEquality</m:ci>
 195     <xsl:apply-templates/>
 196   </m:apply>
 197 </xsl:template>
 198
 199 <xsl:template match="inrFormation">
 200   <m:apply>
 201     <m:ci>inrFormation</m:ci>
 202     <xsl:apply-templates/>
 203   </m:apply>
 204 </xsl:template>
 205
 206 <xsl:template match="decideEquality">
 207   <m:apply>
 208     <m:ci>decideEquality</m:ci>
 209     <xsl:apply-templates/>
 210   </m:apply>
 211 </xsl:template>
 212
 213 <xsl:template match="unionElimination">
 214   <m:apply>
 215     <m:ci>unionElimination</m:ci>
 216     <m:cn>
 217       <xsl:value-of select="@number_hyp"/>
 218     </m:cn>
 219     <xsl:apply-templates/>
 220   </m:apply>
 221 </xsl:template>
 222
 223 <xsl:template match="decideReduceLeft">
 224   <m:ci>decideReduceLeft</m:ci>
 225 </xsl:template>
 226
 227 <xsl:template match="decideReduceRight">
 228   <m:ci>decideReduceRight</m:ci>
 229 </xsl:template>
 230
 231 <xsl:template match="universeFormation">
 232   <m:apply>
 233     <m:ci>universeFormation</m:ci>
 234     <xsl:apply-templates/>
 235   </m:apply>
 236 </xsl:template>
 237
 238 <xsl:template match="universeEquality">
 239   <m:ci>universeEquality</m:ci>
 240 </xsl:template>
 241
 242 <xsl:template match="cumulativity">
 243   <m:apply>
 244     <m:ci>cumulativity</m:ci>
 245     <xsl:apply-templates/>
 246   </m:apply>
 247 </xsl:template>
 248
 249 <xsl:template match="equalityFormation">
 250   <m:apply>
 251     <m:ci>equalityFormation</m:ci>
 252     <xsl:apply-templates/>
 253   </m:apply>
 254 </xsl:template>
 255
 256 <xsl:template match="equalityEquality">
 257   <m:ci>equalityEquality</m:ci>
 258 </xsl:template>
 259
 260 <xsl:template match="axiomEquality">
 261   <m:ci>axiomEquality</m:ci>
 262 </xsl:template>
 263
 264 <xsl:template match="equalityElimination">
 265   <m:apply>
 266     <m:ci>equalityElimination</m:ci>
 267     <m:cn>
 268       <xsl:value-of select="@number_hyp"/>
 269     </m:cn>
 270   </m:apply>
 271 </xsl:template>
 272
 273 <xsl:template match="hypothesisEquality">
 274   <m:apply>
 275     <m:ci>hypothesisEquality</m:ci>
 276     <m:cn>
 277       <xsl:value-of select="@number_hyp"/>
 278     </m:cn>
 279   </m:apply>
 280 </xsl:template>
 281
 282 <xsl:template match="substitution">
 283   <m:apply>
 284     <m:ci>substitution</m:ci>
 285     <xsl:apply-templates/>
 286   </m:apply>
 287 </xsl:template>
 288
 289 <xsl:template match="equality">
 290   <m:ci>equality</m:ci>
 291 </xsl:template>
 292
 293 <xsl:template match="voidFormation">
 294   <m:ci>voidFormation</m:ci>
 295 </xsl:template>
 296
 297 <xsl:template match="voidEquality">
 298   <m:ci>voidEquality</m:ci>
 299 </xsl:template>
 300
 301 <xsl:template match="anyEquality">
 302   <m:ci>anyEquality</m:ci>
 303 </xsl:template>
 304
 305 <xsl:template match="voidElimination">
 306   <m:apply>
 307     <m:ci>voidElimination</m:ci>
 308     <m:cn>
 309       <xsl:value-of select="@number_hyp"/>
 310     </m:cn>
 311   </m:apply>
 312 </xsl:template>
 313
 314 <xsl:template match="atomFormation">
 315   <m:ci>atomFormation</m:ci>
 316 </xsl:template>
 317
 318 <xsl:template match="atomEquality">
 319   <m:ci>atomEquality</m:ci>
 320 </xsl:template>
 321
 322 <xsl:template match="tokenEquality">
 323   <m:ci>tokenEquality</m:ci>
 324 </xsl:template>
 325
 326 <xsl:template match="tokenFormation">
 327   <m:apply>
 328     <m:ci>tokenFormation</m:ci>
 329     <xsl:apply-templates/>
 330   </m:apply>
 331 </xsl:template>
 332
 333 <xsl:template match="atom_eqEquality">
 334   <m:apply>
 335     <m:ci>atom_eqEquality</m:ci>
 336     <xsl:apply-templates/>
 337   </m:apply>
 338 </xsl:template>
 339
 340 <xsl:template match="atom_eqReduceTrue">
 341   <m:apply>
 342     <m:ci>atom_eqReduceTrue</m:ci>
 343     <xsl:apply-templates/>
 344   </m:apply>
 345 </xsl:template>
 346
 347 <xsl:template match="atom_eqReduceFalse">
 348   <m:ci>atom_eqReduceFalse</m:ci>
 349 </xsl:template>
 350
 351 <xsl:template match="intFormation">
 352   <m:ci>intFormation</m:ci>
 353 </xsl:template>
 354
 355 <xsl:template match="intEquality">
 356   <m:ci>intEquality</m:ci>
 357 </xsl:template>
 358
 359 <xsl:template match="natural_numberEquality">
 360   <m:ci>natural_numberEquality</m:ci>
 361 </xsl:template>
 362
 363 <xsl:template match="minusEquality">
 364   <m:ci>minusEquality</m:ci>
 365 </xsl:template>
 366
 367 <xsl:template match="addEquality">
 368   <m:ci>addEquality</m:ci>
 369 </xsl:template>
 370
 371 <xsl:template match="subtractEquality">
 372   <m:ci>subtractEquality</m:ci>
 373 </xsl:template>
 374
 375 <xsl:template match="multiplyEquality">
 376   <m:ci>multiplyEquality</m:ci>
 377 </xsl:template>
 378
 379 <xsl:template match="divideFormation">
 380   <m:ci>divideFormation</m:ci>
 381 </xsl:template>
 382
 383 <xsl:template match="addEquality">
 384   <m:ci>addEquality</m:ci>
 385 </xsl:template>
 386
 387 <xsl:template match="subtractEquality">
 388   <m:ci>subtractEquality</m:ci>
 389 </xsl:template>
 390
 391 <xsl:template match="multiplyEquality">
 392   <m:ci>multiplyEquality</m:ci>
 393 </xsl:template>
 394
 395 <xsl:template match="divideEquality">
 396   <m:ci>divideEquality</m:ci>
 397 </xsl:template>
 398
 399 <xsl:template match="remainderBounds1">
 400   <m:ci>remainderBounds1</m:ci>
 401 </xsl:template>
 402
 403 <xsl:template match="remainderBounds2">
 404   <m:ci>remainderBounds2</m:ci>
 405 </xsl:template>
 406
 407 <xsl:template match="remainderBounds3">
 408   <m:ci>remainderBounds3</m:ci>
 409 </xsl:template>
 410
 411 <xsl:template match="remainderBounds4">
 412   <m:ci>remainderBounds4</m:ci>
 413 </xsl:template>
 414
 415 <xsl:template match="divideRemainderSum">
 416   <m:ci>divideRemainderSum</m:ci>
 417 </xsl:template>
 418
 419 <xsl:template match="arith">
 420   <m:apply>
 421     <m:ci>arith</m:ci>
 422     <xsl:apply-templates/>
 423   </m:apply>
 424 </xsl:template>
 425
 426 <xsl:template match="indEquality">
 427   <m:apply>
 428     <m:ci>indEquality</m:ci>
 429     <xsl:apply-templates/>
 430   </m:apply>
 431 </xsl:template>
 432
 433 <xsl:template match="intElimination">
 434   <m:apply>
 435     <m:ci>intElimination</m:ci>
 436     <m:cn>
 437       <xsl:value-of select="@number_hyp"/>
 438     </m:cn>
 439     <xsl:apply-templates/>
 440   </m:apply>
 441 </xsl:template>
 442
 443 <xsl:template match="indReduceDown">
 444   <m:ci>indReduceDown</m:ci>
 445 </xsl:template>
 446
 447 <xsl:template match="indReduceUp">
 448   <m:ci>indReduceUp</m:ci>
 449 </xsl:template>
 450
 451 <xsl:template match="indReduceBase">
 452   <m:ci>indReduceBase</m:ci>
 453 </xsl:template>
 454
 455 <xsl:template match="ind_eqEquality">
 456   <m:ci>ind_eqEquality</m:ci>
 457 </xsl:template>
 458
 459 <xsl:template match="ind_eqReduceTrue">
 460   <m:ci>ind_eqReduceTrue</m:ci>
 461 </xsl:template>
 462
 463 <xsl:template match="ind_eqReduceFalse">
 464   <m:ci>ind_eqReduceFalse</m:ci>
 465 </xsl:template>
 466
 467 <xsl:template match="lessEquality">
 468   <m:ci>lessEquality</m:ci>
 469 </xsl:template>
 470
 471 <xsl:template match="lessReduceTrue">
 472   <m:ci>lessReduceTrue</m:ci>
 473 </xsl:template>
 474
 475 <xsl:template match="lessReduceFalse">
 476   <m:ci>lessReduceFalse</m:ci>
 477 </xsl:template>
 478
 479 <xsl:template match="less_thanEquality">
 480   <m:ci>less_thanEquality</m:ci>
 481 </xsl:template>
 482
 483 <xsl:template match="less_thanFormation">
 484   <m:ci>less_thanFormation</m:ci>
 485 </xsl:template>
 486
 487 <xsl:template match="less_thanMember">
 488   <m:ci>less_thanMember</m:ci>
 489 </xsl:template>
 490
 491 <xsl:template match="listFormation">
 492   <m:ci>listFormation</m:ci>
 493 </xsl:template>
 494
 495 <xsl:template match="listEquality">
 496   <m:ci>listEquality</m:ci>
 497 </xsl:template>
 498
 499 <xsl:template match="nilEquality">
 500   <m:apply>
 501     <m:ci>nilEquality</m:ci>
 502     <xsl:apply-templates/>
 503   </m:apply>
 504 </xsl:template>
 505
 506 <xsl:template match="nilFormation">
 507   <m:apply>
 508     <m:ci>nilFormation</m:ci>
 509     <xsl:apply-templates/>
 510   </m:apply>
 511 </xsl:template>
 512
 513 <xsl:template match="consFormation">
 514   <m:ci>consFormation</m:ci>
 515 </xsl:template>
 516
 517 <xsl:template match="consEquality">
 518   <m:ci>consEquality</m:ci>
 519 </xsl:template>
 520
 521 <xsl:template match="list_indEquality">
 522   <m:apply>
 523     <m:ci>list_indEquality</m:ci>
 524     <xsl:apply-templates/>
 525   </m:apply>
 526 </xsl:template>
 527
 528 <xsl:template match="listElimination">
 529   <m:apply>
 530     <m:ci>listElimination</m:ci>
 531     <m:cn>
 532       <xsl:value-of select="@number_hyp"/>
 533     </m:cn>
 534     <xsl:apply-templates/>
 535   </m:apply>
 536 </xsl:template>
 537
 538 <xsl:template match="list_indReduceUp">
 539   <m:ci>list_indReduceUp</m:ci>
 540 </xsl:template>
 541
 542 <xsl:template match="list_indReduceBase">
 543   <m:ci>list_indReduceBase</m:ci>
 544 </xsl:template>
 545
 546 <xsl:template match="recEquality">
 547   <m:apply>
 548     <m:ci>recEquality</m:ci>
 549     <xsl:apply-templates/>
 550   </m:apply>
 551 </xsl:template>
 552
 553 <xsl:template match="rec_memberEquality">
 554   <m:apply>
 555     <m:ci>rec_memberEquality</m:ci>
 556     <xsl:apply-templates/>
 557   </m:apply>
 558 </xsl:template>
 559
 560 <xsl:template match="rec_memberFormation">
 561   <m:apply>
 562     <m:ci>rec_memberFormation</m:ci>
 563     <xsl:apply-templates/>
 564   </m:apply>
 565 </xsl:template>
 566
 567 <xsl:template match="rec_indEquality">
 568   <m:apply>
 569     <m:ci>rec_indEquality</m:ci>
 570     <xsl:apply-templates/>
 571   </m:apply>
 572 </xsl:template>
 573
 574 <xsl:template match="recElimination">
 575   <m:apply>
 576     <m:ci>recElimination</m:ci>
 577     <m:cn>
 578       <xsl:value-of select="@number_hyp"/>
 579     </m:cn>
 580     <xsl:apply-templates/>
 581   </m:apply>
 582 </xsl:template>
 583
 584 <xsl:template match="recUnrollElimination">
 585   <m:apply>
 586     <m:ci>recUnrollElimination</m:ci>
 587     <m:cn>
 588       <xsl:value-of select="@number_hyp"/>
 589     </m:cn>
 590     <xsl:apply-templates/>
 591   </m:apply>
 592 </xsl:template>
 593
 594 <xsl:template match="dependent_setFormation">
 595   <m:apply>
 596     <m:ci>dependent_setFormation</m:ci>
 597     <xsl:apply-templates/>
 598   </m:apply>
 599 </xsl:template>
 600
 601 <xsl:template match="independent_setFormation">
 602   <m:ci>independent_setFormation</m:ci>
 603 </xsl:template>
 604
 605 <xsl:template match="setEquality">
 606   <m:apply>
 607     <m:ci>setEquality</m:ci>
 608     <xsl:apply-templates/>
 609   </m:apply>
 610 </xsl:template>
 611
 612 <xsl:template match="dependent_set_memberEquality">
 613   <m:apply>
 614     <m:ci>dependent_set_memberEquality</m:ci>
 615     <xsl:apply-templates/>
 616   </m:apply>
 617 </xsl:template>
 618
 619 <xsl:template match="dependent_set_memberFormation">
 620   <m:apply>
 621     <m:ci>dependent_set_memberFormation</m:ci>
 622     <xsl:apply-templates/>
 623   </m:apply>
 624 </xsl:template>
 625
 626 <xsl:template match="independent_set_memberEquality">
 627   <m:ci>independent_set_memberEquality</m:ci>
 628 </xsl:template>
 629
 630 <xsl:template match="independent_set_memberFormation">
 631   <m:apply>
 632     <m:ci>independent_set_memberFormation</m:ci>
 633     <xsl:apply-templates/>
 634   </m:apply>
 635 </xsl:template>
 636
 637 <xsl:template match="setElimination">
 638   <m:apply>
 639     <m:ci>setElimination</m:ci>
 640     <m:cn>
 641       <xsl:value-of select="@number_hyp"/>
 642     </m:cn>
 643     <xsl:apply-templates/>
 644   </m:apply>
 645 </xsl:template>
 646
 647 <xsl:template match="isectFormation">
 648   <m:apply>
 649     <m:ci>isectFormation</m:ci>
 650     <xsl:apply-templates/>
 651   </m:apply>
 652 </xsl:template>
 653
 654 <xsl:template match="isectEquality">
 655   <m:apply>
 656     <m:ci>isectEquality</m:ci>
 657     <xsl:apply-templates/>
 658   </m:apply>
 659 </xsl:template>
 660
 661 <xsl:template match="isect_memberEquality">
 662   <m:apply>
 663     <m:ci>isect_memberEquality</m:ci>
 664     <xsl:apply-templates/>
 665   </m:apply>
 666 </xsl:template>
 667
 668 <xsl:template match="isect_memberFormation">
 669   <m:apply>
 670     <m:ci>isect_memberFormation</m:ci>
 671     <xsl:apply-templates/>
 672   </m:apply>
 673 </xsl:template>
 674
 675 <xsl:template match="isect_member_caseEquality">
 676   <m:apply>
 677     <m:ci>isect_member_caseEquality</m:ci>
 678     <xsl:apply-templates/>
 679   </m:apply>
 680 </xsl:template>
 681
 682 <xsl:template match="isectElimination">
 683   <m:apply>
 684     <m:ci>isectElimination</m:ci>
 685     <m:cn>
 686       <xsl:value-of select="@number_hyp"/>
 687     </m:cn>
 688     <xsl:apply-templates/>
 689   </m:apply>
 690 </xsl:template>
 691
 692 <xsl:template match="quotientFormation">
 693   <m:apply>
 694     <m:ci>quotientFormation</m:ci>
 695     <xsl:apply-templates/>
 696   </m:apply>
 697 </xsl:template>
 698
 699 <xsl:template match="quotientWeakEquality">
 700   <m:apply>
 701     <m:ci>quotientWeakEquality</m:ci>
 702     <xsl:apply-templates/>
 703   </m:apply>
 704 </xsl:template>
 705
 706 <xsl:template match="quotientEquality">
 707   <m:ci>quotientEquality</m:ci>
 708 </xsl:template>
 709
 710 <xsl:template match="quotient_memberWeakEquality">
 711   <m:apply>
 712     <m:ci>quotient_memberWeakEquality</m:ci>
 713     <xsl:apply-templates/>
 714   </m:apply>
 715 </xsl:template>
 716
 717 <xsl:template match="quotient_memberFormation">
 718   <m:apply>
 719     <m:ci>quotient_memberFormation</m:ci>
 720     <xsl:apply-templates/>
 721   </m:apply>
 722 </xsl:template>
 723
 724 <xsl:template match="quotient_memberEquality">
 725   <m:apply>
 726     <m:ci>quotient_memberEquality</m:ci>
 727     <xsl:apply-templates/>
 728   </m:apply>
 729 </xsl:template>
 730
 731 <xsl:template match="quotient_equalityElimination">
 732   <m:apply>
 733     <m:ci>quotient_equalityElimination</m:ci>
 734     <m:cn>
 735       <xsl:value-of select="@number_hyp"/>
 736     </m:cn>
 737     <xsl:apply-templates/>
 738   </m:apply>
 739 </xsl:template>
 740
 741 <xsl:template match="quotientElimination">
 742   <m:apply>
 743     <m:ci>quotientElimination</m:ci>
 744     <m:cn>
 745       <xsl:value-of select="@number_hyp"/>
 746     </m:cn>
 747     <xsl:apply-templates/>
 748   </m:apply>
 749 </xsl:template>
 750
 751 <xsl:template match="quotientElimination_2">
 752   <m:apply>
 753     <m:ci>quotientElimination_2</m:ci>
 754     <m:cn>
 755       <xsl:value-of select="@number_hyp"/>
 756     </m:cn>
 757     <xsl:apply-templates/>
 758   </m:apply>
 759 </xsl:template>
 760
 761 <xsl:template match="direct_computation">
 762   <m:apply>
 763     <m:ci>direct_computation</m:ci>
 764     <xsl:apply-templates/>
 765   </m:apply>
 766 </xsl:template>
 767
 768 <xsl:template match="reverse_direct_computation">
 769   <m:apply>
 770     <m:ci>reverse_direct_computation</m:ci>
 771     <xsl:apply-templates/>
 772   </m:apply>
 773 </xsl:template>
 774
 775 <xsl:template match="direct_computation_hypothesis">
 776   <m:apply>
 777     <m:ci>direct_computation_hypothesis</m:ci>
 778     <m:cn>
 779       <xsl:value-of select="@number_hyp"/>
 780     </m:cn>
 781     <xsl:apply-templates/>
 782   </m:apply>
 783 </xsl:template>
 784
 785 <xsl:template match="reverse_direct_computation_hypothesis">
 786   <m:apply>
 787     <m:ci>reverse_direct_computation_hypothesis</m:ci>
 788     <m:cn>
 789       <xsl:value-of select="@number_hyp"/>
 790     </m:cn>
 791     <xsl:apply-templates/>
 792   </m:apply>
 793 </xsl:template>
 794
 795 <xsl:template match="ruleinstance/hypothesis">
 796   <m:apply>
 797     <m:ci>hypothesis</m:ci>
 798     <m:cn>
 799       <xsl:value-of select="@number_hyp"/>
 800     </m:cn>
 801   </m:apply>
 802 </xsl:template>
 803
 804 <xsl:template match="thin">
 805   <m:apply>
 806     <m:ci>thin</m:ci>
 807     <m:cn>
 808       <xsl:value-of select="@number_hyp"/>
 809     </m:cn>
 810   </m:apply>
 811 </xsl:template>
 812
 813 <xsl:template match="cut">
 814   <m:apply>
 815     <m:ci>cut</m:ci>
 816     <m:cn>
 817       <xsl:value-of select="@number_hyp"/>
 818     </m:cn>
 819     <xsl:apply-templates/>
 820   </m:apply>
 821 </xsl:template>
 822
 823 <xsl:template match="hyp_replacement">
 824   <m:apply>
 825     <m:ci>hyp_replacement</m:ci>
 826     <m:cn>
 827       <xsl:value-of select="@number_hyp"/>
 828     </m:cn>
 829     <xsl:apply-templates/>
 830   </m:apply>
 831 </xsl:template>
 832
 833 <xsl:template match="lemma">
 834   <m:apply>
 835     <m:ci>lemma</m:ci>
 836     <m:ci>
 837       <xsl:value-of select="@name"/>
 838     </m:ci>
 839   </m:apply>
 840 </xsl:template>
 841
 842 <xsl:template match="extract">
 843   <m:apply>
 844     <m:ci>extract</m:ci>
 845     <m:ci>
 846       <xsl:value-of select="@name"/>
 847     </m:ci>
 848   </m:apply>
 849 </xsl:template>
 850
 851 <xsl:template match="instantiate">
 852   <m:apply>
 853     <m:ci>instantiate</m:ci>
 854     <xsl:apply-templates/>
 855   </m:apply>
 856 </xsl:template>
 857
 858 <xsl:template match="because">
 859   <m:ci>because</m:ci>
 860 </xsl:template>
 861
 862 <xsl:template match="rename">
 863   <m:apply>
 864     <m:ci>rename</m:ci>
 865     <xsl:apply-templates/>
 866   </m:apply>
 867 </xsl:template>
 868
 869 <xsl:template match="introduction">
 870   <m:apply>
 871     <m:ci>introducition</m:ci>
 872     <xsl:apply-templates/>
 873   </m:apply>
 874 </xsl:template>
 875
 876 </xsl:stylesheet>