1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 include "algebra/CSemiGroups.ma".
23 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation.con".
25 include "model/setoids/Zsetoid.ma".
27 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con".
31 include "devel/loeb/per/csetfun.ma".
33 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con".
35 include "model/setoids/Nsetoid.ma".
37 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con".
39 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con".
41 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con".
43 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con".
45 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con".
47 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/on.con".
49 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con" "__".
51 (* blz 65 Example 1 *)
53 (* Print Zopp_is_fun.*)
55 (* Print Inv_as_un_op.
56 Geen goed voorbeeld: monoids komen hier al in voor en het is een heel onoverzichtelijk bewijs *)
58 (* blz 65 Example 2 *)
60 (* Print plus_is_bin_fun.*)
62 (* Print mult_as_bin_fun.*)
64 (* blz 66 Example 1 *)
66 (* Print plus_is_assoc.*)
68 (* Print Zplus_is_assoc.*)
70 (* Print Zmult_is_assoc.*)
72 include "model/setoids/Qsetoid.ma".
74 (* Print Qplus_is_assoc.*)
76 (* Print Qmult_is_assoc.*)
78 (* blz 66 Examples 2 *)
84 alias id "X" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/X.var".
86 alias id "f" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/f.var".
88 alias id "g" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/g.var".
90 alias id "h" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/h.var".
92 (* Check comp_as_bin_op.*)
94 (* Check assoc_comp.*)
100 (* blz 66 Example 2eblok 1 *)
102 include "model/semigroups/Zsemigroup.ma".
104 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con".
106 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con".
108 (* blz 66 Example % 3 *)
110 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con".
112 (* blz 66 Example % 4 *)
118 alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2b4/A.var".
120 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con".
122 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con".
124 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app.con".
126 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con".
128 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con".
130 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con".
132 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con".
134 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con".
136 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con".
138 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con".
140 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con".
142 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con".
144 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con".
146 include "algebra/CSemiGroups.ma".
148 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con".
150 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con".
152 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con".
160 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con".
162 (* blz 67 Remark 1 *)
164 include "model/monoids/Zmonoid.ma".
166 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con".
168 (* blz 67 Remark 2 *)
174 alias id "X" = "cic:/CoRN/devel/loeb/IDA/Ch6/p67R2/X.var".
176 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con".
182 (* blz 67 Remark 3 *)
184 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con".
188 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con".
190 (* blz 67 Example 1 *)
192 include "model/monoids/Nmonoid.ma".
194 (* Print nat_is_CMonoid.*)
196 include "model/monoids/Zmonoid.ma".
198 (* Print Z_is_CMonoid.*)
200 (* Print Z_mul_is_CMonoid.*)
202 (* blz 67 Example 3 *)
204 (* Print FS_is_CMonoid.*)
206 (* blz 68 Example blok1 1 *)
212 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind".
214 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con".
216 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con".
218 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con".
220 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con".
222 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con".
224 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con".
226 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con".
228 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con".
230 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con".
232 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con".
234 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con".
236 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con".
238 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con".
240 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con".
242 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con".
244 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con".
246 include "algebra/CMonoids.ma".
248 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con".
250 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con".
252 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con".
254 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con".
256 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con".
258 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con".
260 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con".
262 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con".
264 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con".
266 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con".
268 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con".
270 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con".
272 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con".
274 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con".
276 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con".
278 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con".
284 (* blz 68 Example blok2 1 *)
286 (* Print Zplus_is_commut.*)
288 (* Print Zmult_is_commut. *)
290 (* Print Qplus_is_commut1. *)
292 (* Print Qmult_is_commut. *)
296 include "algebra/CMonoids.ma".
302 alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M1.var".
304 alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M2.var".
306 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con".
308 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con".
310 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con".
312 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con".
314 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con".
324 alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M1.var".
326 alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M2.var".
328 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con".
330 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con".
332 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con".
334 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con".
346 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/PM1M2.con" "p69E1__".
348 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/uu.con" "p69E1__".
350 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/e1u.con" "p69E1__".
352 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con".
364 alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/M.var".
366 alias id "I" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/I.var".
368 alias id "C" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/C.var".
370 alias id "Cunit" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/Cunit.var".
372 alias id "op_pres_C" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/op_pres_C.var".
374 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/K.con".
376 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con".
378 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con".
390 alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th12/A.var".
392 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con".
394 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con".
396 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con".
398 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con".
410 include "devel/loeb/per/lst2fun.ma".
412 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p70text/A.con" "p70text__".
414 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con".
416 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con".
418 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con".
420 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con".
422 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con".
424 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con".
426 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con".
438 alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M1.var".
440 alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M2.var".
442 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con".
444 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con".
450 (* blz 71 Example 1 *)
456 alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/M.var".
458 alias id "c" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/c.var".
460 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con".
462 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con".
464 alias id "is_generated_by" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/is_generated_by.var".
466 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/f.con" "p71E1__".
468 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con".
470 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con".
472 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con".
482 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con".
484 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con".
490 (* Print to_word_bijective.*)
496 alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/A.var".
498 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/L.con" "p71E2__".
500 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con".
502 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con".
504 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con".
510 (* blz 71 Remark 1 *)
516 alias id "S1" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S1.var".
518 alias id "S2" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S2.var".
520 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con".
530 alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R2/M.var".
532 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con".
544 alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M1.var".
546 alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M2.var".
548 alias id "f" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/f.var".
550 alias id "isof" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/isof.var".
552 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con".
554 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con".
560 (* blz 71 Examples 2eblok 1 *)
566 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con".
568 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con".
578 alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M1.var".
580 alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M2.var".
582 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/f.con" "p71E2b2__".
584 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con".
586 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con".
588 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con".
598 alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th15/M.var".
600 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con".
602 alias id "D" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th15/D.var".
604 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/member.con".
607 Implicit Arguments member [A].
610 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con".
612 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con".
614 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con".
616 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con".
618 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con".
620 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con".