partial commit: "computation" component ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lprs_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
index 753504dc854af504693c2f163a1e3b5286c559a7..315ee8f7ad6eca0e6e9f99ef4e01ea7e98654f0f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
@@ -12,35 +12,36 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/predsnstaralt_2.ma".
+include "basic_2/notation/relations/predsnstaralt_3.ma".
 include "basic_2/computation/cprs_cprs.ma".
 include "basic_2/computation/lprs.ma".
 
 (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
 
 (* alternative definition *)
-definition lprsa: relation lenv ≝ lpx_sn … cprs.
+definition lprsa: relation3 genv lenv lenv ≝
+           λG. lpx_sn … (cprs G).
 
 interpretation "parallel computation (local environment, sn variant) alternative"
-   'PRedSnStarAlt L1 L2 = (lprsa L1 L2).
+   'PRedSnStarAlt G L1 L2 = (lprsa G L1 L2).
 
 (* Main properties on the alternative definition ****************************)
 
-theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2.
+theorem lprsa_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
 /2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
 
 (* Main inversion lemmas on the alternative definition **********************)
 
-theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2.
+theorem lprs_inv_lprsa: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡➡* L2.
 /3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
 
 (* Alternative eliminators **************************************************)
 
-lemma lprs_ind_alt: ∀R:relation lenv.
+lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
                     R (⋆) (⋆) → (
                        ∀I,K1,K2,V1,V2.
-                       K1 ⊢ ➡* K2 → K1 ⊢ V1 ➡* V2 →
+                       ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 →
                        R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
                     ) →
-                    ∀L1,L2. L1 ⊢ ➡* L2 → R L1 L2.
+                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2.
 /3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-.