X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_cr.ma;h=e71d2bd3e694e178da1a76e489579bd3d8dff816;hb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;hp=5dadd06deed5da57084a7397f05ae6afc443bfaf;hpb=0aa60d67f17b528b896e05bbd01038cbc195f69d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
index 5dadd06de..e71d2bd3e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
@@ -13,10 +13,27 @@
 (**************************************************************************)
 
 include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/csn.ma".
+include "Basic_2/computation/csn_lcpr.ma".
+include "Basic_2/computation/csn_vector.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
 (* Advanced properties ******************************************************)
+(*
+lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+                       ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s * -V1s -V2s /2 width=1/
+#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/
+#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV
+lapply (csn_appl_theta … HV12 … H) -H -HV12 #H
+lapply (csn_fwd_pair_sn … H) #HV1
+@csn_appl_simple // #X #H1 #H2
+whd in ⊢ (? ? %);
+*)
+(*
+lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+              ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/
+*)
 
-axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⇓ T).
+axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).