set "baseuri" "cic:/matita/CoRN-Decl/ftc/IntervalFunct".
+include "CoRN.ma".
+
(* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
-(* INCLUDE
-PartFunEquality
-*)
+include "ftc/PartFunEquality.ma".
(* UNEXPORTED
-Section Operations.
+Section Operations
*)
(*#* * Functions with compact domain
%\end{convention}%
*)
-inline cic:/CoRN/ftc/IntervalFunct/a.var.
+alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Operations/a.var".
-inline cic:/CoRN/ftc/IntervalFunct/b.var.
+alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Operations/b.var".
-inline cic:/CoRN/ftc/IntervalFunct/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var".
(* begin hide *)
-inline cic:/CoRN/ftc/IntervalFunct/I.con.
+inline "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__".
(* end hide *)
-inline cic:/CoRN/ftc/IntervalFunct/f.var.
+alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Operations/f.var".
-inline cic:/CoRN/ftc/IntervalFunct/g.var.
+alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Operations/g.var".
(* UNEXPORTED
-Section Const.
+Section Const
*)
(*#*
%\end{convention}%
*)
-inline cic:/CoRN/ftc/IntervalFunct/c.var.
+alias id "c" = "cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var".
-inline cic:/CoRN/ftc/IntervalFunct/IConst_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IConst.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IConst.con".
(* UNEXPORTED
-End Const.
+End Const
*)
-inline cic:/CoRN/ftc/IntervalFunct/IId_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IId_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IId.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IId.con".
(*#*
Next, we define addition, algebraic inverse, subtraction and product of functions.
*)
-inline cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IPlus.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IPlus.con".
-inline cic:/CoRN/ftc/IntervalFunct/IInv_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IInv_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IInv.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IInv.con".
-inline cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IMinus.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IMinus.con".
-inline cic:/CoRN/ftc/IntervalFunct/IMult_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IMult.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IMult.con".
(* UNEXPORTED
-Section Nth_Power.
+Section Nth_Power
*)
(*#*
Exponentiation to a natural power [n] is also useful.
*)
-inline cic:/CoRN/ftc/IntervalFunct/n.var.
+alias id "n" = "cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var".
-inline cic:/CoRN/ftc/IntervalFunct/INth_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/INth_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/INth.con.
+inline "cic:/CoRN/ftc/IntervalFunct/INth.con".
(* UNEXPORTED
-End Nth_Power.
+End Nth_Power
*)
(*#*
*)
(* UNEXPORTED
-Section Recip_Div.
+Section Recip_Div
*)
(* begin show *)
-inline cic:/CoRN/ftc/IntervalFunct/Hg.var.
+alias id "Hg" = "cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var".
(* end show *)
-inline cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IRecip.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IRecip.con".
-inline cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IDiv.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IDiv.con".
(* UNEXPORTED
-End Recip_Div.
+End Recip_Div
*)
(*#*
Absolute value will also be needed at some point.
*)
-inline cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IAbs.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IAbs.con".
(* UNEXPORTED
-End Operations.
+End Operations
*)
(*#*
*)
(* UNEXPORTED
-Section Composition.
+Section Composition
*)
-inline cic:/CoRN/ftc/IntervalFunct/a.var.
+alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Composition/a.var".
-inline cic:/CoRN/ftc/IntervalFunct/b.var.
+alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Composition/b.var".
-inline cic:/CoRN/ftc/IntervalFunct/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var".
(* begin hide *)
-inline cic:/CoRN/ftc/IntervalFunct/I.con.
+inline "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__".
(* end hide *)
-inline cic:/CoRN/ftc/IntervalFunct/a'.var.
+alias id "a'" = "cic:/CoRN/ftc/IntervalFunct/Composition/a'.var".
-inline cic:/CoRN/ftc/IntervalFunct/b'.var.
+alias id "b'" = "cic:/CoRN/ftc/IntervalFunct/Composition/b'.var".
-inline cic:/CoRN/ftc/IntervalFunct/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var".
(* begin hide *)
-inline cic:/CoRN/ftc/IntervalFunct/I'.con.
+inline "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__".
(* end hide *)
-inline cic:/CoRN/ftc/IntervalFunct/f.var.
+alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Composition/f.var".
-inline cic:/CoRN/ftc/IntervalFunct/g.var.
+alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Composition/g.var".
-inline cic:/CoRN/ftc/IntervalFunct/Hfg.var.
+alias id "Hfg" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var".
-inline cic:/CoRN/ftc/IntervalFunct/IComp_strext.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con".
-inline cic:/CoRN/ftc/IntervalFunct/IComp.con.
+inline "cic:/CoRN/ftc/IntervalFunct/IComp.con".
(* UNEXPORTED
-End Composition.
+End Composition
*)
(* UNEXPORTED