helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6".
  18
  19 (* INCLUDE
  20 CSemiGroups
  21 *)
  22
  23 (* Remark blz 65 1 *)
  24
  25 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation.con.
  26
  27 (* INCLUDE
  28 Zsetoid
  29 *)
  30
  31 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con.
  32
  33 (* Remark blz 65 2 *)
  34
  35 (* INCLUDE
  36 csetfun
  37 *)
  38
  39 inline cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con.
  40
  41 (* INCLUDE
  42 Nsetoid
  43 *)
  44
  45 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con.
  46
  47 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con.
  48
  49 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con.
  50
  51 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con.
  52
  53 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con.
  54
  55 inline cic:/CoRN/devel/loeb/IDA/Ch6/on.con.
  56
  57 inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con.
  58
  59 (* blz 65 Example 1 *)
  60
  61 (* Print Zopp_is_fun.*)
  62
  63 (* Print Inv_as_un_op.
  64 Geen goed voorbeeld: monoids komen hier al in voor en het is een heel onoverzichtelijk bewijs *)
  65
  66 (* blz 65 Example 2 *)
  67
  68 (* Print plus_is_bin_fun.*)
  69
  70 (* Print mult_as_bin_fun.*)
  71
  72 (* blz 66 Example 1 *)
  73
  74 (* Print plus_is_assoc.*)
  75
  76 (* Print Zplus_is_assoc.*)
  77
  78 (* Print Zmult_is_assoc.*)
  79
  80 (* INCLUDE
  81 Qsetoid
  82 *)
  83
  84 (* Print Qplus_is_assoc.*)
  85
  86 (* Print Qmult_is_assoc.*)
  87
  88 (* blz 66 Examples 2 *)
  89
  90 (* UNEXPORTED
  91 Section p66E2.
  92 *)
  93
  94 inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var.
  95
  96 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var.
  97
  98 inline cic:/CoRN/devel/loeb/IDA/Ch6/g.var.
  99
 100 inline cic:/CoRN/devel/loeb/IDA/Ch6/h.var.
 101
 102 (* Check comp_as_bin_op.*)
 103
 104 (* Check assoc_comp.*)
 105
 106 (* UNEXPORTED
 107 End p66E2.
 108 *)
 109
 110 (* blz 66 Example 2eblok 1 *)
 111
 112 (* INCLUDE
 113 Zsemigroup
 114 *)
 115
 116 inline cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con.
 117
 118 inline cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con.
 119
 120 (* blz 66 Example % 3 *)
 121
 122 inline cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con.
 123
 124 (* blz 66 Example % 4 *)
 125
 126 (* UNEXPORTED
 127 Section p66E2b4.
 128 *)
 129
 130 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
 131
 132 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con.
 133
 134 inline cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con.
 135
 136 inline cic:/CoRN/devel/loeb/IDA/Ch6/app.con.
 137
 138 inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con.
 139
 140 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con.
 141
 142 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con.
 143
 144 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con.
 145
 146 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con.
 147
 148 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con.
 149
 150 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con.
 151
 152 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con.
 153
 154 inline cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con.
 155
 156 inline cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con.
 157
 158 (* INCLUDE
 159 CSemiGroups
 160 *)
 161
 162 inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con.
 163
 164 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con.
 165
 166 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con.
 167
 168 (* UNEXPORTED
 169 End p66E2b4.
 170 *)
 171
 172 (* Definition 5 *)
 173
 174 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con.
 175
 176 (* blz 67 Remark 1 *)
 177
 178 (* INCLUDE
 179 Zmonoid
 180 *)
 181
 182 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con.
 183
 184 (* blz 67 Remark 2 *)
 185
 186 (* UNEXPORTED
 187 Section p67R2.
 188 *)
 189
 190 inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var.
 191
 192 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con.
 193
 194 (* UNEXPORTED
 195 End p67R2.
 196 *)
 197
 198 (* blz 67 Remark 3 *)
 199
 200 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con.
 201
 202 (* Lemma 6 *)
 203
 204 inline cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con.
 205
 206 (* blz 67 Example 1 *)
 207
 208 (* INCLUDE
 209 Nmonoid
 210 *)
 211
 212 (* Print nat_is_CMonoid.*)
 213
 214 (* INCLUDE
 215 Zmonoid
 216 *)
 217
 218 (* Print Z_is_CMonoid.*)
 219
 220 (* Print Z_mul_is_CMonoid.*)
 221
 222 (* blz 67 Example 3 *)
 223
 224 (* Print FS_is_CMonoid.*)
 225
 226 (* blz 68 Example blok1 1 *)
 227
 228 (* UNEXPORTED
 229 Section p68E1b1.
 230 *)
 231
 232 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind.
 233
 234 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con.
 235
 236 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con.
 237
 238 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con.
 239
 240 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con.
 241
 242 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con.
 243
 244 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con.
 245
 246 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con.
 247
 248 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con.
 249
 250 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con.
 251
 252 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con.
 253
 254 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con.
 255
 256 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con.
 257
 258 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con.
 259
 260 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con.
 261
 262 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con.
 263
 264 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con.
 265
 266 (* INCLUDE
 267 CMonoids
 268 *)
 269
 270 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con.
 271
 272 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con.
 273
 274 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con.
 275
 276 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con.
 277
 278 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con.
 279
 280 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con.
 281
 282 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con.
 283
 284 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con.
 285
 286 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con.
 287
 288 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con.
 289
 290 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con.
 291
 292 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con.
 293
 294 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con.
 295
 296 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con.
 297
 298 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con.
 299
 300 inline cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con.
 301
 302 (* UNEXPORTED
 303 End p68E1b1.
 304 *)
 305
 306 (* blz 68 Example blok2 1 *)
 307
 308 (* Print Zplus_is_commut.*)
 309
 310 (* Print Zmult_is_commut. *)
 311
 312 (* Print Qplus_is_commut1. *)
 313
 314 (* Print Qmult_is_commut. *)
 315
 316 (* Definition 9 *)
 317
 318 (* INCLUDE
 319 CMonoids
 320 *)
 321
 322 (* UNEXPORTED
 323 Section D9S.
 324 *)
 325
 326 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
 327
 328 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
 329
 330 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con.
 331
 332 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con.
 333
 334 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con.
 335
 336 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con.
 337
 338 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con.
 339
 340 (* UNEXPORTED
 341 End D9S.
 342 *)
 343
 344 (* UNEXPORTED
 345 Section D9M.
 346 *)
 347
 348 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
 349
 350 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
 351
 352 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con.
 353
 354 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con.
 355
 356 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con.
 357
 358 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con.
 359
 360 (* UNEXPORTED
 361 End D9M.
 362 *)
 363
 364 (* blz 69 Example *)
 365
 366 (* UNEXPORTED
 367 Section p69E1.
 368 *)
 369
 370 inline cic:/CoRN/devel/loeb/IDA/Ch6/PM1M2.con.
 371
 372 inline cic:/CoRN/devel/loeb/IDA/Ch6/uu.con.
 373
 374 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1u.con.
 375
 376 inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con.
 377
 378 (* UNEXPORTED
 379 End p69E1.
 380 *)
 381
 382 (* Theorem 11 *)
 383
 384 (* UNEXPORTED
 385 Section Th11.
 386 *)
 387
 388 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
 389
 390 inline cic:/CoRN/devel/loeb/IDA/Ch6/I.var.
 391
 392 inline cic:/CoRN/devel/loeb/IDA/Ch6/C.var.
 393
 394 inline cic:/CoRN/devel/loeb/IDA/Ch6/Cunit.var.
 395
 396 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_C.var.
 397
 398 inline cic:/CoRN/devel/loeb/IDA/Ch6/K.con.
 399
 400 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con.
 401
 402 inline cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con.
 403
 404 (* UNEXPORTED
 405 End Th11.
 406 *)
 407
 408 (* Theorem 12 *)
 409
 410 (* UNEXPORTED
 411 Section Th12.
 412 *)
 413
 414 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
 415
 416 inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con.
 417
 418 inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con.
 419
 420 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con.
 421
 422 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con.
 423
 424 (* UNEXPORTED
 425 End Th12.
 426 *)
 427
 428 (* blz 70 text *)
 429
 430 (* UNEXPORTED
 431 Section p70text.
 432 *)
 433
 434 (* INCLUDE
 435 lst2fun
 436 *)
 437
 438 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.con.
 439
 440 inline cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con.
 441
 442 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con.
 443
 444 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con.
 445
 446 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con.
 447
 448 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con.
 449
 450 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con.
 451
 452 inline cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con.
 453
 454 (* UNEXPORTED
 455 End p70text.
 456 *)
 457
 458 (* Definition 13 *)
 459
 460 (* UNEXPORTED
 461 Section Th13.
 462 *)
 463
 464 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
 465
 466 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
 467
 468 inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con.
 469
 470 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con.
 471
 472 (* UNEXPORTED
 473 End Th13.
 474 *)
 475
 476 (* blz 71 Example 1 *)
 477
 478 (* UNEXPORTED
 479 Section p71E1.
 480 *)
 481
 482 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
 483
 484 inline cic:/CoRN/devel/loeb/IDA/Ch6/c.var.
 485
 486 inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con.
 487
 488 inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con.
 489
 490 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_generated_by.var.
 491
 492 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con.
 493
 494 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con.
 495
 496 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con.
 497
 498 inline cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con.
 499
 500 (* UNEXPORTED
 501 End p71E1.
 502 *)
 503
 504 (* UNEXPORTED
 505 Section p71E1'.
 506 *)
 507
 508 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con.
 509
 510 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con.
 511
 512 (* UNEXPORTED
 513 End p71E1'.
 514 *)
 515
 516 (* Print to_word_bijective.*)
 517
 518 (* UNEXPORTED
 519 Section p71E2.
 520 *)
 521
 522 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
 523
 524 inline cic:/CoRN/devel/loeb/IDA/Ch6/L.con.
 525
 526 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con.
 527
 528 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con.
 529
 530 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con.
 531
 532 (* UNEXPORTED
 533 End p71E2.
 534 *)
 535
 536 (* blz 71 Remark 1 *)
 537
 538 (* UNEXPORTED
 539 Section p71R1.
 540 *)
 541
 542 inline cic:/CoRN/devel/loeb/IDA/Ch6/S1.var.
 543
 544 inline cic:/CoRN/devel/loeb/IDA/Ch6/S2.var.
 545
 546 inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con.
 547
 548 (* UNEXPORTED
 549 End p71R1.
 550 *)
 551
 552 (* UNEXPORTED
 553 Section p71R2.
 554 *)
 555
 556 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
 557
 558 inline cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con.
 559
 560 (* UNEXPORTED
 561 End p71R2.
 562 *)
 563
 564 (* Theorem 14 *)
 565
 566 (* UNEXPORTED
 567 Section Th14.
 568 *)
 569
 570 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
 571
 572 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
 573
 574 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var.
 575
 576 inline cic:/CoRN/devel/loeb/IDA/Ch6/isof.var.
 577
 578 inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con.
 579
 580 inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con.
 581
 582 (* UNEXPORTED
 583 End Th14.
 584 *)
 585
 586 (* blz 71 Examples 2eblok 1 *)
 587
 588 (* UNEXPORTED
 589 Section p71E2b1.
 590 *)
 591
 592 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con.
 593
 594 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con.
 595
 596 (* UNEXPORTED
 597 End p71E2b1.
 598 *)
 599
 600 (* UNEXPORTED
 601 Section p71E2b2.
 602 *)
 603
 604 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
 605
 606 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
 607
 608 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con.
 609
 610 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con.
 611
 612 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con.
 613
 614 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con.
 615
 616 (* UNEXPORTED
 617 End p71E2b2.
 618 *)
 619
 620 (* UNEXPORTED
 621 Section Th15.
 622 *)
 623
 624 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
 625
 626 inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con.
 627
 628 inline cic:/CoRN/devel/loeb/IDA/Ch6/D.var.
 629
 630 inline cic:/CoRN/devel/loeb/IDA/Ch6/member.con.
 631
 632 (* UNEXPORTED
 633 Implicit Arguments member [A].
 634 *)
 635
 636 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con.
 637
 638 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con.
 639
 640 inline cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con.
 641
 642 inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con.
 643
 644 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con.
 645
 646 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con.
 647
 648 (* UNEXPORTED
 649 End Th15.
 650 *)
 651