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