X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs.ma;h=80ed1c0814d82c92e7bf45be0a952ebb37045a3b;hb=775106f04b47236bf47e4321d745ec360ab4ebb4;hp=9c0cc9c4a2ae74c7192ec287ed326945f0c41f67;hpb=cafb43926d8553c5b7f8dafcb5d734783c19bbfb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 9c0cc9c4a..80ed1c081 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -44,6 +44,16 @@ definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
                               ∀L1. L0 ⪤*[RP1, T0] L1 → ∀L2. L0 ⪤*[RP2, T0] L2 →
                               ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
+definition lfxs_confluent: relation … ≝
+                           λR1,R2. 
+                           ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V →
+                           ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2.
+
+definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝
+                            λR1,R2,R3.
+                            ∀K1,K,V1. K1 ⪤*[R1, V1] K →
+                            ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆.