X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fdevel%2Floeb%2FIDA%2FCh6.ma;h=fe7031a986df79181cdb05abdf9b3dc3dcf8505f;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=c1295ea7d8027142460dd7de773a8f4996afaa3a;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma b/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma index c1295ea7d..fe7031a98 100644 --- a/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma +++ b/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma @@ -16,45 +16,39 @@ set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6". -(* INCLUDE -CSemiGroups -*) +include "CoRN.ma". + +include "algebra/CSemiGroups.ma". (* Remark blz 65 1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation.con". -(* INCLUDE -Zsetoid -*) +include "model/setoids/Zsetoid.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_nullary_operation_Z_0.con". (* Remark blz 65 2 *) -(* INCLUDE -csetfun -*) +include "devel/loeb/per/csetfun.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/n_ary_operation.con". -(* INCLUDE -Nsetoid -*) +include "model/setoids/Nsetoid.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/plus1.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus1_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/plus2.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_plus2_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/plus3.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/on.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/on.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ex_3_ary.con" "__". (* blz 65 Example 1 *) @@ -77,9 +71,7 @@ Geen goed voorbeeld: monoids komen hier al in voor en het is een heel onoverzich (* Print Zmult_is_assoc.*) -(* INCLUDE -Qsetoid -*) +include "model/setoids/Qsetoid.ma". (* Print Qplus_is_assoc.*) @@ -88,132 +80,122 @@ Qsetoid (* blz 66 Examples 2 *) (* UNEXPORTED -Section p66E2. +Section p66E2 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var. +alias id "X" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/X.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var. +alias id "f" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/f.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/g.var. +alias id "g" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/g.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/h.var. +alias id "h" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2/h.var". (* Check comp_as_bin_op.*) (* Check assoc_comp.*) (* UNEXPORTED -End p66E2. +End p66E2 *) (* blz 66 Example 2eblok 1 *) -(* INCLUDE -Zsemigroup -*) +include "model/semigroups/Zsemigroup.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Zplus_is_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Zmult_is_CSemiGroup.con". (* blz 66 Example % 3 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/FS_is_CSemiGroup.con". (* blz 66 Example % 4 *) (* UNEXPORTED -Section p66E2b4. +Section p66E2b4 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var. +alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/p66E2b4/A.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Astar.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/empty_word.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/app.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/app.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_irreflexive.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_symmetric.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_cotransitive.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ap_fm_tight.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_is_CSetoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/free_csetoid_as_csetoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/app_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/app_as_csb_fun.con". -(* INCLUDE -CSemiGroups -*) +include "algebra/CSemiGroups.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/eq_fm_reflexive.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_is_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Astar_as_CSemiGroup.con". (* UNEXPORTED -End p66E2b4. +End p66E2b4 *) (* Definition 5 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit.con". (* blz 67 Remark 1 *) -(* INCLUDE -Zmonoid -*) +include "model/monoids/Zmonoid.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Z_0.con". (* blz 67 Remark 2 *) (* UNEXPORTED -Section p67R2. +Section p67R2 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/X.var. +alias id "X" = "cic:/CoRN/devel/loeb/IDA/Ch6/p67R2/X.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_FS_id.con". (* UNEXPORTED -End p67R2. +End p67R2 *) (* blz 67 Remark 3 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_unit_Astar_empty_word.con". (* Lemma 6 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/unique_unit.con". (* blz 67 Example 1 *) -(* INCLUDE -Nmonoid -*) +include "model/monoids/Nmonoid.ma". (* Print nat_is_CMonoid.*) -(* INCLUDE -Zmonoid -*) +include "model/monoids/Zmonoid.ma". (* Print Z_is_CMonoid.*) @@ -226,81 +208,79 @@ Zmonoid (* blz 68 Example blok1 1 *) (* UNEXPORTED -Section p68E1b1. +Section p68E1b1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1.ind". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_irreflexive.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_symmetric.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_cotransitive.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_eq_dec.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/is_e1.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/not_M1_eq_e1_u.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_ap_tight.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSetoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSetoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_CS_mult_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_mult_as_bin_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CSemiGroup.con". -(* INCLUDE -CMonoids -*) +include "algebra/CMonoids.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_as_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_CS_mult_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_mult_as_bin_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_lft_unit_M2.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1_is_rht_unit_M2.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_is_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M2_as_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/two_element_CMonoids.con". (* UNEXPORTED -End p68E1b1. +End p68E1b1 *) (* blz 68 Example blok2 1 *) @@ -315,337 +295,333 @@ End p68E1b1. (* Definition 9 *) -(* INCLUDE -CMonoids -*) +include "algebra/CMonoids.ma". (* UNEXPORTED -Section D9S. +Section D9S *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var. +alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var. +alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9S/M2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/dprod.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/dprod_as_csb_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CSemiGroup.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CSemiGroup.con". (* UNEXPORTED -End D9S. +End D9S *) (* UNEXPORTED -Section D9M. +Section D9M *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var. +alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var. +alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/D9M/M2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_rht_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/e1e2_is_lft_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_as_CMonoid.con". (* UNEXPORTED -End D9M. +End D9M *) (* blz 69 Example *) (* UNEXPORTED -Section p69E1. +Section p69E1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/PM1M2.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/PM1M2.con" "p69E1__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/uu.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/uu.con" "p69E1__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/e1u.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p69E1/e1u.con" "p69E1__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ex_69.con". (* UNEXPORTED -End p69E1. +End p69E1 *) (* Theorem 11 *) (* UNEXPORTED -Section Th11. +Section Th11 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var. +alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/M.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/I.var. +alias id "I" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/I.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/C.var. +alias id "C" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/C.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Cunit.var. +alias id "Cunit" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/Cunit.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_C.var. +alias id "op_pres_C" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th11/op_pres_C.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/K.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/K.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_K.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/K_is_Monoid.con". (* UNEXPORTED -End Th11. +End Th11 *) (* Theorem 12 *) (* UNEXPORTED -Section Th12. +Section Th12 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var. +alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th12/A.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_rht_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/nil_is_lft_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_is_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/free_monoid_as_CMonoid.con". (* UNEXPORTED -End Th12. +End Th12 *) (* blz 70 text *) (* UNEXPORTED -Section p70text. +Section p70text *) -(* INCLUDE -lst2fun -*) +include "devel/loeb/per/lst2fun.ma". -inline cic:/CoRN/devel/loeb/IDA/Ch6/A.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p70text/A.con" "p70text__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/ZerolessOne.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_word.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_word'_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_as_CSetoid_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/to_word_bijective.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/pres_plus_to_word.con". (* UNEXPORTED -End p70text. +End p70text *) (* Definition 13 *) (* UNEXPORTED -Section Th13. +Section Th13 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var. +alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var. +alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th13/M2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/morphism.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphism.con". (* UNEXPORTED -End Th13. +End Th13 *) (* blz 71 Example 1 *) (* UNEXPORTED -Section p71E1. +Section p71E1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var. +alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/M.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/c.var. +alias id "c" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/c.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/power_CMonoid_CSetoid.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/is_generated_by.var. +alias id "is_generated_by" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/is_generated_by.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p71E1/f.con" "p71E1__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con". (* UNEXPORTED -End p71E1. +End p71E1 *) (* UNEXPORTED -Section p71E1'. +Section p71E1' *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/M1_is_generated_by_u.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con". (* UNEXPORTED -End p71E1'. +End p71E1' *) (* Print to_word_bijective.*) (* UNEXPORTED -Section p71E2. +Section p71E2 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/A.var. +alias id "A" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/A.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/L.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2/L.con" "p71E2__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/L_strext.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/L_is_morphism.con". (* UNEXPORTED -End p71E2. +End p71E2 *) (* blz 71 Remark 1 *) (* UNEXPORTED -Section p71R1. +Section p71R1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/S1.var. +alias id "S1" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/S2.var. +alias id "S2" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R1/S2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/morphism_of_CSemiGroups.con". (* UNEXPORTED -End p71R1. +End p71R1 *) (* UNEXPORTED -Section p71R2. +Section p71R2 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var. +alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71R2/M.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/automorphism.con". (* UNEXPORTED -End p71R2. +End p71R2 *) (* Theorem 14 *) (* UNEXPORTED -Section Th14. +Section Th14 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var. +alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var. +alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/M2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f.var. +alias id "f" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/f.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/isof.var. +alias id "isof" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th14/isof.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/iso_imp_bij.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con". (* UNEXPORTED -End Th14. +End Th14 *) (* blz 71 Examples 2eblok 1 *) (* UNEXPORTED -Section p71E2b1. +Section p71E2b1 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/not_isomorphic_M1_M2.con". (* UNEXPORTED -End p71E2b1. +End p71E2b1 *) (* UNEXPORTED -Section p71E2b2. +Section p71E2b2 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M1.var. +alias id "M1" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M1.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/M2.var. +alias id "M2" = "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/M2.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/p71E2b2/f.con" "p71E2b2__". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/f_strext'.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/f_as_CSetoid_fun'.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/isomorphic_PM1M2_PM2M1.con". (* UNEXPORTED -End p71E2b2. +End p71E2b2 *) (* UNEXPORTED -Section Th15. +Section Th15 *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/M.var. +alias id "M" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th15/M.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/D.var. +alias id "D" = "cic:/CoRN/devel/loeb/IDA/Ch6/Th15/D.var". -inline cic:/CoRN/devel/loeb/IDA/Ch6/member.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/member.con". (* UNEXPORTED Implicit Arguments member [A]. *) -inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_unit.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/member_app.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/cm_Sum_app.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con". -inline cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con. +inline "cic:/CoRN/devel/loeb/IDA/Ch6/Dbrack_as_CMonoid.con". (* UNEXPORTED -End Th15. +End Th15 *)