X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freduction%2Flcpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freduction%2Flcpr.ma;h=f01daabceebe6589b793835b561b88b415913897;hb=55dc00c1c44cc21c7ae179cb9df03e7446002c46;hp=0000000000000000000000000000000000000000;hpb=5b03651298a3943b67f49fb78dc30bb8b2780f30;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma
new file mode 100644
index 000000000..f01daabce
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/lcpr.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic-2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+inductive lcpr: relation lenv ≝
+| lcpr_sort: lcpr (⋆) (⋆)
+| lcpr_item: ∀K1,K2,I,V1,V2.
+             lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+  "context-sensitive parallel reduction (environment)"
+  'CPRed L1 L2 = (lcpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+                         ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 * -L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+lemma lcpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⊢ ⇒ L2 →
+                      ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/2/ qed.