diamond property of reduction!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index b3c7a7fe06e8d24c8164bf582743c0ad46004757..88a8bd542182ff72e19c288ded5cbe5915d3a725 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -26,6 +26,13 @@ definition lfxs (R) (T): relation lenv ≝
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
 
+definition lfxs_confluent: relation4 (relation3 lenv term term)
+                                     (relation3 lenv term term) … ≝
+                           λR1,R2,RP1,RP2.
+                           ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+                           ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+                           ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+
 (* Basic properties ***********************************************************)
 
 lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆.
@@ -52,6 +59,14 @@ lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l.
 #R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/
 qed.
 
+lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1.
+                         L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 →
+                         ∀V2. R L1 V V2 →
+                         L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR
+/3 width=5 by lexs_pair_repl, ex2_intro/
+qed-.
+
 lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
                ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2.
 #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/