update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_equivalence / cpcs.ma

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 4daecd3eb0240d29a8d6a5a6ada519ea9a5d4e05..0a9de4f23c49f81b463a7fc8e6e40fb07ec90914 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.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 →
-                  (â\88\80T1,T. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\8c[h] T â\86\92 â¦\83G,Lâ¦\84 ⊢ T ⬌*[h] T2 → Q T → Q T1) →
-                  â\88\80T1. â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2 → Q T1.
+                  (â\88\80T1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\8c[h] T â\86\92 â\9dªG,Lâ\9d« ⊢ T ⬌*[h] T2 → Q T → Q T1) →
+                  â\88\80T1. â\9dªG,Lâ\9d« ⊢ 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 →
-                  (â\88\80T,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\8c*[h] T â\86\92 â¦\83G,Lâ¦\84 ⊢ T ⬌[h] T2 → Q T → Q T2) →
-                  â\88\80T2. â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2 → Q T2.
+                  (â\88\80T,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\8c*[h] T â\86\92 â\9dªG,Lâ\9d« ⊢ T ⬌[h] T2 → Q T → Q T2) →
+                  â\88\80T2. â\9dªG,Lâ\9d« ⊢ 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): â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\8c[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpc_cpcs (h) (G) (L): â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\8c[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 /2 width=1 by inj/ qed.
 
 (* Basic_2A1: was: cpcs_strap2 *)
-lemma cpcs_step_sn (h) (G) (L): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 ⬌[h] T →
-                                â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â¬\8c*[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_sn (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 ⬌[h] T →
+                                â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â¬\8c*[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by TC_strap/
 qed-.
 
 (* Basic_2A1: was: cpcs_strap1 *)
-lemma cpcs_step_dx (h) (G) (L): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T →
-                                â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â¬\8c[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_step_dx (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T →
+                                â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â¬\8c[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 normalize /2 width=3 by step/
 qed-.
 
 (* Basic_1: was: pc3_pr2_r *)
-lemma cpr_cpcs_dx (h) (G) (L): â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â\9e¡[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_dx (h) (G) (L): â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ 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): â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T2 â\9e¡[h] T1 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpr_cpcs_sn (h) (G) (L): â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T2 â\9e¡[h] T1 â\86\92 â\9dªG,Lâ\9d« ⊢ 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): â\88\80T1,T. â¦\83G,Lâ¦\84 â\8a¢ T1 â\9e¡[h] T â\86\92 â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â¬\8c*[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_sn (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h] T â\86\92 â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â¬\8c*[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ 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): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T →
-                                    â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_step_dx (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T →
+                                    â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_introl/ qed-.
 
-lemma cpcs_cpr_div (h) (G) (L): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T →
-                                â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T2 â\9e¡[h] T â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_div (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T →
+                                â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T2 â\9e¡[h] T â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_dx, or_intror/ qed-.
 
-lemma cpr_div (h) (G) (L): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 ➡[h] T →
-                           â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T2 â\9e¡[h] T â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpr_div (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 ➡[h] T →
+                           â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T2 â\9e¡[h] T â\86\92 â\9dªG,Lâ\9d« ⊢ 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): â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T ➡[h] T1 →
-                                 â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â¬\8c*[h] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2.
+lemma cpcs_cpr_conf (h) (G) (L): â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T ➡[h] T1 →
+                                 â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â¬\8c*[h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2.
 /3 width=3 by cpcs_step_sn, or_intror/ qed-.
 
 (* Basic_1: removed theorems 9: