X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FIntervalFunct.ma;h=b08ef762b7c05f49f29118afddf1d91298a2469f;hb=fa0d5a79683ea3966f62b21be7e1a3e274597911;hp=9001c6b487371d5cf0f85881b316b52d63f82e7b;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma index 9001c6b48..b08ef762b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma @@ -16,14 +16,14 @@ 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 @@ -47,24 +47,24 @@ type [I -> IR]. %\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 *) (*#* @@ -74,56 +74,56 @@ Constant and identity functions are defined. %\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 *) (*#* @@ -131,37 +131,37 @@ If a function is non-zero in all the interval then we can define its multiplicat *) (* 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 *) (*#* @@ -183,45 +183,45 @@ compact interval [[a',b']], and let [g] be a setoid function of type *) (* 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