set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids".
+include "CoRN.ma".
+
(* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
(*#* printing [=] %\ensuremath{\equiv}% #≡# *)
i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
*)
-(* INCLUDE
-CLogic
-*)
+include "algebra/CLogic.ma".
-(* INCLUDE
-Step
-*)
+include "tactics/Step.ma".
-inline cic:/CoRN/algebra/CSetoids/Relation.con.
+inline "cic:/CoRN/algebra/CSetoids/Relation.con".
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section Properties_of_relations.
+Section Properties_of_relations
*)
-inline cic:/CoRN/algebra/CSetoids/A.var.
+alias id "A" = "cic:/CoRN/algebra/CSetoids/Properties_of_relations/A.var".
-inline cic:/CoRN/algebra/CSetoids/irreflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/irreflexive.con".
-inline cic:/CoRN/algebra/CSetoids/cotransitive.con.
+inline "cic:/CoRN/algebra/CSetoids/cotransitive.con".
-inline cic:/CoRN/algebra/CSetoids/tight_apart.con.
+inline "cic:/CoRN/algebra/CSetoids/tight_apart.con".
-inline cic:/CoRN/algebra/CSetoids/antisymmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/antisymmetric.con".
(* UNEXPORTED
-End Properties_of_relations.
+End Properties_of_relations
*)
(* begin hide *)
Apartness, being the main relation, needs to be [CProp]-valued. Equality,
as it is characterized by a negative statement, lives in [Prop]. *)
-inline cic:/CoRN/algebra/CSetoids/is_CSetoid.ind.
+inline "cic:/CoRN/algebra/CSetoids/is_CSetoid.ind".
-inline cic:/CoRN/algebra/CSetoids/CSetoid.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/cs_crr.con 0 (* compounds *).
(* UNEXPORTED
Implicit Arguments cs_eq [c].
Implicit Arguments cs_ap [c].
*)
+(* NOTATION
+Infix "[=]" := cs_eq (at level 70, no associativity).
+*)
+
+(* NOTATION
+Infix "[#]" := cs_ap (at level 70, no associativity).
+*)
+
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/cs_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_neq.con".
(* UNEXPORTED
Implicit Arguments cs_neq [S].
*)
+(* NOTATION
+Infix "[~=]" := cs_neq (at level 70, no associativity).
+*)
+
(*#*
%\begin{nameconvention}%
In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by
(* Begin_SpecReals *)
(* UNEXPORTED
-Section CSetoid_axioms.
+Section CSetoid_axioms
*)
-inline cic:/CoRN/algebra/CSetoids/S.var.
+alias id "S" = "cic:/CoRN/algebra/CSetoids/CSetoid_axioms/S.var".
-inline cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con".
-inline cic:/CoRN/algebra/CSetoids/ap_irreflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive.con".
-inline cic:/CoRN/algebra/CSetoids/ap_symmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_symmetric.con".
-inline cic:/CoRN/algebra/CSetoids/ap_cotransitive.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive.con".
-inline cic:/CoRN/algebra/CSetoids/ap_tight.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_tight.con".
(* UNEXPORTED
-End CSetoid_axioms.
+End CSetoid_axioms
*)
(* End_SpecReals *)
(* Begin_SpecReals *)
(* UNEXPORTED
-Section CSetoid_basics.
+Section CSetoid_basics
*)
-inline cic:/CoRN/algebra/CSetoids/S.var.
+alias id "S" = "cic:/CoRN/algebra/CSetoids/CSetoid_basics/S.var".
(* End_SpecReals *)
In `there exists a unique [a:S] such that %\ldots%#...#', we now mean unique with respect to the setoid equality. We use [ex_unq] to denote unique existence.
*)
-inline cic:/CoRN/algebra/CSetoids/ex_unq.con.
+inline "cic:/CoRN/algebra/CSetoids/ex_unq.con".
-inline cic:/CoRN/algebra/CSetoids/eq_reflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_reflexive.con".
-inline cic:/CoRN/algebra/CSetoids/eq_symmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_symmetric.con".
-inline cic:/CoRN/algebra/CSetoids/eq_transitive.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_transitive.con".
(*#*
%\begin{shortcoming}%
%\end{nameconvention}%
*)
-inline cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/eq_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_wdl.con".
(* Begin_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con".
(*#*
%\begin{shortcoming}%
%\end{shortcoming}%
*)
-inline cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con".
-inline cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con".
-inline cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con".
-inline cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con".
-inline cic:/CoRN/algebra/CSetoids/ap_imp_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_imp_neq.con".
-inline cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con".
-inline cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CSetoid_basics.
+End CSetoid_basics
*)
(* End_SpecReals *)
(* UNEXPORTED
-Section product_csetoid.
+Section product_csetoid
*)
(*#* **The product of setoids *)
-inline cic:/CoRN/algebra/CSetoids/prod_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/prod_ap.con".
-inline cic:/CoRN/algebra/CSetoids/prod_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/prod_eq.con".
-inline cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con".
-inline cic:/CoRN/algebra/CSetoids/ProdCSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/ProdCSetoid.con".
(* UNEXPORTED
-End product_csetoid.
+End product_csetoid
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section CSetoid_relations_and_predicates.
+Section CSetoid_relations_and_predicates
*)
-inline cic:/CoRN/algebra/CSetoids/S.var.
+alias id "S" = "cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/S.var".
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section CSetoidPredicates.
+Section CSetoidPredicates
*)
-inline cic:/CoRN/algebra/CSetoids/P.var.
+alias id "P" = "cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CSetoidPredicates/P.var".
-inline cic:/CoRN/algebra/CSetoids/pred_strong_ext.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext.con".
-inline cic:/CoRN/algebra/CSetoids/pred_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_wd.con".
(* UNEXPORTED
-End CSetoidPredicates.
+End CSetoidPredicates
*)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind".
-inline cic:/CoRN/algebra/CSetoids/csp_wd.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con 0 (* compounds *).
+
+inline "cic:/CoRN/algebra/CSetoids/csp_wd.con".
(*#* Similar, with [Prop] instead of [CProp]. *)
(* UNEXPORTED
-Section CSetoidPPredicates.
+Section CSetoidPPredicates
*)
-inline cic:/CoRN/algebra/CSetoids/P.var.
+alias id "P" = "cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CSetoidPPredicates/P.var".
-inline cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con".
-inline cic:/CoRN/algebra/CSetoids/pred_wd'.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_wd'.con".
(* UNEXPORTED
-End CSetoidPPredicates.
+End CSetoidPPredicates
*)
(*#* ***Definition of a setoid predicate *)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con 0 (* compounds *).
-inline cic:/CoRN/algebra/CSetoids/csp'_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csp'_wd.con".
(* Begin_SpecReals *)
%\end{convention}% *)
(* UNEXPORTED
-Section CsetoidRelations.
+Section CsetoidRelations
*)
-inline cic:/CoRN/algebra/CSetoids/R.var.
+alias id "R" = "cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CsetoidRelations/R.var".
-inline cic:/CoRN/algebra/CSetoids/rel_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_wdr.con".
-inline cic:/CoRN/algebra/CSetoids/rel_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_wdl.con".
-inline cic:/CoRN/algebra/CSetoids/rel_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/rel_strext_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_lft.con".
-inline cic:/CoRN/algebra/CSetoids/rel_strext_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_rht.con".
-inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con".
-inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con".
-inline cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CsetoidRelations.
+End CsetoidRelations
*)
(*#* ***Definition of a setoid relation
The type of relations over a setoid. *)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con 0 (* compounds *).
(*#* ***[CProp] Relations
%\begin{convention}%
*)
(* UNEXPORTED
-Section CCsetoidRelations.
+Section CCsetoidRelations
*)
-inline cic:/CoRN/algebra/CSetoids/R.var.
+alias id "R" = "cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CCsetoidRelations/R.var".
-inline cic:/CoRN/algebra/CSetoids/Crel_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_wdr.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_wdl.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con".
-inline cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CCsetoidRelations.
+End CCsetoidRelations
*)
(*#* ***Definition of a [CProp] setoid relation
The type of relations over a setoid. *)
-inline cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind.
+inline "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind".
-inline cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *).
-inline cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con".
+
+inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/ap_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdr.con".
-inline cic:/CoRN/algebra/CSetoids/ap_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdl.con".
-inline cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/ap_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_strext.con".
-inline cic:/CoRN/algebra/CSetoids/predS_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/predS_well_def.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CSetoid_relations_and_predicates.
+End CSetoid_relations_and_predicates
*)
(* UNEXPORTED
(* Begin_SpecReals *)
(* UNEXPORTED
-Section CSetoid_functions.
+Section CSetoid_functions
*)
-inline cic:/CoRN/algebra/CSetoids/S1.var.
+alias id "S1" = "cic:/CoRN/algebra/CSetoids/CSetoid_functions/S1.var".
-inline cic:/CoRN/algebra/CSetoids/S2.var.
+alias id "S2" = "cic:/CoRN/algebra/CSetoids/CSetoid_functions/S2.var".
-inline cic:/CoRN/algebra/CSetoids/S3.var.
+alias id "S3" = "cic:/CoRN/algebra/CSetoids/CSetoid_functions/S3.var".
(* UNEXPORTED
-Section unary_functions.
+Section unary_functions
*)
(*#*
[f] is a function from (the carrier of) [S1] to
(the carrier of) [S2]. *)
-inline cic:/CoRN/algebra/CSetoids/f.var.
+alias id "f" = "cic:/CoRN/algebra/CSetoids/CSetoid_functions/unary_functions/f.var".
-inline cic:/CoRN/algebra/CSetoids/fun_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_wd.con".
-inline cic:/CoRN/algebra/CSetoids/fun_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_strext.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End unary_functions.
+End unary_functions
*)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con 0 (* compounds *).
-inline cic:/CoRN/algebra/CSetoids/csf_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_wd.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con.
+inline "cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-Section binary_functions.
+Section binary_functions
*)
(*#*
[f] is a function from [S1] and [S2] to [S3].
*)
-inline cic:/CoRN/algebra/CSetoids/f.var.
+alias id "f" = "cic:/CoRN/algebra/CSetoids/CSetoid_functions/binary_functions/f.var".
-inline cic:/CoRN/algebra/CSetoids/bin_fun_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_wd.con".
-inline cic:/CoRN/algebra/CSetoids/bin_fun_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End binary_functions.
+End binary_functions
*)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
-inline cic:/CoRN/algebra/CSetoids/csbf_wd.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con 0 (* compounds *).
-inline cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csbf_wd.con".
-inline cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con".
+
+inline "cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con".
(* UNEXPORTED
-End CSetoid_functions.
+End CSetoid_functions
*)
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section csetoid_inner_ops.
+Section csetoid_inner_ops
*)
-inline cic:/CoRN/algebra/CSetoids/S.var.
+alias id "S" = "cic:/CoRN/algebra/CSetoids/csetoid_inner_ops/S.var".
(*#* Properties of binary operations *)
-inline cic:/CoRN/algebra/CSetoids/commutes.con.
+inline "cic:/CoRN/algebra/CSetoids/commutes.con".
-inline cic:/CoRN/algebra/CSetoids/associative.con.
+inline "cic:/CoRN/algebra/CSetoids/associative.con".
(*#* Well-defined unary operations on a setoid. *)
-inline cic:/CoRN/algebra/CSetoids/un_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_wd.con".
-inline cic:/CoRN/algebra/CSetoids/un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_strext.con".
-inline cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con".
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/id_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/id_strext.con".
-inline cic:/CoRN/algebra/CSetoids/id_pres_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/id_pres_eq.con".
-inline cic:/CoRN/algebra/CSetoids/id_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/id_un_op.con".
(* begin hide *)
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con 0 (* compounds *).
+
(* end hide *)
(* Begin_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con".
(*#* Well-defined binary operations on a setoid. *)
-inline cic:/CoRN/algebra/CSetoids/bin_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_wd.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_strext.con".
(* Begin_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con".
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con".
-inline cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con".
(* Begin_SpecReals *)
(* begin hide *)
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *).
+
(* end hide *)
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con".
-inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End csetoid_inner_ops.
+End csetoid_inner_ops
*)
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section csetoid_outer_ops.
+Section csetoid_outer_ops
*)
-inline cic:/CoRN/algebra/CSetoids/S1.var.
+alias id "S1" = "cic:/CoRN/algebra/CSetoids/csetoid_outer_ops/S1.var".
-inline cic:/CoRN/algebra/CSetoids/S2.var.
+alias id "S2" = "cic:/CoRN/algebra/CSetoids/csetoid_outer_ops/S2.var".
(*#*
Well-defined outer operations on a setoid.
*)
-inline cic:/CoRN/algebra/CSetoids/outer_op_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/outer_op_well_def.con".
-inline cic:/CoRN/algebra/CSetoids/outer_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/outer_op_strext.con".
-inline cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con".
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con".
-inline cic:/CoRN/algebra/CSetoids/csoo_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_wd.con".
-inline cic:/CoRN/algebra/CSetoids/csoo_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_strext.con".
(* begin hide *)
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *).
+
(* end hide *)
-inline cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con".
(* UNEXPORTED
-End csetoid_outer_ops.
+End csetoid_outer_ops
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section SubCSetoids.
+Section SubCSetoids
*)
-inline cic:/CoRN/algebra/CSetoids/S.var.
+alias id "S" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/S.var".
+
+alias id "P" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/P.var".
-inline cic:/CoRN/algebra/CSetoids/P.var.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con 0 (* compounds *).
(*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
uniform inheritance condition and will not be inserted. However it will
also not be printed, which is handy.
*)
-inline cic:/CoRN/algebra/CSetoids/restrict_relation.con.
+inline "cic:/CoRN/algebra/CSetoids/restrict_relation.con".
-inline cic:/CoRN/algebra/CSetoids/Crestrict_relation.con.
+inline "cic:/CoRN/algebra/CSetoids/Crestrict_relation.con".
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con".
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con".
(* End_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con".
(* Begin_SpecReals *)
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con".
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con".
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section SubCSetoid_unary_operations.
+Section SubCSetoid_unary_operations
*)
-inline cic:/CoRN/algebra/CSetoids/f.var.
+alias id "f" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_unary_operations/f.var".
-inline cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con".
(*#*
%\begin{convention}%
Assume [pr:un_op_pres_pred].
%\end{convention}% *)
-inline cic:/CoRN/algebra/CSetoids/pr.var.
+alias id "pr" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_unary_operations/pr.var".
-inline cic:/CoRN/algebra/CSetoids/restr_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op.con".
-inline cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con".
-inline cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con".
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con".
(* UNEXPORTED
-End SubCSetoid_unary_operations.
+End SubCSetoid_unary_operations
*)
(*#* ***Subsetoid binary operations
*)
(* UNEXPORTED
-Section SubCSetoid_binary_operations.
+Section SubCSetoid_binary_operations
*)
-inline cic:/CoRN/algebra/CSetoids/f.var.
+alias id "f" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_binary_operations/f.var".
-inline cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con".
(*#*
%\begin{convention}%
%\end{convention}%
*)
-inline cic:/CoRN/algebra/CSetoids/pr.var.
+alias id "pr" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_binary_operations/pr.var".
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op.con".
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con".
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con".
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con".
-inline cic:/CoRN/algebra/CSetoids/restr_f_assoc.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_f_assoc.con".
(* UNEXPORTED
-End SubCSetoid_binary_operations.
+End SubCSetoid_binary_operations
*)
(* Begin_SpecReals *)
(* UNEXPORTED
-End SubCSetoids.
+End SubCSetoids
*)
(* End_SpecReals *)
(*#* **Miscellaneous
*)
-inline cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con.
+inline "cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con".
(*#*
Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
*)
-inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con.
+inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con".
-inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con.
+inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con".
(* UNEXPORTED
Implicit Arguments nat_less_n_fun [S n].