X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRefSeparated.ma;h=5aee670ee432c8aefa0dd7cd9cd0f4627be785ba;hb=HEAD;hp=a65a4ecdad1a6457e6efcabf6e7a5f29166a2381;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma index a65a4ecda..5aee670ee 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma @@ -16,158 +16,165 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparated". +include "CoRN.ma". + (* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *) (* begin hide *) -(* INCLUDE -COrdLemmas -*) +include "ftc/COrdLemmas.ma". -(* INCLUDE -Partitions -*) +include "ftc/Partitions.ma". (* UNEXPORTED -Section Separating__Separated. +Section Separating__Separated *) -inline cic:/CoRN/ftc/RefSeparated/a.var. +alias id "a" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/a.var". -inline cic:/CoRN/ftc/RefSeparated/b.var. +alias id "b" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/b.var". -inline cic:/CoRN/ftc/RefSeparated/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hab.var". -inline cic:/CoRN/ftc/RefSeparated/I.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/I.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/F.var. +alias id "F" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/F.var". -inline cic:/CoRN/ftc/RefSeparated/contF.var. +alias id "contF" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/contF.var". -inline cic:/CoRN/ftc/RefSeparated/incF.var. +alias id "incF" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/incF.var". -inline cic:/CoRN/ftc/RefSeparated/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hab'.var". -inline cic:/CoRN/ftc/RefSeparated/m.var. +alias id "m" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/m.var". -inline cic:/CoRN/ftc/RefSeparated/n.var. +alias id "n" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/n.var". -inline cic:/CoRN/ftc/RefSeparated/P.var. +alias id "P" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/P.var". -inline cic:/CoRN/ftc/RefSeparated/R.var. +alias id "R" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/R.var". -inline cic:/CoRN/ftc/RefSeparated/HP.var. +alias id "HP" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/HP.var". -inline cic:/CoRN/ftc/RefSeparated/HR.var. +alias id "HR" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/HR.var". -inline cic:/CoRN/ftc/RefSeparated/RS_pos_n.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_pos_n.con". -inline cic:/CoRN/ftc/RefSeparated/RS_pos_m.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_pos_m.con". -inline cic:/CoRN/ftc/RefSeparated/alpha.var. +alias id "alpha" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/alpha.var". -inline cic:/CoRN/ftc/RefSeparated/Halpha.var. +alias id "Halpha" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Halpha.var". -inline cic:/CoRN/ftc/RefSeparated/e.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/e.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/RS_He.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_He.con". -inline cic:/CoRN/ftc/RefSeparated/contF'.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/contF'.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/d.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/d.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/RS_Hd.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_Hd.con". -inline cic:/CoRN/ftc/RefSeparated/RS_Hd'.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_Hd'.con". -inline cic:/CoRN/ftc/RefSeparated/csi.var. +alias id "csi" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/csi.var". -inline cic:/CoRN/ftc/RefSeparated/Hcsi.var. +alias id "Hcsi" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hcsi.var". -inline cic:/CoRN/ftc/RefSeparated/M.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/M.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/deltaP.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/deltaP.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/deltaR.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/deltaR.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/delta.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/delta.con" "Separating__Separated__". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_d.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_d.con". -inline cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con. +inline "cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con". (* UNEXPORTED -Section Defining_ai'. +Section Defining_ai' *) -inline cic:/CoRN/ftc/RefSeparated/i.var. +alias id "i" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/i.var". -inline cic:/CoRN/ftc/RefSeparated/Hi.var. +alias id "Hi" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hi.var". -inline cic:/CoRN/ftc/RefSeparated/separation_conseq.con. +inline "cic:/CoRN/ftc/RefSeparated/separation_conseq.con". -inline cic:/CoRN/ftc/RefSeparated/pred1.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/pred1.con" "Separating__Separated__Defining_ai'__". -inline cic:/CoRN/ftc/RefSeparated/pred2.con. +inline "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/pred2.con" "Separating__Separated__Defining_ai'__". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/Hi0.var. +alias id "Hi0" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hi0.var". -inline cic:/CoRN/ftc/RefSeparated/Hin.var. +alias id "Hin" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hin.var". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_less.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_less.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con". (* UNEXPORTED -End Defining_ai'. +End Defining_ai' *) -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con". + +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_part.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_part.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con. +alias id "g" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/g.var". -inline cic:/CoRN/ftc/RefSeparated/g.var. +alias id "gP" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/gP.var". -inline cic:/CoRN/ftc/RefSeparated/gP.var. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_points.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con. +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). +*) + +(* NOTATION +Notation just2 := + (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)). +*) -inline cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con". -inline cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con. +inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con". (* UNEXPORTED -End Separating__Separated. +End Separating__Separated *) (* end hide *)