inline "cic:/CoRN/algebra/CLogic/CProp.con".
(* UNEXPORTED
-Section Basics.
+Section Basics
*)
(*#* ** Basics
*)
(* UNEXPORTED
-End Basics.
+End Basics
*)
(* begin hide *)
*)
(* UNEXPORTED
-Section Choice.
+Section Choice
*)
(* **Choice
Let [P] be a predicate on $\NN^2$#N times N#.
*)
-inline "cic:/CoRN/algebra/CLogic/P.var".
+alias id "P" = "cic:/CoRN/algebra/CLogic/Choice/P.var".
inline "cic:/CoRN/algebra/CLogic/choice.con".
(* UNEXPORTED
-End Choice.
+End Choice
*)
(* UNEXPORTED
-Section Logical_Remarks.
+Section Logical_Remarks
*)
(*#* We prove a few logical results which are helpful to have as lemmas
inline "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con".
(* UNEXPORTED
-End Logical_Remarks.
+End Logical_Remarks
*)
(* UNEXPORTED
-Section CRelation_Definition.
+Section CRelation_Definition
*)
(*#* ** [CProp]-valued Relations
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CLogic/A.var".
+alias id "A" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var".
inline "cic:/CoRN/algebra/CLogic/Crelation.con".
-inline "cic:/CoRN/algebra/CLogic/R.var".
+alias id "R" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var".
inline "cic:/CoRN/algebra/CLogic/Creflexive.con".
inline "cic:/CoRN/algebra/CLogic/Cequiv.con".
(* UNEXPORTED
-End CRelation_Definition.
+End CRelation_Definition
*)
(* UNEXPORTED
-Section TRelation_Definition.
+Section TRelation_Definition
*)
(*#* ** [Prop]-valued Relations
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CLogic/A.var".
+alias id "A" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var".
inline "cic:/CoRN/algebra/CLogic/Trelation.con".
-inline "cic:/CoRN/algebra/CLogic/R.var".
+alias id "R" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var".
inline "cic:/CoRN/algebra/CLogic/Treflexive.con".
inline "cic:/CoRN/algebra/CLogic/Tequiv.con".
(* UNEXPORTED
-End TRelation_Definition.
+End TRelation_Definition
*)
inline "cic:/CoRN/algebra/CLogic/eqs.ind".
(* UNEXPORTED
-Section le_odd.
+Section le_odd
*)
(*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
inline "cic:/CoRN/algebra/CLogic/to_Ceven.con".
(* UNEXPORTED
-End le_odd.
+End le_odd
*)
(* UNEXPORTED
-Section Misc.
+Section Misc
*)
(*#* **Miscellaneous
inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
(* UNEXPORTED
-End Misc.
+End Misc
*)
(*#* **Results about the natural numbers
*)
(* UNEXPORTED
-Section Odd_and_Even.
+Section Odd_and_Even
*)
(*#*
inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
(* UNEXPORTED
-End Odd_and_Even.
+End Odd_and_Even
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Natural_Numbers.
+Section Natural_Numbers
*)
(*#* **Algebraic Properties
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CLogic/h.var".
+alias id "h" = "cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var".
(*#*
First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
(* UNEXPORTED
-End Natural_Numbers.
+End Natural_Numbers
*)
(*#*
inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
(* UNEXPORTED
-Section Predicates_to_CProp.
+Section Predicates_to_CProp
*)
(*#* **Logical Properties
inline "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con".
(* UNEXPORTED
-End Predicates_to_CProp.
+End Predicates_to_CProp
*)
(* UNEXPORTED
-Section Predicates_to_Prop.
+Section Predicates_to_Prop
*)
(*#* Finally, analogous results for [Prop]-valued predicates are presented for
inline "cic:/CoRN/algebra/CLogic/four_ind.con".
(* UNEXPORTED
-End Predicates_to_Prop.
+End Predicates_to_Prop
*)
(*#* **Integers