notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index 36ef1b2a1e7273342644bec2450a9fcff4948156..2f316a737c2444ddd9f48f57d427e7d4172daf8a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -64,6 +64,17 @@ lemma cprs_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢
 #h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/
 qed.
 
+lemma cpxs_sort: ∀h,g,G,L,k,l1. deg h g k l1 →
+                 ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] ⋆((next h)^l2 k).
+#h #g #G #L #k #l1 #Hkl1 #l2 @(nat_ind_plus … l2) -l2 /2 width=1 by cpx_cpxs/
+#l2 #IHl2 #Hl21 >iter_SO
+@(cpxs_strap1 … (⋆(iter l2 ℕ (next h) k)))
+[ /3 width=3 by lt_to_le/
+| @(cpx_st … (l1-l2-1)) <plus_minus_m_m
+  /2 width=1 by deg_iter, monotonic_le_minus_r/
+]
+qed.
+
 lemma cpxs_bind_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
                     ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
                     ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
@@ -91,22 +102,22 @@ lemma cpxs_pair_sn: ∀h,g,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
 /3 width=3 by cpxs_strap1, cpx_pair_sn/
 qed.
 
-lemma cpxs_zeta: â\88\80h,g,G,L,V,T1,T,T2. â\87§[0, 1] T2 ≡ T →
+lemma cpxs_zeta: â\88\80h,g,G,L,V,T1,T,T2. â¬\86[0, 1] T2 ≡ T →
                  ⦃G, L.ⓓV⦄ ⊢ T1 ➡*[h, g] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡*[h, g] T2.
 #h #g #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1
 /3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
 qed.
 
-lemma cpxs_tau: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_eps: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
                 ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2.
 #h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_tau/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/
 qed.
 
-lemma cpxs_ti: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+lemma cpxs_ct: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
                ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2.
 #h #g #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ti/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/
 qed.
 
 lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
@@ -117,7 +128,7 @@ lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
 qed.
 
 lemma cpxs_theta_dx: ∀h,g,a,G,L,V1,V,V2,W1,W2,T1,T2.
-                     â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, g] V â\86\92 â\87§[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 →
+                     â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, g] V â\86\92 â¬\86[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[h, g] T2 →
                      ⦃G, L⦄ ⊢ W1 ➡[h, g] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[h, g] ⓓ{a}W2.ⓐV2.T2.
 #h #g #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 
 /4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/