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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6".
25 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation.con.
31 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con.
39 inline cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con.
45 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con.
47 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con.
49 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con.
51 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con.
53 inline cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con.
55 inline cic:/CoRN/devel/loeb/IDA/Ch6/on.con.
57 inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con.
59 (* blz 65 Example 1 *)
61 (* Print Zopp_is_fun.*)
63 (* Print Inv_as_un_op.
64 Geen goed voorbeeld: monoids komen hier al in voor en het is een heel onoverzichtelijk bewijs *)
66 (* blz 65 Example 2 *)
68 (* Print plus_is_bin_fun.*)
70 (* Print mult_as_bin_fun.*)
72 (* blz 66 Example 1 *)
74 (* Print plus_is_assoc.*)
76 (* Print Zplus_is_assoc.*)
78 (* Print Zmult_is_assoc.*)
84 (* Print Qplus_is_assoc.*)
86 (* Print Qmult_is_assoc.*)
88 (* blz 66 Examples 2 *)
94 inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var.
96 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var.
98 inline cic:/CoRN/devel/loeb/IDA/Ch6/g.var.
100 inline cic:/CoRN/devel/loeb/IDA/Ch6/h.var.
102 (* Check comp_as_bin_op.*)
104 (* Check assoc_comp.*)
110 (* blz 66 Example 2eblok 1 *)
116 inline cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con.
118 inline cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con.
120 (* blz 66 Example % 3 *)
122 inline cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con.
124 (* blz 66 Example % 4 *)
130 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
132 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con.
134 inline cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con.
136 inline cic:/CoRN/devel/loeb/IDA/Ch6/app.con.
138 inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con.
140 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con.
142 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con.
144 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con.
146 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con.
148 inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con.
150 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con.
152 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con.
154 inline cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con.
156 inline cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con.
162 inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con.
164 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con.
166 inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con.
174 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con.
176 (* blz 67 Remark 1 *)
182 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con.
184 (* blz 67 Remark 2 *)
190 inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var.
192 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con.
198 (* blz 67 Remark 3 *)
200 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con.
204 inline cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con.
206 (* blz 67 Example 1 *)
212 (* Print nat_is_CMonoid.*)
218 (* Print Z_is_CMonoid.*)
220 (* Print Z_mul_is_CMonoid.*)
222 (* blz 67 Example 3 *)
224 (* Print FS_is_CMonoid.*)
226 (* blz 68 Example blok1 1 *)
232 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind.
234 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con.
236 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con.
238 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con.
240 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con.
242 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con.
244 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con.
246 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con.
248 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con.
250 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con.
252 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con.
254 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con.
256 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con.
258 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con.
260 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con.
262 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con.
264 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con.
270 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con.
272 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con.
274 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con.
276 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con.
278 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con.
280 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con.
282 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con.
284 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con.
286 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con.
288 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con.
290 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con.
292 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con.
294 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con.
296 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con.
298 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con.
300 inline cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con.
306 (* blz 68 Example blok2 1 *)
308 (* Print Zplus_is_commut.*)
310 (* Print Zmult_is_commut. *)
312 (* Print Qplus_is_commut1. *)
314 (* Print Qmult_is_commut. *)
326 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
328 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
330 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con.
332 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con.
334 inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con.
336 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con.
338 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con.
348 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
350 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
352 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con.
354 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con.
356 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con.
358 inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con.
370 inline cic:/CoRN/devel/loeb/IDA/Ch6/PM1M2.con.
372 inline cic:/CoRN/devel/loeb/IDA/Ch6/uu.con.
374 inline cic:/CoRN/devel/loeb/IDA/Ch6/e1u.con.
376 inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con.
388 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
390 inline cic:/CoRN/devel/loeb/IDA/Ch6/I.var.
392 inline cic:/CoRN/devel/loeb/IDA/Ch6/C.var.
394 inline cic:/CoRN/devel/loeb/IDA/Ch6/Cunit.var.
396 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_C.var.
398 inline cic:/CoRN/devel/loeb/IDA/Ch6/K.con.
400 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con.
402 inline cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con.
414 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
416 inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con.
418 inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con.
420 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con.
422 inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con.
438 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.con.
440 inline cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con.
442 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con.
444 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con.
446 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con.
448 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con.
450 inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con.
452 inline cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con.
464 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
466 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
468 inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con.
470 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con.
476 (* blz 71 Example 1 *)
482 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
484 inline cic:/CoRN/devel/loeb/IDA/Ch6/c.var.
486 inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con.
488 inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con.
490 inline cic:/CoRN/devel/loeb/IDA/Ch6/is_generated_by.var.
492 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con.
494 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con.
496 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con.
498 inline cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con.
508 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con.
510 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con.
516 (* Print to_word_bijective.*)
522 inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var.
524 inline cic:/CoRN/devel/loeb/IDA/Ch6/L.con.
526 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con.
528 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con.
530 inline cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con.
536 (* blz 71 Remark 1 *)
542 inline cic:/CoRN/devel/loeb/IDA/Ch6/S1.var.
544 inline cic:/CoRN/devel/loeb/IDA/Ch6/S2.var.
546 inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con.
556 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
558 inline cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con.
570 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
572 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
574 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var.
576 inline cic:/CoRN/devel/loeb/IDA/Ch6/isof.var.
578 inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con.
580 inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con.
586 (* blz 71 Examples 2eblok 1 *)
592 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con.
594 inline cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con.
604 inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var.
606 inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var.
608 inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con.
610 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con.
612 inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con.
614 inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con.
624 inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var.
626 inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con.
628 inline cic:/CoRN/devel/loeb/IDA/Ch6/D.var.
630 inline cic:/CoRN/devel/loeb/IDA/Ch6/member.con.
633 Implicit Arguments member [A].
636 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con.
638 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con.
640 inline cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con.
642 inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con.
644 inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con.
646 inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con.