]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk_gtkmathview/lablgtk-20001129_gtkmathview-0.2.1/minidom/test.xml
Initial revision
[helm.git] / helm / DEVEL / lablgtk_gtkmathview / lablgtk-20001129_gtkmathview-0.2.1 / minidom / 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>