X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_cpms.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_cpms.ma;h=0b01d3843ef264a47888f89f9c3bc658483ff75f;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=4e6732f13baeae9a27755e075b53013106739b9d;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

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 4e6732f13..0b01d3843 100644
--- 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,23 +19,23 @@ include "basic_2/rt_computation/lprs_lpr.ma".
 (* Properties with t-bound context-sensitive rt-computarion for terms *******)
 
 lemma lprs_cpms_trans (h) (n) (G) (T1:term) (T2:term):
-      ∀L2. ❪G,L2❫ ⊢ T1 ➡*[h,n] T2 →
-      ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ T1 ➡*[h,n] T2.
+      ∀L2. ❨G,L2❩ ⊢ T1 ➡*[h,n] T2 →
+      ∀L1. ❨G,L1❩ ⊢ ➡*[h,0] L2 → ❨G,L1❩ ⊢ T1 ➡*[h,n] T2.
 #h #n #G #T1 #T2 #L2 #HT12 #L1 #H
 @(lprs_ind_sn … H) -L1
 /2 width=3 by lpr_cpms_trans/
 qed-.
 
 lemma lprs_cpm_trans (h) (n) (G) (T1:term) (T2:term):
-      ∀L2. ❪G,L2❫ ⊢ T1 ➡[h,n] T2 →
-      ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ T1 ➡*[h,n] T2.
+      ∀L2. ❨G,L2❩ ⊢ T1 ➡[h,n] T2 →
+      ∀L1. ❨G,L1❩ ⊢ ➡*[h,0] L2 → ❨G,L1❩ ⊢ T1 ➡*[h,n] T2.
 /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
 
 (* Basic_2A1: includes cprs_bind2 *)
 lemma cpms_bind_alt (h) (n) (G) (L):
-      ∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 →
-      ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ➡*[h,n] T2 →
-      ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.
+      ∀V1,V2. ❨G,L❩ ⊢ V1 ➡*[h,0] V2 →
+      ∀I,T1,T2. ❨G,L.ⓑ[I]V2❩ ⊢ T1 ➡*[h,n] T2 →
+      ∀p. ❨G,L❩ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[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 *)
@@ -44,8 +44,8 @@ lemma cpms_bind_alt (h) (n) (G) (L):
 (* Basic_2A1: includes: cprs_inv_abst1 *)
 (* Basic_2A1: uses: scpds_inv_abst1 *)
 lemma cpms_inv_abst_sn (h) (n) (G) (L):
-      ∀p,V1,T1,X2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ➡*[h,n] X2 →
-      ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓛ[p]V2.T2.
+      ∀p,V1,T1,X2. ❨G,L❩ ⊢ ⓛ[p]V1.T1 ➡*[h,n] X2 →
+      ∃∃V2,T2. ❨G,L❩ ⊢ V1 ➡*[h,0] V2 & ❨G,L.ⓛV1❩ ⊢ T1 ➡*[h,n] T2 & X2 = ⓛ[p]V2.T2.
 #h #n #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):
-      ∀T,X. ❪G,L❫ ⊢ ⓛ[p]W.T ➡*[h,n] X →
-      ∃∃U. ❪G,L.ⓛW❫⊢ T ➡*[h,n] U & ❪G,L❫ ⊢ ⓛ[p]W.U ➡*[h,0] X.
+      ∀T,X. ❨G,L❩ ⊢ ⓛ[p]W.T ➡*[h,n] X →
+      ∃∃U. ❨G,L.ⓛW❩⊢ T ➡*[h,n] U & ❨G,L❩ ⊢ ⓛ[p]W.U ➡*[h,0] 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 (h) (n) (p1) (p2) (G) (L):
-      ∀W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
-      ∧∧ p1 = p2 & ❪G,L❫ ⊢ W1 ➡*[h,0] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ➡*[h,n] T2.
+      ∀W1,W2,T1,T2. ❨G,L❩ ⊢ ⓛ[p1]W1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
+      ∧∧ p1 = p2 & ❨G,L❩ ⊢ W1 ➡*[h,0] W2 & ❨G,L.ⓛW1❩ ⊢ T1 ➡*[h,n] T2.
 #h #n #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 (h) (n) (G) (L):
-      ∀p,V1,T1,X2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
-      ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
-       | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
+      ∀p,V1,T1,X2. ❨G,L❩ ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
+      ∨∨ ∃∃V2,T2. ❨G,L❩ ⊢ V1 ➡*[h,0] V2 & ❨G,L.ⓓV1❩ ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
+       | ∃∃T2. ❨G,L.ⓓV1❩ ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
 #h #n #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 (h) (n) (G) (L):
-      ∀p1,p2,V1,W2,T1,T2. ❪G,L❫ ⊢ ⓓ[p1]V1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
-      ∃∃T. ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T & ⇧[1] ⓛ[p2]W2.T2 ≘ T & p1 = Ⓣ.
+      ∀p1,p2,V1,W2,T1,T2. ❨G,L❩ ⊢ ⓓ[p1]V1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
+      ∃∃T. ❨G,L.ⓓV1❩ ⊢ T1 ➡*[h,n] T & ⇧[1] ⓛ[p2]W2.T2 ≘ T & p1 = Ⓣ.
 #h #n #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
 elim (cpms_inv_abbr_sn_dx … H) -H *
 [ #V #T #_ #_ #H destruct