X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRefSeparated.ma;h=5aee670ee432c8aefa0dd7cd9cd0f4627be785ba;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=186466579fe76361af94e195d7ac1960fc68a967;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma b/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma index 186466579..5aee670ee 100644 --- a/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma +++ b/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma @@ -27,68 +27,68 @@ include "ftc/COrdLemmas.ma". 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_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/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/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". @@ -101,24 +101,24 @@ inline "cic:/CoRN/ftc/RefSeparated/RS_delta_d.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/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/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". @@ -129,7 +129,7 @@ inline "cic:/CoRN/ftc/RefSeparated/sep__sep_less.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". @@ -150,9 +150,9 @@ inline "cic:/CoRN/ftc/RefSeparated/sep__sep_part.con". inline "cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con". -inline "cic:/CoRN/ftc/RefSeparated/g.var". +alias id "g" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/g.var". -inline "cic:/CoRN/ftc/RefSeparated/gP.var". +alias id "gP" = "cic:/CoRN/ftc/RefSeparated/Separating__Separated/gP.var". inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points.con". @@ -160,12 +160,21 @@ inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.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_Mesh.con". (* UNEXPORTED -End Separating__Separated. +End Separating__Separated *) (* end hide *)