helm/DEVEL/mlminidom/test.xml

   1 <?xml version="1.0" encoding="iso-8859-1"?>
   2 <?cocoon-format type="text/xhtml"?>
   3 <m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
   4     <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
   5         <m:mtr>
   6             <m:mtd>
   7                 <m:mrow>
   8                     <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
   9                 </m:mrow>
  10             </m:mtd>
  11         </m:mtr>
  12         <m:mtr>
  13             <m:mtd>
  14                 <m:mrow>
  15                     <m:mphantom>
  16                         <m:mtext>__</m:mtext>
  17                     </m:mphantom>
  18                     <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
  19                         <m:mrow helm:xref="i22">
  20                             <m:mtable columnalign="left" equalrows="false" align="baseline 1">
  21                                 <m:mtr>
  22                                     <m:mtd>
  23                                         <m:mrow>
  24                                             <m:mo stretchy="false">(</m:mo>
  25                                             <m:mrow helm:xref="i23">
  26                                                 <m:mtable columnalign="left" equalrows="false" align="baseline 1">
  27                                                     <m:mtr>
  28                                                         <m:mtd>
  29                                                             <m:mo color="Blue">&#928;</m:mo>
  30                                                             <m:mi>A</m:mi>
  31                                                             <m:mo>:</m:mo>
  32                                                             <m:mrow helm:xref="i24">
  33                                                                 <m:mo>Prop</m:mo>
  34                                                             </m:mrow>
  35                                                         </m:mtd>
  36                                                     </m:mtr>
  37                                                     <m:mtr>
  38                                                         <m:mtd>
  39                                                             <m:mrow>
  40                                                                 <m:mo>.</m:mo>
  41                                                                 <m:mrow helm:xref="i25">
  42                                                                     <m:mtable columnalign="left" equalrows="false" align="baseline 1">
  43                                                                         <m:mtr>
  44                                                                             <m:mtd>
  45                                                                                 <m:mo color="Blue">&#928;</m:mo>
  46                                                                                 <m:mi>B</m:mi>
  47                                                                                 <m:mo>:</m:mo>
  48                                                                                 <m:mrow helm:xref="i26">
  49                                                                                     <m:mo>Prop</m:mo>
  50                                                                                 </m:mrow>
  51                                                                             </m:mtd>
  52                                                                         </m:mtr>
  53                                                                         <m:mtr>
  54                                                                             <m:mtd>
  55                                                                                 <m:mrow>
  56                                                                                     <m:mo>.</m:mo>
  57                                                                                     <m:mrow helm:xref="i27">
  58                                                                                         <m:mtable columnalign="left" equalrows="false" align="baseline 1">
  59                                                                                             <m:mtr>
  60                                                                                                 <m:mtd>
  61                                                                                                     <m:mo color="Blue">&#928;</m:mo>
  62                                                                                                     <m:mi>P</m:mi>
  63                                                                                                     <m:mo>:</m:mo>
  64                                                                                                     <m:mrow helm:xref="i28">
  65                                                                                                         <m:mo>Prop</m:mo>
  66                                                                                                     </m:mrow>
  67                                                                                                 </m:mtd>
  68                                                                                             </m:mtr>
  69                                                                                             <m:mtr>
  70                                                                                                 <m:mtd>
  71                                                                                                     <m:mrow>
  72                                                                                                         <m:mo>.</m:mo>
  73                                                                                                         <m:mrow helm:xref="i29">
  74                                                                                                             <m:mtable columnalign="left" equalrows="false" align="baseline 1">
  75                                                                                                                 <m:mtr>
  76                                                                                                                     <m:mtd>
  77                                                                                                                         <m:mo color="Blue">&#928;</m:mo>
  78                                                                                                                         <m:mi>f</m:mi>
  79                                                                                                                         <m:mo>:</m:mo>
  80                                                                                                                         <m:mrow helm:xref="i30">
  81                                                                                                                             <m:mo stretchy="false">(</m:mo>
  82                                                                                                                             <m:mi helm:xref="i31">A</m:mi>
  83                                                                                                                             <m:mo color="Blue">&#8594;</m:mo>
  84                                                                                                                             <m:mrow helm:xref="i32">
  85                                                                                                                                 <m:mo stretchy="false">(</m:mo>
  86                                                                                                                                 <m:mi helm:xref="i33">B</m:mi>
  87                                                                                                                                 <m:mo color="Blue">&#8594;</m:mo>
  88                                                                                                                                 <m:mi helm:xref="i34">P</m:mi>
  89                                                                                                                                 <m:mo stretchy="false">)</m:mo>
  90                                                                                                                             </m:mrow>
  91                                                                                                                             <m:mo stretchy="false">)</m:mo>
  92                                                                                                                         </m:mrow>
  93                                                                                                                     </m:mtd>
  94                                                                                                                 </m:mtr>
  95                                                                                                                 <m:mtr>
  96                                                                                                                     <m:mtd>
  97                                                                                                                         <m:mrow>
  98                                                                                                                             <m:mo>.</m:mo>
  99                                                                                                                             <m:mrow helm:xref="i35">
 100                                                                                                                                 <m:mo color="Blue">&#928;</m:mo>
 101                                                                                                                                 <m:mi>a</m:mi>
 102                                                                                                                                 <m:mo>:</m:mo>
 103                                                                                                                                 <m:mrow helm:xref="i36">
 104                                                                                                                                     <m:mo stretchy="false">(</m:mo>
 105                                                                                                                                     <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
 106                                                                                                                                     <m:mphantom>
 107                                                                                                                                         <m:mtext>_</m:mtext>
 108                                                                                                                                     </m:mphantom>
 109                                                                                                                                     <m:mi helm:xref="i38">A</m:mi>
 110                                                                                                                                     <m:mphantom>
 111                                                                                                                                         <m:mtext>_</m:mtext>
 112                                                                                                                                     </m:mphantom>
 113                                                                                                                                     <m:mi helm:xref="i39">B</m:mi>
 114                                                                                                                                     <m:mo stretchy="false">)</m:mo>
 115                                                                                                                                 </m:mrow>
 116                                                                                                                                 <m:mo>.</m:mo>
 117                                                                                                                                 <m:mi helm:xref="i40">P</m:mi>
 118                                                                                                                             </m:mrow>
 119                                                                                                                         </m:mrow>
 120                                                                                                                     </m:mtd>
 121                                                                                                                 </m:mtr>
 122                                                                                                             </m:mtable>
 123                                                                                                         </m:mrow>
 124                                                                                                     </m:mrow>
 125                                                                                                 </m:mtd>
 126                                                                                             </m:mtr>
 127                                                                                         </m:mtable>
 128                                                                                     </m:mrow>
 129                                                                                 </m:mrow>
 130                                                                             </m:mtd>
 131                                                                         </m:mtr>
 132                                                                     </m:mtable>
 133                                                                 </m:mrow>
 134                                                             </m:mrow>
 135                                                         </m:mtd>
 136                                                     </m:mtr>
 137                                                 </m:mtable>
 138                                             </m:mrow>
 139                                         </m:mrow>
 140                                     </m:mtd>
 141                                 </m:mtr>
 142                                 <m:mtr>
 143                                     <m:mtd>
 144                                         <m:mrow>
 145                                             <m:mo color="#b03060">:&gt;</m:mo>
 146                                             <m:mrow helm:xref="i41">
 147                                                 <m:mo>Prop</m:mo>
 148                                             </m:mrow>
 149                                         </m:mrow>
 150                                     </m:mtd>
 151                                 </m:mtr>
 152                                 <m:mtr>
 153                                     <m:mtd>
 154                                         <m:mrow>
 155                                             <m:mo stretchy="false">)</m:mo>
 156                                         </m:mrow>
 157                                     </m:mtd>
 158                                 </m:mtr>
 159                             </m:mtable>
 160                         </m:mrow>
 161                         <m:annotation-xml encoding="MathML">
 162                             <m:apply helm:xref="i22">
 163                                 <m:csymbol>cast</m:csymbol>
 164                                 <m:apply helm:xref="i23">
 165                                     <m:csymbol>prod</m:csymbol>
 166                                     <m:bvar>
 167                                         <m:ci>A</m:ci>
 168                                         <m:type>
 169                                             <m:apply helm:xref="i24">
 170                                                 <m:csymbol>Prop</m:csymbol>
 171                                             </m:apply>
 172                                         </m:type>
 173                                     </m:bvar>
 174                                     <m:apply helm:xref="i25">
 175                                         <m:csymbol>prod</m:csymbol>
 176                                         <m:bvar>
 177                                             <m:ci>B</m:ci>
 178                                             <m:type>
 179                                                 <m:apply helm:xref="i26">
 180                                                     <m:csymbol>Prop</m:csymbol>
 181                                                 </m:apply>
 182                                             </m:type>
 183                                         </m:bvar>
 184                                         <m:apply helm:xref="i27">
 185                                             <m:csymbol>prod</m:csymbol>
 186                                             <m:bvar>
 187                                                 <m:ci>P</m:ci>
 188                                                 <m:type>
 189                                                     <m:apply helm:xref="i28">
 190                                                         <m:csymbol>Prop</m:csymbol>
 191                                                     </m:apply>
 192                                                 </m:type>
 193                                             </m:bvar>
 194                                             <m:apply helm:xref="i29">
 195                                                 <m:csymbol>prod</m:csymbol>
 196                                                 <m:bvar>
 197                                                     <m:ci>f</m:ci>
 198                                                     <m:type>
 199                                                         <m:apply helm:xref="i30">
 200                                                             <m:csymbol>arrow</m:csymbol>
 201                                                             <m:ci helm:xref="i31">A</m:ci>
 202                                                             <m:apply helm:xref="i32">
 203                                                                 <m:csymbol>arrow</m:csymbol>
 204                                                                 <m:ci helm:xref="i33">B</m:ci>
 205                                                                 <m:ci helm:xref="i34">P</m:ci>
 206                                                             </m:apply>
 207                                                         </m:apply>
 208                                                     </m:type>
 209                                                 </m:bvar>
 210                                                 <m:apply helm:xref="i35">
 211                                                     <m:csymbol>prod</m:csymbol>
 212                                                     <m:bvar>
 213                                                         <m:ci>a</m:ci>
 214                                                         <m:type>
 215                                                             <m:apply helm:xref="i36">
 216                                                                 <m:csymbol>app</m:csymbol>
 217                                                                 <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
 218                                                                 <m:ci helm:xref="i38">A</m:ci>
 219                                                                 <m:ci helm:xref="i39">B</m:ci>
 220                                                             </m:apply>
 221                                                         </m:type>
 222                                                     </m:bvar>
 223                                                     <m:ci helm:xref="i40">P</m:ci>
 224                                                 </m:apply>
 225                                             </m:apply>
 226                                         </m:apply>
 227                                     </m:apply>
 228                                 </m:apply>
 229                                 <m:apply helm:xref="i41">
 230                                     <m:csymbol>Prop</m:csymbol>
 231                                 </m:apply>
 232                             </m:apply>
 233                         </m:annotation-xml>
 234                     </m:semantics>
 235                 </m:mrow>
 236             </m:mtd>
 237         </m:mtr>
 238         <m:mtr>
 239             <m:mtd>
 240                 <m:mrow>
 241                     <m:mtext>AS</m:mtext>
 242                 </m:mrow>
 243             </m:mtd>
 244         </m:mtr>
 245         <m:mtr>
 246             <m:mtd>
 247                 <m:mrow>
 248                     <m:mphantom>
 249                         <m:mtext>__</m:mtext>
 250                     </m:mphantom>
 251                     <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
 252                         <m:mrow helm:xref="i1">
 253                             <m:mtable columnalign="left" equalrows="false" align="baseline 1">
 254                                 <m:mtr>
 255                                     <m:mtd>
 256                                         <m:mo color="Red">&#955;</m:mo>
 257                                         <m:mi>A</m:mi>
 258                                         <m:mo>:</m:mo>
 259                                         <m:mrow helm:xref="i2">
 260                                             <m:mo>Prop</m:mo>
 261                                         </m:mrow>
 262                                     </m:mtd>
 263                                 </m:mtr>
 264                                 <m:mtr>
 265                                     <m:mtd>
 266                                         <m:mrow>
 267                                             <m:mo>.</m:mo>
 268                                             <m:mrow helm:xref="i3">
 269                                                 <m:mtable columnalign="left" equalrows="false" align="baseline 1">
 270                                                     <m:mtr>
 271                                                         <m:mtd>
 272                                                             <m:mo color="Red">&#955;</m:mo>
 273                                                             <m:mi>B</m:mi>
 274                                                             <m:mo>:</m:mo>
 275                                                             <m:mrow helm:xref="i4">
 276                                                                 <m:mo>Prop</m:mo>
 277                                                             </m:mrow>
 278                                                         </m:mtd>
 279                                                     </m:mtr>
 280                                                     <m:mtr>
 281                                                         <m:mtd>
 282                                                             <m:mrow>
 283                                                                 <m:mo>.</m:mo>
 284                                                                 <m:mrow helm:xref="i5">
 285                                                                     <m:mtable columnalign="left" equalrows="false" align="baseline 1">
 286                                                                         <m:mtr>
 287                                                                             <m:mtd>
 288                                                                                 <m:mo color="Red">&#955;</m:mo>
 289                                                                                 <m:mi>P</m:mi>
 290                                                                                 <m:mo>:</m:mo>
 291                                                                                 <m:mrow helm:xref="i6">
 292                                                                                     <m:mo>Prop</m:mo>
 293                                                                                 </m:mrow>
 294                                                                             </m:mtd>
 295                                                                         </m:mtr>
 296                                                                         <m:mtr>
 297                                                                             <m:mtd>
 298                                                                                 <m:mrow>
 299                                                                                     <m:mo>.</m:mo>
 300                                                                                     <m:mrow helm:xref="i7">
 301                                                                                         <m:mtable columnalign="left" equalrows="false" align="baseline 1">
 302                                                                                             <m:mtr>
 303                                                                                                 <m:mtd>
 304                                                                                                     <m:mo color="Red">&#955;</m:mo>
 305                                                                                                     <m:mi>f</m:mi>
 306                                                                                                     <m:mo>:</m:mo>
 307                                                                                                     <m:mrow helm:xref="i8">
 308                                                                                                         <m:mo stretchy="false">(</m:mo>
 309                                                                                                         <m:mi helm:xref="i9">A</m:mi>
 310                                                                                                         <m:mo color="Blue">&#8594;</m:mo>
 311                                                                                                         <m:mrow helm:xref="i10">
 312                                                                                                             <m:mo stretchy="false">(</m:mo>
 313                                                                                                             <m:mi helm:xref="i11">B</m:mi>
 314                                                                                                             <m:mo color="Blue">&#8594;</m:mo>
 315                                                                                                             <m:mi helm:xref="i12">P</m:mi>
 316                                                                                                             <m:mo stretchy="false">)</m:mo>
 317                                                                                                         </m:mrow>
 318                                                                                                         <m:mo stretchy="false">)</m:mo>
 319                                                                                                     </m:mrow>
 320                                                                                                 </m:mtd>
 321                                                                                             </m:mtr>
 322                                                                                             <m:mtr>
 323                                                                                                 <m:mtd>
 324                                                                                                     <m:mrow>
 325                                                                                                         <m:mo>.</m:mo>
 326                                                                                                         <m:mrow helm:xref="i13">
 327                                                                                                             <m:mtable columnalign="left" equalrows="false" align="baseline 1">
 328                                                                                                                 <m:mtr>
 329                                                                                                                     <m:mtd>
 330                                                                                                                         <m:mo color="Red">&#955;</m:mo>
 331                                                                                                                         <m:mi>a</m:mi>
 332                                                                                                                         <m:mo>:</m:mo>
 333                                                                                                                         <m:mrow helm:xref="i14">
 334                                                                                                                             <m:mo stretchy="false">(</m:mo>
 335                                                                                                                             <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
 336                                                                                                                             <m:mphantom>
 337                                                                                                                                 <m:mtext>_</m:mtext>
 338                                                                                                                             </m:mphantom>
 339                                                                                                                             <m:mi helm:xref="i16">A</m:mi>
 340                                                                                                                             <m:mphantom>
 341                                                                                                                                 <m:mtext>_</m:mtext>
 342                                                                                                                             </m:mphantom>
 343                                                                                                                             <m:mi helm:xref="i17">B</m:mi>
 344                                                                                                                             <m:mo stretchy="false">)</m:mo>
 345                                                                                                                         </m:mrow>
 346                                                                                                                     </m:mtd>
 347                                                                                                                 </m:mtr>
 348                                                                                                                 <m:mtr>
 349                                                                                                                     <m:mtd>
 350                                                                                                                         <m:mrow>
 351                                                                                                                             <m:mo>.</m:mo>
 352                                                                                                                             <m:mrow helm:xref="i18">
 353                                                                                                                                 <m:mo>&lt;</m:mo>
 354                                                                                                                                 <m:mi helm:xref="i19">P</m:mi>
 355                                                                                                                                 <m:mo>&gt;</m:mo>
 356                                                                                                                                 <m:mo>CASES</m:mo>
 357                                                                                                                                 <m:mphantom>
 358                                                                                                                                     <m:mtext>_</m:mtext>
 359                                                                                                                                 </m:mphantom>
 360                                                                                                                                 <m:mi helm:xref="i20">a</m:mi>
 361                                                                                                                                 <m:mphantom>
 362                                                                                                                                     <m:mtext>_</m:mtext>
 363                                                                                                                                 </m:mphantom>
 364                                                                                                                                 <m:mo>OF</m:mo>
 365                                                                                                                                 <m:mrow>
 366                                                                                                                                     <m:mo stretchy="false">(</m:mo>
 367                                                                                                                                     <m:mi>conj</m:mi>
 368                                                                                                                                     <m:mphantom>
 369                                                                                                                                         <m:mtext>_</m:mtext>
 370                                                                                                                                     </m:mphantom>
 371                                                                                                                                     <m:mi>$1</m:mi>
 372                                                                                                                                     <m:mphantom>
 373                                                                                                                                         <m:mtext>_</m:mtext>
 374                                                                                                                                     </m:mphantom>
 375                                                                                                                                     <m:mi>$2</m:mi>
 376                                                                                                                                     <m:mo stretchy="false">)</m:mo>
 377                                                                                                                                 </m:mrow>
 378                                                                                                                                 <m:mo color="Green">&#8658;</m:mo>
 379                                                                                                                                 <m:mrow>
 380                                                                                                                                     <m:mo stretchy="false">(</m:mo>
 381                                                                                                                                     <m:mi helm:xref="i21">f</m:mi>
 382                                                                                                                                     <m:mphantom>
 383                                                                                                                                         <m:mtext>_</m:mtext>
 384                                                                                                                                     </m:mphantom>
 385                                                                                                                                     <m:mi>$1</m:mi>
 386                                                                                                                                     <m:mphantom>
 387                                                                                                                                         <m:mtext>_</m:mtext>
 388                                                                                                                                     </m:mphantom>
 389                                                                                                                                     <m:mi>$2</m:mi>
 390                                                                                                                                     <m:mo stretchy="false">)</m:mo>
 391                                                                                                                                 </m:mrow>
 392                                                                                                                                 <m:mphantom>
 393                                                                                                                                     <m:mtext>_</m:mtext>
 394                                                                                                                                 </m:mphantom>
 395                                                                                                                                 <m:mo>END</m:mo>
 396                                                                                                                             </m:mrow>
 397                                                                                                                         </m:mrow>
 398                                                                                                                     </m:mtd>
 399                                                                                                                 </m:mtr>
 400                                                                                                             </m:mtable>
 401                                                                                                         </m:mrow>
 402                                                                                                     </m:mrow>
 403                                                                                                 </m:mtd>
 404                                                                                             </m:mtr>
 405                                                                                         </m:mtable>
 406                                                                                     </m:mrow>
 407                                                                                 </m:mrow>
 408                                                                             </m:mtd>
 409                                                                         </m:mtr>
 410                                                                     </m:mtable>
 411                                                                 </m:mrow>
 412                                                             </m:mrow>
 413                                                         </m:mtd>
 414                                                     </m:mtr>
 415                                                 </m:mtable>
 416                                             </m:mrow>
 417                                         </m:mrow>
 418                                     </m:mtd>
 419                                 </m:mtr>
 420                             </m:mtable>
 421                         </m:mrow>
 422                         <m:annotation-xml encoding="MathML">
 423                             <m:lambda helm:xref="i1">
 424                                 <m:bvar>
 425                                     <m:ci>A</m:ci>
 426                                     <m:type>
 427                                         <m:apply helm:xref="i2">
 428                                             <m:csymbol>Prop</m:csymbol>
 429                                         </m:apply>
 430                                     </m:type>
 431                                 </m:bvar>
 432                                 <m:lambda helm:xref="i3">
 433                                     <m:bvar>
 434                                         <m:ci>B</m:ci>
 435                                         <m:type>
 436                                             <m:apply helm:xref="i4">
 437                                                 <m:csymbol>Prop</m:csymbol>
 438                                             </m:apply>
 439                                         </m:type>
 440                                     </m:bvar>
 441                                     <m:lambda helm:xref="i5">
 442                                         <m:bvar>
 443                                             <m:ci>P</m:ci>
 444                                             <m:type>
 445                                                 <m:apply helm:xref="i6">
 446                                                     <m:csymbol>Prop</m:csymbol>
 447                                                 </m:apply>
 448                                             </m:type>
 449                                         </m:bvar>
 450                                         <m:lambda helm:xref="i7">
 451                                             <m:bvar>
 452                                                 <m:ci>f</m:ci>
 453                                                 <m:type>
 454                                                     <m:apply helm:xref="i8">
 455                                                         <m:csymbol>arrow</m:csymbol>
 456                                                         <m:ci helm:xref="i9">A</m:ci>
 457                                                         <m:apply helm:xref="i10">
 458                                                             <m:csymbol>arrow</m:csymbol>
 459                                                             <m:ci helm:xref="i11">B</m:ci>
 460                                                             <m:ci helm:xref="i12">P</m:ci>
 461                                                         </m:apply>
 462                                                     </m:apply>
 463                                                 </m:type>
 464                                             </m:bvar>
 465                                             <m:lambda helm:xref="i13">
 466                                                 <m:bvar>
 467                                                     <m:ci>a</m:ci>
 468                                                     <m:type>
 469                                                         <m:apply helm:xref="i14">
 470                                                             <m:csymbol>app</m:csymbol>
 471                                                             <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
 472                                                             <m:ci helm:xref="i16">A</m:ci>
 473                                                             <m:ci helm:xref="i17">B</m:ci>
 474                                                         </m:apply>
 475                                                     </m:type>
 476                                                 </m:bvar>
 477                                                 <m:apply helm:xref="i18">
 478                                                     <m:csymbol>mutcase</m:csymbol>
 479                                                     <m:ci helm:xref="i19">P</m:ci>
 480                                                     <m:ci helm:xref="i20">a</m:ci>
 481                                                     <m:apply>
 482                                                         <m:csymbol>app</m:csymbol>
 483                                                         <m:ci>conj</m:ci>
 484                                                         <m:ci>$1</m:ci>
 485                                                         <m:ci>$2</m:ci>
 486                                                     </m:apply>
 487                                                     <m:apply>
 488                                                         <m:csymbol>app</m:csymbol>
 489                                                         <m:ci helm:xref="i21">f</m:ci>
 490                                                         <m:ci>$1</m:ci>
 491                                                         <m:ci>$2</m:ci>
 492                                                     </m:apply>
 493                                                 </m:apply>
 494                                             </m:lambda>
 495                                         </m:lambda>
 496                                     </m:lambda>
 497                                 </m:lambda>
 498                             </m:lambda>
 499                         </m:annotation-xml>
 500                     </m:semantics>
 501                 </m:mrow>
 502             </m:mtd>
 503         </m:mtr>
 504     </m:mtable>
 505 </m:math>