more results on strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / cprs_cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
index e198001045b9f727e571dcf427ad0af18cd9e147..9f8d517e267cfc0e27879e6ebc60e4ba907f53e1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
@@ -17,6 +17,28 @@ include "Basic_2/computation/cprs_lcpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
 
+(* Advanced properties ******************************************************)
+
+lemma cprs_abbr_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
+                    L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1
+[ /3 width=1/
+| #T1 #T #HT1 #_ #IHT1
+  @(cprs_strap2 … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
+                L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+/3 width=1/ qed.
+
+(* Basic_1: was only: pr3_pr2_pr3_t *)
+lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
+                       ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT2 /3 width=5/
+qed.
+
 (* Main propertis ***********************************************************)
 
 (* Basic_1: was: pr3_t *)
@@ -28,17 +50,3 @@ theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 →
                    ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0.
 /3 width=3/ qed.
 
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was only: pr3_pr2_pr3_t *)
-lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
-                       ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT2 /3 width=5/
-qed.
-
-lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
-                L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
-#L #V1 #V2 #HV12 #T1 #T2 #HT12
-@(cprs_strap2 … (ⓓV1.T2)) /2 width=1/ /3 width=1/
-qed.