update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lprs_cpms.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
index c75c79f8f58085c295a11dfde865510940d0ef5a..8bfdf9432c606bf4011ca7140d51a7c731395452 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
@@ -19,22 +19,22 @@ include "basic_2/rt_computation/lprs_lpr.ma".
 (* Properties with t-bound context-sensitive rt-computarion for terms *******)
 
 lemma lprs_cpms_trans (n) (h) (G):
-                      â\88\80L2,T1,T2. â¦\83G,L2â¦\84 ⊢ T1 ➡*[n,h] T2 →
-                      â\88\80L1. â¦\83G,L1â¦\84 â\8a¢ â\9e¡*[h] L2 â\86\92 â¦\83G,L1â¦\84 ⊢ T1 ➡*[n,h] T2.
+                      â\88\80L2,T1,T2. â\9dªG,L2â\9d« ⊢ T1 ➡*[n,h] T2 →
+                      â\88\80L1. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h] L2 â\86\92 â\9dªG,L1â\9d« ⊢ T1 ➡*[n,h] T2.
 #n #h #G #L2 #T1 #T2 #HT12 #L1 #H
 @(lprs_ind_sn … H) -L1 /2 width=3 by lpr_cpms_trans/
 qed-.
 
 lemma lprs_cpm_trans (n) (h) (G):
-                     â\88\80L2,T1,T2. â¦\83G,L2â¦\84 ⊢ T1 ➡[n,h] T2 →
-                     â\88\80L1. â¦\83G,L1â¦\84 â\8a¢ â\9e¡*[h] L2 â\86\92 â¦\83G,L1â¦\84 ⊢ T1 ➡*[n,h] T2.
+                     â\88\80L2,T1,T2. â\9dªG,L2â\9d« ⊢ T1 ➡[n,h] T2 →
+                     â\88\80L1. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h] L2 â\86\92 â\9dªG,L1â\9d« ⊢ T1 ➡*[n,h] T2.
 /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
 
 (* Basic_2A1: includes cprs_bind2 *)
 lemma cpms_bind_dx (n) (h) (G) (L):
-                   â\88\80V1,V2. â¦\83G,Lâ¦\84 ⊢ V1 ➡*[h] V2 →
-                   â\88\80I,T1,T2. â¦\83G,L.â\93\91{I}V2â¦\84 ⊢ T1 ➡*[n,h] T2 →
-                   â\88\80p. â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡*[n,h] â\93\91{p,I}V2.T2.
+                   â\88\80V1,V2. â\9dªG,Lâ\9d« ⊢ V1 ➡*[h] V2 →
+                   â\88\80I,T1,T2. â\9dªG,L.â\93\91[I]V2â\9d« ⊢ T1 ➡*[n,h] T2 →
+                   â\88\80p. â\9dªG,Lâ\9d« â\8a¢ â\93\91[p,I]V1.T1 â\9e¡*[n,h] â\93\91[p,I]V2.T2.
 /4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed.
 
 (* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *)
@@ -43,9 +43,9 @@ lemma cpms_bind_dx (n) (h) (G) (L):
 (* Basic_2A1: includes: cprs_inv_abst1 *)
 (* Basic_2A1: uses: scpds_inv_abst1 *)
 lemma cpms_inv_abst_sn (n) (h) (G) (L):
-                       â\88\80p,V1,T1,X2. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 ➡*[n,h] X2 →
-                       â\88\83â\88\83V2,T2. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V2 & â¦\83G,L.â\93\9bV1â¦\84 ⊢ T1 ➡*[n,h] T2 &
-                                X2 = ⓛ{p}V2.T2.
+                       â\88\80p,V1,T1,X2. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]V1.T1 ➡*[n,h] X2 →
+                       â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h] V2 & â\9dªG,L.â\93\9bV1â\9d« ⊢ T1 ➡*[n,h] T2 &
+                                X2 = ⓛ[p]V2.T2.
 #n #h #G #L #p #V1 #T1 #X2 #H
 @(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
 #n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
@@ -54,8 +54,8 @@ elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
 qed-.
 
 lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
-                            â\88\80T,X. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}W.T ➡*[n,h] X →
-                            â\88\83â\88\83U. â¦\83G,L.â\93\9bWâ¦\84â\8a¢ T â\9e¡*[n,h] U & â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}W.U ➡*[h] X.
+                            â\88\80T,X. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]W.T ➡*[n,h] X →
+                            â\88\83â\88\83U. â\9dªG,L.â\93\9bWâ\9d«â\8a¢ T â\9e¡*[n,h] U & â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]W.U ➡*[h] X.
 #h #n #p #G #L #W #T #X #H
 elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
 @(ex2_intro … HTU) /2 width=1 by cpms_bind/
