X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftpr.ma;h=79d8df114a028a4d813a108471d15ae2f155484e;hb=cb38da6095e3af84131a3ebf47a9f252f34a804c;hp=db2e187c21ec2685b81c5e11f7f298fbfe57ab5c;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
index db2e187c2..79d8df114 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
@@ -24,13 +24,13 @@ inductive tpr: relation term ≝
 | tpr_beta : ∀V1,V2,W,T1,T2.
              tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
 | tpr_delta: ∀I,V1,V2,T1,T2,T.
-             tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
+             tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
              tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
              tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
              tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
 | tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
-| tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓣV. T1) T2
+| tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
 .
 
 interpretation
@@ -39,8 +39,7 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
-                                ⓑ{I} V1. T1 ➡  ⓑ{I} V2. T2.
+lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{I} V1. T1 ➡  ⓑ{I} V2. T2.
 /2 width=3/ qed.
 
 (* Basic_1: was by definition: pr0_refl *)
@@ -69,7 +68,7 @@ lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
 
 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
                         (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                    ⋆.  ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+                                    ⋆.  ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
                                     U2 = ⓑ{I} V2. T
                         ) ∨
                         ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
@@ -86,7 +85,7 @@ qed.
 
 lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
                      (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+                                 ⋆.  ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
                                  U2 = ⓑ{I} V2. T
                      ) ∨
                      ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
@@ -95,7 +94,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
 (* Basic_1: was pr0_gen_abbr *)
 lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
                      (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  ⓓV2 ⊢ T2 [0, 1] ▶ T &
+                                 ⋆.  ⓓV2 ⊢ T2 ▶ [0, 1] T &
                                  U2 = ⓓV2. T
                       ) ∨
                       ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
@@ -156,7 +155,7 @@ elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
 qed-.
 
 (* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
                             ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
                                      U = ⓐV2. T2.
 #V1 #T1 #U #H #HT1
@@ -170,8 +169,8 @@ elim (tpr_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 →
-                       (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓣV2. T2)
+lemma tpr_inv_cast1: ∀V1,T1,U2. ⓝV1. T1 ➡ U2 →
+                       (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓝV2. T2)
                      ∨ T1 ➡ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_flat1 … H) -H * /3 width=5/
@@ -184,7 +183,7 @@ fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
                         ∨∨           T1 = #i
                          | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
                                      T1 = ⓓV. T
-                         | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
+                         | ∃∃V,T.    T ➡ #i & T1 = ⓝV. T.
 #T1 #T2 * -T1 -T2
 [ #I #i #H destruct /2 width=1/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
@@ -200,7 +199,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
                      ∨∨           T1 = #i
                       | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
                                   T1 = ⓓV. T
-                      | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
+                      | ∃∃V,T.    T ➡ #i & T1 = ⓝV. T.
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 3: