]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma
- advances on free variables allow to reduce lleq_lpx_trans to llor_total :)
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lleq_llor.ma
index 2a31fece3ef91b93a59ff655b972a9f9ef9c510a..253cb294abf924916fd8eef92cfca6072ae96e74 100644 (file)
 (**************************************************************************)
 
 include "basic_2/multiple/llor.ma".
+include "basic_2/multiple/llpx_sn_frees.ma".
 include "basic_2/multiple/lleq_alt.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
 (* Properties on poinwise union for local environments **********************)
 
-lemma llpx_sn_llor_dx: āˆ€R,L1,L2.
-                       (āˆ€U,i. L2 āŠ¢ i Ļµ š…*[0]ā¦ƒUā¦„ ā†’ L1 āŠ¢ i Ļµ š…*[0]ā¦ƒUā¦„) ā†’
-                       āˆ€T. llpx_sn R 0 T L1 L2 ā†’ āˆ€L. L1 ā©–[T] L2 ā‰” L ā†’ L2 ā‰”[T, 0] L.
-#R #L1 #L2 #HR #T #H1 #L #H2
+lemma llpx_sn_llor_dx: āˆ€R. (s_r_confluent1 ā€¦ R (llpx_sn R 0)) ā†’ (frees_trans R) ā†’
+                       āˆ€L1,L2,T,d. llpx_sn R d T L1 L2 ā†’ āˆ€L. L1 ā©–[T, d] L2 ā‰” L ā†’ L2 ā‰”[T, d] L.
+#R #H1R #H2R #L1 #L2 #T #d #H1 #L #H2
+lapply (llpx_sn_frees_trans ā€¦ H1R H2R ā€¦ H1) -H1R -H2R #HR
 elim (llpx_sn_llpx_sn_alt ā€¦ H1) -H1 #HL12 #IH1
 elim H2 -H2 #_ #HL1 #IH2
 @lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
@@ -30,5 +31,11 @@ lapply (ldrop_fwd_length_lt2 ā€¦ HLK) #HiL
 elim (ldrop_O1_lt (ā’») L1 i) // -HiL #I1 #K1 #V1 #HLK1
 elim (IH1 ā€¦ HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
 elim (IH2 ā€¦ HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
-elim H -H /2 width=1 by/
+[ elim (ylt_yle_false ā€¦ H) -H //
+| elim H -H /2 width=1 by/
+]
 qed.
+
+lemma llpx_sn_llor_dx_sym: āˆ€R. (s_r_confluent1 ā€¦ R (llpx_sn R 0)) ā†’ (frees_trans R) ā†’
+                           āˆ€L1,L2,T,d. llpx_sn R d T L1 L2 ā†’ āˆ€L. L1 ā©–[T, d] L2 ā‰” L ā†’ L ā‰”[T, d] L2.
+/3 width=6 by llpx_sn_llor_dx, lleq_sym/ qed.