X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fsex_sex.ma;h=342530903ef3406ec58c40563878c772505f76c4;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hp=c1954b1a789f00b113efbbd08973972c36a51afd;hpb=f308429a0fde273605a2330efc63268b4ac36c99;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
index c1954b1a7..342530903 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/rtmap_sand.ma".
+include "ground/relocation/rtmap_sand.ma".
 include "static_2/relocation/drops.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
@@ -21,8 +21,8 @@ include "static_2/relocation/drops.ma".
 
 theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
                       ∀L1,f.
-                      (∀g,I,K,n. ⬇*[n] L1 ≘ K.ⓘ{I} → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
-                      (∀g,I,K,n. ⬇*[n] L1 ≘ K.ⓘ{I} → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
+                      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
+                      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
                       ∀L0. L1 ⪤[RN1,RP1,f] L0 →
                       ∀L2. L0 ⪤[RN2,RP2,f] L2 →
                       L1 ⪤[RN,RP,f] L2.
@@ -50,7 +50,7 @@ theorem sex_trans (RN) (RP) (f): (∀g,I,K. sex_transitive RN RN RN RN RP g K I)
                                  Transitive … (sex RN RP f).
 /2 width=9 by sex_trans_gen/ qed-.
 
-theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈⦃f⦄ →
+theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ →
                             ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2.
 #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
 [ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ]
@@ -62,8 +62,8 @@ qed-.
 
 theorem sex_conf (RN1) (RP1) (RN2) (RP2):
                  ∀L,f.
-                 (∀g,I,K,n. ⬇*[n] L ≘ K.ⓘ{I} → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
-                 (∀g,I,K,n. ⬇*[n] L ≘ K.ⓘ{I} → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
+                 (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
+                 (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
                  pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
 #RN1 #RP1 #RN2 #RP2 #L elim L -L
 [ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1
@@ -82,6 +82,30 @@ theorem sex_conf (RN1) (RP1) (RN2) (RP2):
 ]
 qed-.
 
+lemma sex_repl (RN) (RP) (SN) (SP) (L1) (f):
+      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_replace3_sex … RN SN RN RP SN SP g K1 I) →
+      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_replace3_sex … RP SP RN RP SN SP g K1 I) →
+      ∀L2. L1 ⪤[RN,RP,f] L2 → ∀K1. L1 ⪤[SN,SP,f] K1 →
+      ∀K2. L2 ⪤[SN,SP,f] K2 → K1 ⪤[RN,RP,f] K2.
+#RN #RP #SN #SP #L1 elim L1 -L1
+[ #f #_ #_ #Y #HY #Y1 #HY1 #Y2 #HY2
+  lapply (sex_inv_atom1 … HY) -HY #H destruct
+  lapply (sex_inv_atom1 … HY1) -HY1 #H destruct
+  lapply (sex_inv_atom1 … HY2) -HY2 #H destruct //
+| #L1 #I1 #IH #f elim (pn_split f) * #g #H destruct
+  #HN #HP #Y #HY #Y1 #HY1 #Y2 #HY2
+  [ elim (sex_inv_push1 … HY) -HY #I2 #L2 #HL12 #HI12 #H destruct
+    elim (sex_inv_push1 … HY1) -HY1 #J1 #K1 #HLK1 #HIJ1 #H destruct
+    elim (sex_inv_push1 … HY2) -HY2 #J2 #K2 #HLK2 #HIJ2 #H destruct
+    /5 width=13 by sex_push, drops_refl, drops_drop/
+  | elim (sex_inv_next1 … HY) -HY #I2 #L2 #HL12 #HI12 #H destruct
+    elim (sex_inv_next1 … HY1) -HY1 #J1 #K1 #HLK1 #HIJ1 #H destruct
+    elim (sex_inv_next1 … HY2) -HY2 #J2 #K2 #HLK2 #HIJ2 #H destruct
+    /5 width=13 by sex_next, drops_refl, drops_drop/
+  ]
+]
+qed-.
+
 theorem sex_canc_sn: ∀RN,RP,f. Transitive … (sex RN RP f) →
                                symmetric … (sex RN RP f) →
                                left_cancellable … (sex RN RP f).