X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs.ma;h=b002e073af1af7be489b4f845d88376be49088cf;hb=632c54beaf67e68a1eeeec22274466157003b779;hp=3a779a649182b05ca4917e1aa643e21f6ec2c6c4;hpb=984856dbab870ddc3156040df69b1f1846cc3aaf;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index 3a779a649..b002e073a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -14,7 +14,7 @@
 
 include "ground_2/relocation/rtmap_sle.ma".
 include "basic_2/notation/relations/relationstar_5.ma".
-include "basic_2/grammar/lenv.ma".
+include "basic_2/syntax/lenv.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
 
@@ -32,12 +32,14 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝
 interpretation "generic entrywise extension (local environment)"
    'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
 
-definition lexs_confluent: relation6 (relation3 lenv term term)
-                                     (relation3 lenv term term) … ≝
-                           λR1,R2,RN1,RP1,RN2,RP2.
-                           ∀f,L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
-                           ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 →
-                           ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition R_pw_confluent2_lexs: relation3 lenv term term → relation3 lenv term term →
+                                 relation3 lenv term term → relation3 lenv term term →
+                                 relation3 lenv term term → relation3 lenv term term →
+                                 relation3 rtmap lenv term ≝
+                                 λR1,R2,RN1,RP1,RN2,RP2,f,L0,T0.
+                                 ∀T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+                                 ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 →
+                                 ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
 definition lexs_transitive: relation5 (relation3 lenv term term)
                                       (relation3 lenv term term) … ≝
@@ -171,16 +173,23 @@ lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⦻*[RN, RP, f]
 #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *)
 qed-.
 
-(* Note: fexs_sym and fexs_trans hold, but lexs_sym and lexs_trans do not  *)
 (* Basic_2A1: includes: lpx_sn_refl *)
-lemma lexs_refl: ∀RN,RP,f.
+lemma lexs_refl: ∀RN,RP.
                  (∀L. reflexive … (RN L)) →
                  (∀L. reflexive … (RP L)) →
-                 reflexive … (lexs RN RP f).
-#RN #RP #f #HRN #HRP #L generalize in match f; -f elim L -L //
+                 ∀f.reflexive … (lexs RN RP f).
+#RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
 #L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/
 qed.
 
+lemma lexs_sym: ∀RN,RP.
+                (∀L1,L2,T1,T2. RN L1 T1 T2 → RN L2 T2 T1) →
+                (∀L1,L2,T1,T2. RP L1 T1 T2 → RP L2 T2 T1) →
+                ∀f. symmetric … (lexs RN RP f).
+#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
+/3 width=2 by lexs_next, lexs_push/
+qed-.
+
 lemma lexs_pair_repl: ∀RN,RP,f,I,L1,L2,V1,V2.
                       L1.ⓑ{I}V1 ⦻*[RN, RP, f] L2.ⓑ{I}V2 →
                       ∀W1,W2. RN L1 W1 W2 → RP L1 W1 W2 →
@@ -197,6 +206,17 @@ lemma lexs_co: ∀RN1,RP1,RN2,RP2.
 /3 width=1 by lexs_atom, lexs_next, lexs_push/
 qed-.
 
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
+                    (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) →
+                    ∀f,L1,L2. L1 ⦻*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
+                    L1 ⦻*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
+#f #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+] 
+qed-.
+
 lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
                       ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 →
                       ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
@@ -222,3 +242,16 @@ lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) →
   #g2 #H #H2 destruct /3 width=5 by lexs_next/
 ]
 qed-.
+
+lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+                      ∀f,L1,L2. L1 ⦻*[R1, RP, f] L2 → ∀g. f ⊆ g →
+                      ∃∃L. L1 ⦻*[R1, RP, g] L & L ⦻*[R2, cfull, f] L2.
+#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
+[ /2 width=3 by lexs_atom, ex2_intro/ ]
+#f #I #L1 #L2 #V1 #V2 #_ #HV12 #IH #y #H
+[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+  elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, ex2_intro/
+| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+  elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+]
+qed-.