X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRefLemma.ma;h=6034e5361c67c2ad1644410a752f60898512103b;hb=842e243be954d67360788d08701289f3237c2699;hp=e0bfd909a9f84d2e9f750b86ae2bdab3cbb474ad;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma index e0bfd909a..6034e5361 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma @@ -27,7 +27,7 @@ include "ftc/RefSeparated.ma". include "ftc/RefSepRef.ma". (* UNEXPORTED -Section Refinement_Lemma. +Section Refinement_Lemma *) (*#* *The Refinement Lemmas @@ -81,32 +81,32 @@ Using the results from these files, we prove our main lemma in several steps %\end{convention}% *) -inline "cic:/CoRN/ftc/RefLemma/a.var". +alias id "a" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var". -inline "cic:/CoRN/ftc/RefLemma/b.var". +alias id "b" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var". -inline "cic:/CoRN/ftc/RefLemma/Hab.var". +alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/I.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/F.var". +alias id "F" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var". -inline "cic:/CoRN/ftc/RefLemma/contF.var". +alias id "contF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var". -inline "cic:/CoRN/ftc/RefLemma/incF.var". +alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/contF'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__". (* end hide *) (* UNEXPORTED -Section First_Refinement_Lemma. +Section First_Refinement_Lemma *) (*#* @@ -124,43 +124,43 @@ respectively. %\end{convention}% *) -inline "cic:/CoRN/ftc/RefLemma/e.var". +alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var". -inline "cic:/CoRN/ftc/RefLemma/He.var". +alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/d.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/m.var". +alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var". -inline "cic:/CoRN/ftc/RefLemma/n.var". +alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var". -inline "cic:/CoRN/ftc/RefLemma/P.var". +alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var". -inline "cic:/CoRN/ftc/RefLemma/HMesh.var". +alias id "HMesh" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var". -inline "cic:/CoRN/ftc/RefLemma/Q.var". +alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var". -inline "cic:/CoRN/ftc/RefLemma/Href.var". +alias id "Href" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var". -inline "cic:/CoRN/ftc/RefLemma/fP.var". +alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var". -inline "cic:/CoRN/ftc/RefLemma/fQ.var". +alias id "fQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var". -inline "cic:/CoRN/ftc/RefLemma/HfQ.var". +alias id "HfQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var". -inline "cic:/CoRN/ftc/RefLemma/HfQ'.var". +alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/sub.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_sub_0.con". @@ -174,11 +174,11 @@ inline "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con". inline "cic:/CoRN/ftc/RefLemma/RL_sub_S.con". -inline "cic:/CoRN/ftc/RefLemma/H.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/H'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/H0.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con". @@ -186,8 +186,24 @@ inline "cic:/CoRN/ftc/RefLemma/RL_h.con". inline "cic:/CoRN/ftc/RefLemma/RL_g.con". +(* NOTATION +Notation g := RL_g. +*) + +(* NOTATION +Notation h := RL_h. +*) + inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con". +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)). +*) + +(* NOTATION +Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)). +*) + inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con". inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con". @@ -207,11 +223,11 @@ inline "cic:/CoRN/ftc/RefLemma/ref_calc8.con". inline "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con". (* UNEXPORTED -End First_Refinement_Lemma. +End First_Refinement_Lemma *) (* UNEXPORTED -Section Second_Refinement_Lemma. +Section Second_Refinement_Lemma *) (*#* @@ -230,62 +246,62 @@ and [R], respectively. %\end{convention}% *) -inline "cic:/CoRN/ftc/RefLemma/n.var". +alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var". -inline "cic:/CoRN/ftc/RefLemma/j.var". +alias id "j" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var". -inline "cic:/CoRN/ftc/RefLemma/k.var". +alias id "k" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var". -inline "cic:/CoRN/ftc/RefLemma/P.var". +alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var". -inline "cic:/CoRN/ftc/RefLemma/Q.var". +alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var". -inline "cic:/CoRN/ftc/RefLemma/R.var". +alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var". -inline "cic:/CoRN/ftc/RefLemma/HrefP.var". +alias id "HrefP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var". -inline "cic:/CoRN/ftc/RefLemma/HrefR.var". +alias id "HrefR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var". -inline "cic:/CoRN/ftc/RefLemma/e.var". +alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var". -inline "cic:/CoRN/ftc/RefLemma/e'.var". +alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var". -inline "cic:/CoRN/ftc/RefLemma/He.var". +alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var". -inline "cic:/CoRN/ftc/RefLemma/He'.var". +alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/d.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/d'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/HMeshP.var". +alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var". -inline "cic:/CoRN/ftc/RefLemma/HMeshR.var". +alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var". -inline "cic:/CoRN/ftc/RefLemma/fP.var". +alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var". -inline "cic:/CoRN/ftc/RefLemma/fR.var". +alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR.var". +alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR'.var". +alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var". inline "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con". (* UNEXPORTED -End Second_Refinement_Lemma. +End Second_Refinement_Lemma *) (* UNEXPORTED -Section Third_Refinement_Lemma. +Section Third_Refinement_Lemma *) (*#* @@ -304,109 +320,109 @@ respectively; %\end{convention}% *) -inline "cic:/CoRN/ftc/RefLemma/n.var". +alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var". -inline "cic:/CoRN/ftc/RefLemma/m.var". +alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var". -inline "cic:/CoRN/ftc/RefLemma/P.var". +alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var". -inline "cic:/CoRN/ftc/RefLemma/R.var". +alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var". -inline "cic:/CoRN/ftc/RefLemma/e.var". +alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var". -inline "cic:/CoRN/ftc/RefLemma/e'.var". +alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var". -inline "cic:/CoRN/ftc/RefLemma/He.var". +alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var". -inline "cic:/CoRN/ftc/RefLemma/He'.var". +alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/d.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/d'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/HMeshP.var". +alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var". -inline "cic:/CoRN/ftc/RefLemma/HMeshR.var". +alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var". -inline "cic:/CoRN/ftc/RefLemma/fP.var". +alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var". -inline "cic:/CoRN/ftc/RefLemma/fR.var". +alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR.var". +alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR'.var". +alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var". -inline "cic:/CoRN/ftc/RefLemma/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var". -inline "cic:/CoRN/ftc/RefLemma/beta.var". +alias id "beta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var". -inline "cic:/CoRN/ftc/RefLemma/Hbeta.var". +alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/alpha.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_alpha.con". -inline "cic:/CoRN/ftc/RefLemma/csi1.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_csi1.con". -inline "cic:/CoRN/ftc/RefLemma/delta1.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_delta1.con". -inline "cic:/CoRN/ftc/RefLemma/P'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con". inline "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con". -inline "cic:/CoRN/ftc/RefLemma/fP'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con". inline "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con". -inline "cic:/CoRN/ftc/RefLemma/csi2.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_csi2.con". -inline "cic:/CoRN/ftc/RefLemma/delta2.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_delta2.con". -inline "cic:/CoRN/ftc/RefLemma/R'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con". inline "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con". -inline "cic:/CoRN/ftc/RefLemma/fR'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con". inline "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con". -inline "cic:/CoRN/ftc/RefLemma/csi3.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_csi3.con". -inline "cic:/CoRN/ftc/RefLemma/Q.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con". inline "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con". -inline "cic:/CoRN/ftc/RefLemma/fQ.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__". inline "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con". @@ -417,16 +433,20 @@ inline "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con". inline "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con". (* UNEXPORTED -End Third_Refinement_Lemma. +End Third_Refinement_Lemma *) (* UNEXPORTED -Section Fourth_Refinement_Lemma. +Section Fourth_Refinement_Lemma *) (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/Fa.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__". + +(* NOTATION +Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)). +*) inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con". @@ -437,111 +457,111 @@ Finally, this is inequality (2.6.7) exactly as stated (same conventions as above) *) -inline "cic:/CoRN/ftc/RefLemma/n.var". +alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var". -inline "cic:/CoRN/ftc/RefLemma/m.var". +alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var". -inline "cic:/CoRN/ftc/RefLemma/P.var". +alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var". -inline "cic:/CoRN/ftc/RefLemma/R.var". +alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var". -inline "cic:/CoRN/ftc/RefLemma/e.var". +alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var". -inline "cic:/CoRN/ftc/RefLemma/e'.var". +alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var". -inline "cic:/CoRN/ftc/RefLemma/He.var". +alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var". -inline "cic:/CoRN/ftc/RefLemma/He'.var". +alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/d.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/d'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/HMeshP.var". +alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var". -inline "cic:/CoRN/ftc/RefLemma/HMeshR.var". +alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var". -inline "cic:/CoRN/ftc/RefLemma/fP.var". +alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var". -inline "cic:/CoRN/ftc/RefLemma/fR.var". +alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR.var". +alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR'.var". +alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var". (* begin show *) -inline "cic:/CoRN/ftc/RefLemma/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var". (* end show *) inline "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con". (* UNEXPORTED -End Fourth_Refinement_Lemma. +End Fourth_Refinement_Lemma *) (* UNEXPORTED -Section Main_Refinement_Lemma. +Section Main_Refinement_Lemma *) (*#* We finish by presenting Theorem 9. *) -inline "cic:/CoRN/ftc/RefLemma/n.var". +alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var". -inline "cic:/CoRN/ftc/RefLemma/m.var". +alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var". -inline "cic:/CoRN/ftc/RefLemma/P.var". +alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var". -inline "cic:/CoRN/ftc/RefLemma/R.var". +alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var". -inline "cic:/CoRN/ftc/RefLemma/e.var". +alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var". -inline "cic:/CoRN/ftc/RefLemma/e'.var". +alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var". -inline "cic:/CoRN/ftc/RefLemma/He.var". +alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var". -inline "cic:/CoRN/ftc/RefLemma/He'.var". +alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var". (* begin hide *) -inline "cic:/CoRN/ftc/RefLemma/d.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__". -inline "cic:/CoRN/ftc/RefLemma/d'.con". +inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__". (* end hide *) -inline "cic:/CoRN/ftc/RefLemma/HMeshP.var". +alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var". -inline "cic:/CoRN/ftc/RefLemma/HMeshR.var". +alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var". -inline "cic:/CoRN/ftc/RefLemma/fP.var". +alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var". -inline "cic:/CoRN/ftc/RefLemma/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var". -inline "cic:/CoRN/ftc/RefLemma/fR.var". +alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR.var". +alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var". -inline "cic:/CoRN/ftc/RefLemma/HfR'.var". +alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var". inline "cic:/CoRN/ftc/RefLemma/refinement_lemma.con". (* UNEXPORTED -End Main_Refinement_Lemma. +End Main_Refinement_Lemma *) (* UNEXPORTED -End Refinement_Lemma. +End Refinement_Lemma *)