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" as definition.
25 include "model/setoids/Zsetoid.ma".
27 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con" as lemma.
31 include "devel/loeb/per/csetfun.ma".
33 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con" as definition.
35 include "model/setoids/Nsetoid.ma".
37 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con" as definition.
39 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con" as lemma.
41 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con" as definition.
43 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con" as lemma.
45 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con" as definition.
47 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/on.con" as definition.
49 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con" "__" as definition.
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 *)
85 cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/X.var
89 cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/f.var
93 cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/g.var
97 cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/h.var
100 (* Check comp_as_bin_op.*)
102 (* Check assoc_comp.*)
108 (* blz 66 Example 2eblok 1 *)
110 include "model/semigroups/Zsemigroup.ma".
112 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con" as lemma.
114 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con" as lemma.
116 (* blz 66 Example % 3 *)
118 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con" as lemma.
120 (* blz 66 Example % 4 *)
127 cic:/CoRN/devel/loeb/IDA/Ch6/p66E2b4/A.var
130 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con" as definition.
132 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con" as definition.
134 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app.con" as definition.
136 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con" as definition.
138 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con" as definition.
140 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con" as lemma.
142 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con" as lemma.
144 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con" as lemma.
146 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con" as lemma.
148 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con" as definition.
150 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con" as definition.
152 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con" as lemma.
154 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con" as definition.
156 include "algebra/CSemiGroups.ma".
158 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con" as lemma.
160 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con" as lemma.
162 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con" as definition.
170 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con" as definition.
172 (* blz 67 Remark 1 *)
174 include "model/monoids/Zmonoid.ma".
176 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con" as lemma.
178 (* blz 67 Remark 2 *)
185 cic:/CoRN/devel/loeb/IDA/Ch6/p67R2/X.var
188 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con" as lemma.
194 (* blz 67 Remark 3 *)
196 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con" as lemma.
200 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con" as lemma.
202 (* blz 67 Example 1 *)
204 include "model/monoids/Nmonoid.ma".
206 (* Print nat_is_CMonoid.*)
208 include "model/monoids/Zmonoid.ma".
210 (* Print Z_is_CMonoid.*)
212 (* Print Z_mul_is_CMonoid.*)
214 (* blz 67 Example 3 *)
216 (* Print FS_is_CMonoid.*)
218 (* blz 68 Example blok1 1 *)
224 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind".
226 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con" as definition.
228 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con" as definition.
230 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con" as lemma.
232 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con" as lemma.
234 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con" as lemma.
236 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con" as lemma.
238 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con" as definition.
240 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con" as lemma.
242 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con" as lemma.
244 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con" as definition.
246 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con" as definition.
248 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con" as definition.
250 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con" as definition.
252 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con" as lemma.
254 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con" as definition.
256 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con" as lemma.
258 include "algebra/CMonoids.ma".
260 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con" as lemma.
262 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con" as lemma.
264 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con" as definition.
266 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con" as definition.
268 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con" as definition.
270 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con" as definition.
272 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con" as definition.
274 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con" as lemma.
276 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con" as definition.
278 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con" as lemma.
280 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con" as definition.
282 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con" as lemma.
284 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con" as lemma.
286 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con" as definition.
288 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con" as definition.
290 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con" as lemma.
296 (* blz 68 Example blok2 1 *)
298 (* Print Zplus_is_commut.*)
300 (* Print Zmult_is_commut. *)
302 (* Print Qplus_is_commut1. *)
304 (* Print Qmult_is_commut. *)
308 include "algebra/CMonoids.ma".
315 cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M1.var
319 cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M2.var
322 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con" as definition.
324 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con" as lemma.
326 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con" as definition.
328 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con" as lemma.
330 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con" as definition.
341 cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M1.var
345 cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M2.var
348 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con" as lemma.
350 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con" as lemma.
352 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con" as definition.
354 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con" as definition.
366 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/PM1M2.con" "p69E1__" as definition.
368 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/uu.con" "p69E1__" as definition.
370 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/e1u.con" "p69E1__" as definition.
372 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con" as lemma.
385 cic:/CoRN/devel/loeb/IDA/Ch6/Th11/M.var
389 cic:/CoRN/devel/loeb/IDA/Ch6/Th11/I.var
393 cic:/CoRN/devel/loeb/IDA/Ch6/Th11/C.var
397 cic:/CoRN/devel/loeb/IDA/Ch6/Th11/Cunit.var
401 cic:/CoRN/devel/loeb/IDA/Ch6/Th11/op_pres_C.var
404 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/K.con" as definition.
406 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con" as lemma.
408 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con" as definition.
421 cic:/CoRN/devel/loeb/IDA/Ch6/Th12/A.var
424 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con" as lemma.
426 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con" as lemma.
428 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con" as definition.
430 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con" as definition.
442 include "devel/loeb/per/lst2fun.ma".
444 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p70text/A.con" "p70text__" as definition.
446 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con" as lemma.
448 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con" as definition.
450 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con" as definition.
452 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con" as lemma.
454 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con" as definition.
456 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con" as lemma.
458 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con" as lemma.
471 cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M1.var
475 cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M2.var
478 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con" as definition.
480 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con" as definition.
486 (* blz 71 Example 1 *)
493 cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/M.var
497 cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/c.var
500 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con" as definition.
502 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con" as definition.
505 cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/is_generated_by.var
508 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/f.con" "p71E1__" as definition.
510 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con" as lemma.
512 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con" as definition.
514 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con" as lemma.
524 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con" as lemma.
526 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con" as lemma.
532 (* Print to_word_bijective.*)
539 cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/A.var
542 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/L.con" "p71E2__" as definition.
544 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con" as lemma.
546 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con" as definition.
548 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con" as lemma.
554 (* blz 71 Remark 1 *)
561 cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S1.var
565 cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S2.var
568 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con" as definition.
579 cic:/CoRN/devel/loeb/IDA/Ch6/p71R2/M.var
582 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con" as definition.
595 cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M1.var
599 cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M2.var
603 cic:/CoRN/devel/loeb/IDA/Ch6/Th14/f.var
607 cic:/CoRN/devel/loeb/IDA/Ch6/Th14/isof.var
610 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con" as lemma.
612 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con" as lemma.
618 (* blz 71 Examples 2eblok 1 *)
624 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con" as definition.
626 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con" as lemma.
637 cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M1.var
641 cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M2.var
644 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/f.con" "p71E2b2__" as definition.
646 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con" as lemma.
648 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con" as definition.
650 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con" as lemma.
661 cic:/CoRN/devel/loeb/IDA/Ch6/Th15/M.var
664 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con" as definition.
667 cic:/CoRN/devel/loeb/IDA/Ch6/Th15/D.var
670 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/member.con" as definition.
673 Implicit Arguments member [A].
676 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con" as definition.
678 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con" as lemma.
680 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con" as lemma.
682 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con" as lemma.
684 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con" as lemma.
686 inline procedural "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con" as definition.