@@ -63,8 +63,8 @@ qed-.
 
 (* Basic_2A1: includes: cprs_inv_abst *)
 lemma cpms_inv_abst_bi (n) (h) (p1) (p2) (G) (L):
-                       â\88\80W1,W2,T1,T2. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p1}W1.T1 â\9e¡*[n,h] â\93\9b{p2}W2.T2 →
-                       â\88§â\88§ p1 = p2 & â¦\83G,Lâ¦\84 â\8a¢ W1 â\9e¡*[h] W2 & â¦\83G,L.â\93\9bW1â¦\84 ⊢ T1 ➡*[n,h] T2.
+                       â\88\80W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p1]W1.T1 â\9e¡*[n,h] â\93\9b[p2]W2.T2 →
+                       â\88§â\88§ p1 = p2 & â\9dªG,Lâ\9d« â\8a¢ W1 â\9e¡*[h] W2 & â\9dªG,L.â\93\9bW1â\9d« ⊢ T1 ➡*[n,h] T2.
 #n #h #p1 #p2 #G #L #W1 #W2 #T1 #T2 #H
 elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct
 /2 width=1 by and3_intro/
@@ -73,9 +73,9 @@ qed-.
 (* Basic_1: was pr3_gen_abbr *)
 (* Basic_2A1: includes: cprs_inv_abbr1 *)
 lemma cpms_inv_abbr_sn_dx (n) (h) (G) (L):
-                          â\88\80p,V1,T1,X2. â¦\83G,Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 ➡*[n,h] X2 →
-                          â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V2 & â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n,h] T2 & X2 = â\93\93{p}V2.T2
-                           | â\88\83â\88\83T2. â¦\83G,L.â\93\93V1â¦\84 ⊢ T1 ➡*[n ,h] T2 & ⇧*[1] X2 ≘ T2 & p = Ⓣ.
+                          â\88\80p,V1,T1,X2. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p]V1.T1 ➡*[n,h] X2 →
+                          â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h] V2 & â\9dªG,L.â\93\93V1â\9d« â\8a¢ T1 â\9e¡*[n,h] T2 & X2 = â\93\93[p]V2.T2
+                           | â\88\83â\88\83T2. â\9dªG,L.â\93\93V1â\9d« ⊢ T1 ➡*[n ,h] T2 & ⇧*[1] X2 ≘ T2 & p = Ⓣ.
 #n #h #G #L #p #V1 #T1 #X2 #H
 @(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
 #n1 #n2 #X #X2 #_ * *
@@ -95,8 +95,8 @@ qed-.
 
 (* Basic_2A1: uses: scpds_inv_abbr_abst *)
 lemma cpms_inv_abbr_abst (n) (h) (G) (L):
-                         â\88\80p1,p2,V1,W2,T1,T2. â¦\83G,Lâ¦\84 â\8a¢ â\93\93{p1}V1.T1 â\9e¡*[n,h] â\93\9b{p2}W2.T2 →
-                         â\88\83â\88\83T. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n,h] T & â\87§*[1] â\93\9b{p2}W2.T2 ≘ T & p1 = Ⓣ.
+                         â\88\80p1,p2,V1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p1]V1.T1 â\9e¡*[n,h] â\93\9b[p2]W2.T2 →
+                         â\88\83â\88\83T. â\9dªG,L.â\93\93V1â\9d« â\8a¢ T1 â\9e¡*[n,h] T & â\87§*[1] â\93\9b[p2]W2.T2 ≘ T & p1 = Ⓣ.
 #n #h #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
 elim (cpms_inv_abbr_sn_dx … H) -H *
 [ #V #T #_ #_ #H destruct