X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx.ma;h=31f2e017a2ace0bb5c3cf792a1805440203f8b68;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=9ed838235de6ac14cdd1e7c9d4002efa7d9a0a10;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
index 9ed838235..31f2e017a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
@@ -18,21 +18,21 @@ include "basic_2/rt_transition/cpx.ma".
 
 (* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
 
-definition csx: ∀h. relation3 genv lenv term ≝
-                λh,G,L. SN … (cpx h G L) teqx.
+definition csx (h) (G) (L): predicate term ≝
+           SN … (cpx h G L) teqx.
 
 interpretation
-   "strong normalization for unbound context-sensitive parallel rt-transition (term)"
-   'PRedTyStrong h G L T = (csx h G L T).
+  "strong normalization for unbound context-sensitive parallel rt-transition (term)"
+  'PRedTyStrong h G L T = (csx h G L T).
 
 (* Basic eliminators ********************************************************)
 
-lemma csx_ind: ∀h,G,L. ∀Q:predicate term.
-               (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
-                     (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) →
-                     Q T1
-               ) →
-               ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ →  Q T.
+lemma csx_ind (h) (G) (L) (Q:predicate …):
+      (∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+        (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) →
+        Q T1
+      ) →
+      ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T →  Q T.
 #h #G #L #Q #H0 #T1 #H elim H -T1
 /5 width=1 by SN_intro/
 qed-.
@@ -40,15 +40,16 @@ qed-.
 (* Basic properties *********************************************************)
 
 (* Basic_1: was just: sn3_pr2_intro *)
-lemma csx_intro: ∀h,G,L,T1.
-                 (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫) →
-                 ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫.
+lemma csx_intro (h) (G) (L):
+      ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] T2) →
+      ❪G,L❫ ⊢ ⬈*𝐒[h] T1.
 /4 width=1 by SN_intro/ qed.
 
 (* Basic forward lemmas *****************************************************)
 
-fact csx_fwd_pair_sn_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
-                          ∀I,V,T. U = ②[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫.
+fact csx_fwd_pair_sn_aux (h) (G) (L):
+     ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U →
+     ∀I,V,T. U = ②[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] V.
 #h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
 @csx_intro #V2 #HLV2 #HV2
 @(IH (②[I]V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2
@@ -56,11 +57,13 @@ fact csx_fwd_pair_sn_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
 qed-.
 
 (* Basic_1: was just: sn3_gen_head *)
-lemma csx_fwd_pair_sn: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪②[I]V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫.
+lemma csx_fwd_pair_sn (h) (G) (L):
+      ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ②[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] V.
 /2 width=5 by csx_fwd_pair_sn_aux/ qed-.
 
-fact csx_fwd_bind_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
-                          ∀p,I,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫.
+fact csx_fwd_bind_dx_aux (h) (G) (L):
+     ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U →
+     ∀p,I,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T.
 #h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct
 @csx_intro #T2 #HLT2 #HT2
 @(IH (ⓑ[p, I]V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2
@@ -68,11 +71,13 @@ fact csx_fwd_bind_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
 qed-.
 
 (* Basic_1: was just: sn3_gen_bind *)
-lemma csx_fwd_bind_dx: ∀h,p,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_bind_dx (h) (G) (L):
+      ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T.
 /2 width=4 by csx_fwd_bind_dx_aux/ qed-.
 
-fact csx_fwd_flat_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
-                          ∀I,V,T. U = ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+fact csx_fwd_flat_dx_aux (h) (G) (L):
+     ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U →
+     ∀I,V,T. U = ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
 #h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
 @csx_intro #T2 #HLT2 #HT2
 @(IH (ⓕ[I]V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2
@@ -80,15 +85,18 @@ fact csx_fwd_flat_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
 qed-.
 
 (* Basic_1: was just: sn3_gen_flat *)
-lemma csx_fwd_flat_dx: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓕ[I]V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_flat_dx (h) (G) (L):
+      ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
 /2 width=5 by csx_fwd_flat_dx_aux/ qed-.
 
-lemma csx_fwd_bind: ∀h,p,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ →
-                    ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ ∧ ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_bind (h) (G) (L):
+      ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T →
+      ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] V & ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T.
 /3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-.
 
-lemma csx_fwd_flat: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓕ[I]V.T❫ →
-                    ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_flat (h) (G) (L):
+      ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓕ[I]V.T →
+      ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] V & ❪G,L❫ ⊢ ⬈*𝐒[h] T.
 /3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-.
 
 (* Basic_1: removed theorems 14: