X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frdsx.ma;h=5b62dbae165abf621a7d683fc912990e32292c76;hp=ff62c4d6b94e511383ac1428fa215b9138b6fdd0;hb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;hpb=ec261374a2990bebeded039a64c0be0795ad9e93

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
index ff62c4d6b..5b62dbae1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
@@ -13,13 +13,13 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predtysnstrong_5.ma".
-include "basic_2/static/lfdeq.ma".
+include "static_2/static/rdeq.ma".
 include "basic_2/rt_transition/lpx.ma".
 
 (* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
 
 definition rdsx (h) (o) (G) (T): predicate lenv ≝
-                                 SN … (lpx h G) (lfdeq h o T).
+                                 SN … (lpx h G) (rdeq h o T).
 
 interpretation
    "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
@@ -29,13 +29,13 @@ interpretation
 
 (* Basic_2A1: uses: lsx_ind *)
 lemma rdsx_ind (h) (o) (G) (T):
-               ∀R:predicate lenv.
+               ∀Q:predicate lenv.
                (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
-                     (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
-                     R L1
+                     (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+                     Q L1
                ) →
-               ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #H0 #L1 #H elim H -L1
+               ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ →  Q L.
+#h #o #G #T #Q #H0 #L1 #H elim H -L1
 /5 width=1 by SN_intro/
 qed-.
 
@@ -57,7 +57,7 @@ lemma rdsx_fwd_pair_sn (h) (o) (G):
 #h #o #G #I #L #V #T #H
 @(rdsx_ind … H) -L #L1 #_ #IHL1
 @rdsx_intro #L2 #HL12 #HnL12
-/4 width=3 by lfdeq_fwd_pair_sn/
+/4 width=3 by rdeq_fwd_pair_sn/
 qed-.
 
 (* Basic_2A1: uses: lsx_fwd_flat_dx *)
@@ -67,14 +67,14 @@ lemma rdsx_fwd_flat_dx (h) (o) (G):
 #h #o #G #I #L #V #T #H 
 @(rdsx_ind … H) -L #L1 #_ #IHL1
 @rdsx_intro #L2 #HL12 #HnL12
-/4 width=3 by lfdeq_fwd_flat_dx/
+/4 width=3 by rdeq_fwd_flat_dx/
 qed-.
 
 fact rdsx_fwd_pair_aux (h) (o) (G): ∀L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
                                     ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
 #h #o #G #L #H
 @(rdsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
-/5 width=5 by lpx_pair, rdsx_intro, lfdeq_fwd_zero_pair/
+/5 width=5 by lpx_pair, rdsx_intro, rdeq_fwd_zero_pair/
 qed-.
 
 lemma rdsx_fwd_pair (h) (o) (G):