X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_cpms.ma;h=591dbd1c1eeb46bbfa180b0e09ab75f14aae0af6;hp=ad24e58761d2e5b42d3cda3895cd5823b792e551;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

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 ad24e5876..591dbd1c1 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,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):
-                      ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[n, h] T2 →
-                      ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
+                      ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ➡*[n,h] T2 →
+                      ∀L1. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L1⦄ ⊢ 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):
-                     ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 →
-                     ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
+                     ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ➡[n,h] T2 →
+                     ∀L1. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L1⦄ ⊢ 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):
-                   ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
-                   ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[n, h] T2 →
-                   ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2.
+                   ∀V1,V2. ⦃G,L⦄ ⊢ V1 ➡*[h] V2 →
+                   ∀I,T1,T2. ⦃G,L.ⓑ{I}V2⦄ ⊢ T1 ➡*[n,h] T2 →
+                   ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n,h] ⓑ{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,8 +43,8 @@ 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):
-                       ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 →
-                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 &
+                       ∀p,V1,T1,X2. ⦃G,L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n,h] X2 →
+                       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ➡*[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ 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/
@@ -63,8 +63,8 @@ qed-.
 
 (* Basic_2A1: includes: cprs_inv_abst *)
 lemma cpms_inv_abst_bi (n) (h) (p1) (p2) (G) (L):
-                       ∀W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ➡*[n, h] ⓛ{p2}W2.T2 →
-                       ∧∧ p1 = p2 & ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2.
+                       ∀W1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}W1.T1 ➡*[n,h] ⓛ{p2}W2.T2 →
+                       ∧∧ p1 = p2 & ⦃G,L⦄ ⊢ W1 ➡*[h] W2 & ⦃G,L.ⓛW1⦄ ⊢ 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):
-                          ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n, h] X2 →
-                          ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T2 & X2 = ⓓ{p}V2.T2
-                           | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n ,h] T2 & ⬆*[1] X2 ≘ T2 & p = Ⓣ.
+                          ∀p,V1,T1,X2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n,h] X2 →
+                          ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ➡*[h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓓ{p}V2.T2
+                           | ∃∃T2. ⦃G,L.ⓓV1⦄ ⊢ 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):
-                         ∀p1,p2,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n, h] ⓛ{p2}W2.T2 →
-                         ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T & ⬆*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ.
+                         ∀p1,p2,V1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n,h] ⓛ{p2}W2.T2 →
+                         ∃∃T. ⦃G,L.ⓓV1⦄ ⊢ T1 ➡*[n,h] T & ⬆*[1] ⓛ{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