milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / sex.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
index 49010d3305684e905ea643f6d35b3491c0780417..3fba7476ad0d087ac365539b8668024fc793e1ee 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
@@ -32,6 +32,14 @@ inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
 interpretation "generic entrywise extension (local environment)"
    'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
 
+definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
+                           relation3 lenv bind bind →
+                           relation3 lenv bind bind → relation3 lenv bind bind →
+                           relation3 rtmap lenv bind ≝
+                           λR1,R2,R3,RN,RP,f,L1,I1.
+                           ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
+                           ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
+
 definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind →
                                 relation3 lenv bind bind → relation3 lenv bind bind →
                                 relation3 lenv bind bind → relation3 lenv bind bind →
@@ -41,13 +49,14 @@ definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind
                                 ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
                                 ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
 
-definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
-                           relation3 lenv bind bind →
-                           relation3 lenv bind bind → relation3 lenv bind bind →
-                           relation3 rtmap lenv bind ≝
-                           λR1,R2,R3,RN,RP,f,L1,I1.
-                           ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
-                           ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
+definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind →
+                              relation3 lenv bind bind → relation3 lenv bind bind →
+                              relation3 lenv bind bind → relation3 lenv bind bind →
+                              relation3 rtmap lenv bind ≝
+                              λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+                              ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
+                              ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+                              ∀I. R2 L1 I1 I → R1 L2 I2 I.
 
 (* Basic inversion lemmas ***************************************************)