helm/software/matita/contribs/procedural/CoRN/devel/loeb/IDA/Ch6.mma

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