*)
(* 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/antisymmetric.con".
(* UNEXPORTED
-End Properties_of_relations.
+End Properties_of_relations
*)
(* begin hide *)
(* 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/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 *)
(* 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/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_wd.con".
(* UNEXPORTED
-End CSetoidPredicates.
+End CSetoidPredicates
*)
inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind".
(*#* 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_wd'.con".
(* UNEXPORTED
-End CSetoidPPredicates.
+End CSetoidPPredicates
*)
(*#* ***Definition of a setoid predicate *)
%\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".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CsetoidRelations.
+End CsetoidRelations
*)
(*#* ***Definition of a setoid relation
*)
(* 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".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CCsetoidRelations.
+End CCsetoidRelations
*)
(*#* ***Definition of a [CProp] setoid relation
(* 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".
(* Begin_SpecReals *)
(* UNEXPORTED
-End unary_functions.
+End unary_functions
*)
inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
(* 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".
(* Begin_SpecReals *)
(* UNEXPORTED
-End binary_functions.
+End binary_functions
*)
inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
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 *)
(* 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/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".
-inline "cic:/CoRN/algebra/CSetoids/P.var".
+alias id "P" = "cic:/CoRN/algebra/CSetoids/SubCSetoids/P.var".
inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
*)
(* 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".
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/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".
%\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_f_assoc.con".
(* UNEXPORTED
-End SubCSetoid_binary_operations.
+End SubCSetoid_binary_operations
*)
(* Begin_SpecReals *)
(* UNEXPORTED
-End SubCSetoids.
+End SubCSetoids
*)
(* End_SpecReals *)