X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_equivalence%2Fcpcs.ma;h=21d9864ce3461d702bdbb31bafcc725b02b5c5dd;hb=62d0f5f2c89830ebe884e6afee91eb68b68790fc;hp=0a9de4f23c49f81b463a7fc8e6e40fb07ec90914;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
index 0a9de4f23..21d9864ce 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/star.ma".
+include "ground/lib/star.ma".
 include "basic_2/notation/relations/pconvstar_5.ma".
 include "basic_2/rt_conversion/cpc.ma".
 
@@ -29,16 +29,16 @@ interpretation "context-sensitive parallel r-equivalence (term)"
 (* Basic_2A1: was: cpcs_ind_dx *)
 lemma cpcs_ind_sn (h) (G) (L) (T2):
                   ∀Q:predicate term. Q T2 →
-                  (∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T → ❪G,L❫ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
-                  ∀T1. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T1.
+                  (∀T1,T. ❨G,L❩ ⊢ T1 ⬌[h] T → ❨G,L❩ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
+                  ∀T1. ❨G,L❩ ⊢ T1 ⬌*[h] T2 → Q T1.
 normalize /3 width=6 by TC_star_ind_dx/
 qed-.
 
 (* Basic_2A1: was: cpcs_ind *)
 lemma cpcs_ind_dx (h) (G) (L) (T1):
                   ∀Q:predicate term. Q T1 →
-                  (∀T,T2. ❪G,L❫ ⊢ T1 ⬌*[h] T → ❪G,L❫ ⊢ T ⬌[h] T2 → Q T → Q T2) →
-                  ∀T2. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T2.
+                  (∀T,T2. ❨G,L❩ ⊢ T1 ⬌*[h] T → ❨G,L❩ ⊢ T ⬌[h] T2 → Q T → Q T2) →
+                  ∀T2. ❨G,L❩ ⊢ T1 ⬌*[h] T2 → Q T2.
 normalize /3 width=6 by TC_star_ind/
 qed-.
 
@@ -54,50 +54,50 @@ lemma cpcs_sym (h) (G) (L): symmetric … (cpcs h G L).
 /2 width=1 by cpc_sym/
 qed-.
 
-lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ❨G,L❩ ⊢ T1 ⬌[h] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /2 width=1 by inj/ qed.
 
 (* Basic_2A1: was: cpcs_strap2 *)
-lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T →
-                                ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ⬌[h] T →
+                                ∀T2. ❨G,L❩ ⊢ T ⬌*[h] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by TC_strap/
 qed-.
 
 (* Basic_2A1: was: cpcs_strap1 *)
-lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
-                                ∀T2. ❪G,L❫ ⊢ T ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ⬌*[h] T →
+                                ∀T2. ❨G,L❩ ⊢ T ⬌[h] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by step/
 qed-.
 
 (* Basic_1: was: pc3_pr2_r *)
-lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ❨G,L❩ ⊢ T1 ➡[h,0] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=1 by cpc_cpcs, or_introl/ qed.
 
 (* Basic_1: was: pc3_pr2_x *)
-lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T2 ➡[h] T1 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ❨G,L❩ ⊢ T2 ➡[h,0] T1 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=1 by cpc_cpcs, or_intror/ qed.
 
 (* Basic_1: was: pc3_pr2_u *)
 (* Basic_2A1: was: cpcs_cpr_strap2 *)
-lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T → ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ➡[h,0] T → ∀T2. ❨G,L❩ ⊢ T ⬌*[h] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_sn, or_introl/ qed-.
 
 (* Basic_2A1: was: cpcs_cpr_strap1 *)
-lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
-                                    ∀T2. ❪G,L❫ ⊢ T ➡[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ⬌*[h] T →
+                                    ∀T2. ❨G,L❩ ⊢ T ➡[h,0] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_introl/ qed-.
 
-lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
-                                ∀T2. ❪G,L❫ ⊢ T2 ➡[h] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ⬌*[h] T →
+                                ∀T2. ❨G,L❩ ⊢ T2 ➡[h,0] T → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_intror/ qed-.
 
-lemma cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h] T →
-                           ∀T2. ❪G,L❫ ⊢ T2 ➡[h] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpr_div (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T1 ➡[h,0] T →
+                           ∀T2. ❨G,L❩ ⊢ T2 ➡[h,0] T → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-.
 
 (* Basic_1: was: pc3_pr2_u2 *)
-lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T ➡[h] T1 →
-                                 ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ❨G,L❩ ⊢ T ➡[h,0] T1 →
+                                 ∀T2. ❨G,L❩ ⊢ T ⬌*[h] T2 → ❨G,L❩ ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_sn, or_intror/ qed-.
 
 (* Basic_1: removed theorems 9: