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