From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 2 Jun 2019 13:52:42 +0000 (+0200)
Subject: milestone in basic_2
X-Git-Tag: make_still_working~246
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87f57ddc367303c33e19c83cd8989cd561f3185b;p=helm.git

milestone in basic_2

+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions
---

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
index 704301fe0..2b3dfcd4c 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
@@ -20,10 +20,10 @@ include "basic_2/dynamic/cnv.ma".
 (* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************)
 
 (* Note: extended validity of a closure, height of cnv_appl > 1 *)
-lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![Ⓕ,h].
+lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h].
 #h #p #G #L #s
 @(cnv_appl … 2 p … (⋆s) … (⋆s))
-[ #H destruct
+[ //
 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
 | /4 width=1 by cnv_bind, cnv_zero/
 | /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
@@ -32,15 +32,15 @@ lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0
 qed.
 
 (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
-lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![Ⓣ,h].
+lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h].
 #h #p #G #L #s
 @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
-[ /2 width=1 by/
+[ /2 width=1 by ylt_inj/
 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
 | @cnv_zero
   @cnv_bind //
   @(cnv_appl … 1 p … (⋆s) … (⋆s))
-  [ /2 width=1 by/
+  [ /2 width=1 by ylt_inj/
   | /2 width=1 by cnv_sort, cnv_zero/
   | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
   | /2 width=3 by cpms_ell, lifts_sort/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index 4db46f940..fe0b19cf3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/ynat/ynat_lt.ma".
 include "basic_2/notation/relations/exclaim_5.ma".
 include "basic_2/notation/relations/exclaim_4.ma".
 include "basic_2/notation/relations/exclaimstar_4.ma".
@@ -21,12 +22,12 @@ include "basic_2/rt_computation/cpms.ma".
 
 (* activate genv *)
 (* Basic_2A1: uses: snv *)
-inductive cnv (a) (h): relation3 genv lenv term ≝
+inductive cnv (a:ynat) (h): relation3 genv lenv term ≝
 | cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
 | cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
 | cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
 | cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n ≤ 1) → cnv a h G L V → cnv a h G L T →
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T →
             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T)
 | cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
             ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → cnv a h G L (ⓝU.T)
@@ -36,10 +37,10 @@ interpretation "context-sensitive native validity (term)"
    'Exclaim a h G L T = (cnv a h G L T).
 
 interpretation "context-sensitive restricted native validity (term)"
-   'Exclaim h G L T = (cnv true h G L T).
+   'Exclaim h G L T = (cnv (yinj (S (S O))) h G L T).
 
 interpretation "context-sensitive extended native validity (term)"
-   'ExclaimStar h G L T = (cnv false h G L T).
+   'ExclaimStar h G L T = (cnv Y h G L T).
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -111,7 +112,7 @@ lemma cnv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] 
 /2 width=4 by cnv_inv_bind_aux/ qed-.
 
 fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T →
-                               ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                               ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 #a #h #G #L #X * -L -X
 [ #G #L #s #X1 #X2 #H destruct
@@ -125,7 +126,7 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_appl *)
 lemma cnv_inv_appl (a) (h): ∀G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-                            ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                            ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                          ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
index cb2f97f55..c63a1aa12 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
@@ -12,7 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lib/arith_2b.ma".
 include "basic_2/rt_computation/cpms_aaa.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
 include "basic_2/dynamic/cnv.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
@@ -61,32 +63,19 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma cnv_inv_appl_SO (a) (h) (G) (L):
-      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                   ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
-* #h #G #L #V #T #H
-elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU
-[ elim (cnv_fwd_aaa … HT) #A #HA
-  elim (aaa_cpm_SO h … (ⓛ{p}W.U))
-  [|*: /2 width=8 by cpms_aaa_conf/ ] #X #HU0
-  elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct
-  lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0
-  lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0
-  /2 width=7 by ex5_4_intro/
-| lapply (Ha ?) -Ha [ // ] #Ha
-  lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct
-  /2 width=7 by ex5_4_intro/
-| @(ex5_4_intro … HV HT HVW HTU) #H destruct
-]
-qed-.
-
-lemma cnv_inv_appl_true (h) (G) (L):
-      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
-      ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
-                   ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W0.U0.
-#h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn
->Hn -n [| // ] #HV #HT #HVW #HTU
+lemma cnv_inv_appl_pred (a) (h) (G) (L):
+      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![yinj a, h] →
+      ∃∃p,W0,U0. ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                   ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W0.U0.
+#a #h #G #L #V #T #H
+elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU
+lapply (ylt_inv_inj … Ha) -Ha #Ha
+elim (cnv_fwd_aaa … HT) #A #HA
+elim (cpms_total_aaa h … (a-↑n) … (ⓛ{p}W.U))
+[|*: /2 width=8 by cpms_aaa_conf/ ] -HA #X #HU0
+elim (cpms_inv_abst_sn … HU0) #W0 #U0 #HW0 #_ #H destruct
+lapply (cpms_trans … HVW … HW0) -HVW -HW0 #HVW0
+lapply (cpms_trans … HTU … HU0) -HTU -HU0
+>(arith_m2 … Ha) -Ha #HTU0
 /2 width=5 by ex4_3_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
index 3437d2629..e2eca5cdf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/cpms_cpms.ma".
 include "basic_2/rt_equivalence/cpes.ma".
 include "basic_2/dynamic/cnv_aaa.ma".
 
@@ -21,7 +20,7 @@ include "basic_2/dynamic/cnv_aaa.ma".
 (* Properties with t-bound rt-equivalence for terms *************************)
 
 lemma cnv_appl_cpes (a) (h) (G) (L):
-      ∀n. (a = Ⓣ → n ≤ 1) →
+      ∀n. yinj n < a →
       ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] →
       ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W →
       ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h].
@@ -39,30 +38,20 @@ qed.
 
 lemma cnv_inv_appl_cpes (a) (h) (G) (L):
       ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+      ∃∃n,p,W,U. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                  ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
 #a #h #G #L #V #T #H
 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
 /3 width=7 by cpms_div, ex5_4_intro/
 qed-.
 
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
-      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
+lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
+      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![yinj a, h] →
+      ∃∃p,W,U. ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W.U.
 #a #h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.
-
-lemma cnv_inv_appl_true_cpes (h) (G) (L):
-      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
-      ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
-                 ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
-#h #G #L #V #T #H
-elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
->Hn -n [| // ] #HV #HT #HVW #HTU
-/2 width=5 by ex4_3_intro/
+elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
+/3 width=7 by cpms_div, ex4_3_intro/
 qed-.
 
 lemma cnv_inv_cast_cpes (a) (h) (G) (L):
@@ -82,7 +71,7 @@ lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term):
       (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
                      Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
       ) →
-      (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
+      (∀n,p,G,L,V,W,T,U. yinj n < a → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
                          ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U →
                          Q G L V → Q G L T → Q G L (ⓐV.T)
       ) →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
index c02e30077..d1f41252b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
@@ -15,7 +15,6 @@
 include "ground_2/xoa/ex_5_1.ma".
 include "ground_2/xoa/ex_9_3.ma".
 include "basic_2/rt_transition/cpm_tdeq.ma".
-include "basic_2/rt_transition/cpr.ma".
 include "basic_2/rt_computation/fpbg_fqup.ma".
 include "basic_2/dynamic/cnv_fsb.ma".
 
@@ -76,7 +75,7 @@ qed-.
 lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L):
                            ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] →
                            ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X →
-                           ∃∃m,q,W,U1,T2. a = Ⓣ → m ≤ 1 & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
+                           ∃∃m,q,W,U1,T2. yinj m < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
                                         & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2.
 #a #h #n #G #L #V #T1 #H0 #X #H1 #H2
 elim (cpm_inv_appl1 … H1) -H1 *
@@ -134,7 +133,7 @@ lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …):
                     ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
                     Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
                    ) →
-                   (∀m. (a = Ⓣ → m ≤ 1) →
+                   (∀m. yinj m < a →
                     ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G, L⦄ ⊢ V ➡*[1,h] W →
                     ∀p,T1,U1. ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] →
                     ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
index 8e2781a6b..8c720f4ca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
@@ -69,7 +69,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h):
     lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
     lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
     [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
-    /4 width=7 by cnv_appl, minus_le_trans_sn/
+    /3 width=7 by cnv_appl, le_ylt_trans/
   | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
     elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
     elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
@@ -102,7 +102,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h):
     elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
     lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
     lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
-    /5 width=7 by cnv_appl, cnv_bind, minus_le_trans_sn/
+    /4 width=7 by cnv_appl, cnv_bind, le_ylt_trans/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
   elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
index 2574f3703..7dc23b79a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
@@ -50,16 +50,19 @@ theorem cnv_dec (a) (h) (G) (L) (T):
 | #V #T #HG #HL #HT destruct
   elim (IH G L V) [| -IH #HV | // ]
   [ elim (IH G L T) -IH [| #HT #HV | // ]
-    [ cases a #HT #HV
-      [ elim (cnv_fwd_aaa … HT) #A #HA
-        elim (cpme_total_aaa h 1 … HA) #X
+    [ cases a -a [ * [| #a ]] #HT #HV
+      [ @or_intror #H
+        elim (cnv_inv_appl … H) -H #n #p #W #U #H #_ #_ #_ #_
+        /3 width=2 by lt_zero_false, ylt_inv_inj/
+      | elim (cnv_fwd_aaa … HT) #A #HA
+        elim (cpme_total_aaa h a … HA) #X
         elim (abst_dec X) [ * ]
         [ #p #W #U #H #HTU destruct
           elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
           [ elim HTU -HTU #HTU #_
-            /3 width=7 by cnv_appl_cpes, or_introl/
+            /4 width=7 by ylt_inj, cnv_appl_cpes, or_introl/
           | @or_intror #H
-            elim (cnv_inv_appl_true_cpes … H) -H #q #W0 #U0 #_ #_ #HVW0 #HTU0
+            elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #HVW0 #HTU0
             elim (cnv_cpme_cpms_conf … HT … HTU0 … HTU) -T #HU0 #_
             elim (cpms_inv_abst_bi … HU0) -HU0 #_ #HW0 #_ -p -q -U0
             /3 width=3 by cpes_cprs_trans/
@@ -68,7 +71,7 @@ theorem cnv_dec (a) (h) (G) (L) (T):
           ]
         | #HnTU #HTX
           @or_intror #H
-          elim (cnv_inv_appl_true_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0
+          elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0
           elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_
           elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0
           /2 width=4 by/
@@ -79,7 +82,7 @@ theorem cnv_dec (a) (h) (G) (L) (T):
         [ #p #W #U #H #HTU destruct
           elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
           [ elim HTU -HTU #n #HTU #_
-            @or_introl @(cnv_appl_cpes … HV … HT … HVW … HTU) #H destruct
+            /3 width=7 by cnv_appl_cpes, or_introl/ 
           | @or_intror #H
             elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0
             elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 5b83675b3..66ddc0d99 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -26,10 +26,10 @@ interpretation "native type assignment (term)"
    'Colon a h G L T U = (nta a h G L T U).
 
 interpretation "restricted native type assignment (term)"
-   'Colon h G L T U = (nta true h G L T U).
+   'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
 
 interpretation "extended native type assignment (term)"
-   'ColonStar h G L T U = (nta false h G L T U).
+   'ColonStar h G L T U = (nta Y h G L T U).
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
index b0530a3bb..2fbdaa07e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
@@ -21,10 +21,10 @@ include "basic_2/dynamic/nta.ma".
 (* Properties with advanced rt_computation for terms ************************)
 
 (* Basic_2A1: was by definition nta_appl ntaa_appl *)
-lemma nta_appl_abst (a) (h) (p) (G) (K):
+lemma nta_appl_abst (a) (h) (p) (G) (K): yinj 0 < a →
       ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
       ∀T,U. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,K⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #K #V #W #H1 #T #U #H2
+#a #h #p #G #K #Ha #V #W #H1 #T #U #H2
 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
 /4 width=7 by cnv_bind, cnv_appl, cnv_cast, cpms_appl_dx, cpms_bind_dx/
@@ -32,16 +32,16 @@ qed.
 
 (* Basic_1: was by definition: ty3_appl *)
 (* Basic_2A1: was nta_appl_old *)
-lemma nta_appl (a) (h) (p) (G) (L):
+lemma nta_appl (a) (h) (p) (G) (L): yinj 1 < a →
       ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
       ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #L #V #W #H1 #T #U #H2
+#a #h #p #G #L #Ha #V #W #H1 #T #U #H2
 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
 elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct
 elim (cprs_conf … HWX1 … HW0) -HW0 #X0 #HX10 #HWX0
 @(cnv_cast … (ⓐV.ⓛ{p}W0.U0)) (**) (* full auto too slow *)
-[ /3 width=7 by cnv_appl, cpms_bind/
+[ /3 width=7 by cnv_appl, cpms_bind, lt_ylt_trans/
 | /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
 | /2 width=1 by cpms_appl_dx/
 | /2 width=1 by cpms_appl_dx/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 4f9b52385..d459d184a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -71,7 +71,7 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
   /4 width=5 by nta_bind_cnv/
 | #V #T #HG #HL #HT #X #H destruct
   elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
-  /4 width=9 by nta_appl/
+  /4 width=9 by nta_appl, ylt_inj/
 | #U #T #HG #HL #HT #X #H destruct
   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
   /4 width=4 by nta_cast/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
index daf753fb3..0d058a673 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -51,9 +51,8 @@ elim (cnv_inv_appl … H2) #n #p #X1 #X2 #_ #HV #_ #HVX1 #HUX2
 elim (cnv_cpms_conf … HU … HUX0 … HUX2) -HU -HUX2
 <minus_O_n <minus_n_O #X #HX0 #H
 elim (cpms_inv_abst_sn … H) -H #X3 #X4 #HX13 #HX24 #H destruct
-@(cnv_cast … (ⓐV.X0)) [2:|*: /2 width=1 by cpms_appl_dx/ ]
-@(cnv_appl … X3) [4: |*: /2 width=7 by cpms_trans, cpms_cprs_trans/ ]
-#H destruct
+@(cnv_cast … (ⓐV.X0)) [2:|*: /2 width=1 by cpms_appl_dx/ ] (**) (* full auto a bit slow *)
+/3 width=10 by cnv_appl, cpms_trans, cpms_cprs_trans/
 qed.
 
 (* Basic_1: uses: ty3_sred_wcpr0_pr0 *)
@@ -169,7 +168,7 @@ lemma nta_inv_appl_sn (h) (G) (L) (X2):
       ∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h].
 #h #G #L #X2 #V #T #H
 elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2
-elim (cnv_inv_appl_true … H1) #p #W #U #HV #HT #HVW #HTU
+elim (cnv_inv_appl_pred … H1) #p #W #U #HV #HT #HVW #HTU
 /5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index a5c53bf3e..bf8f10608 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -27,8 +27,12 @@
    <table name="basic_2_sum"/>
 
    <subsection name="B">Stage "B"</subsection>
+   <news class="beta" date="2019 June 2.">
+         Parametrized applicability condition
+         allows λδ-2B to generalize both λδ-1A and λδ-1B.
+   </news>
    <news class="beta" date="2019 April 16.">
-         Extended (λδ-2) and restricted (λδ-1) validity is decidable 
+         Extended (λδ-2A) and restricted (λδ-1A) validity is decidable 
          (anniversary milestone).
    </news>
    <news class="beta" date="2019 March 25.">
@@ -37,7 +41,7 @@
          (i.e. no induction on the degree).
    </news>
    <news class="beta" date="2018 November 1.">
-         Extended (λδ-2) and restricted (λδ-1) type rules justified.
+         Extended (λδ-2A) and restricted (λδ-1A) type rules justified.
    </news>
    <news class="alpha" date="2018 September 21.">
          λδ-2A completed with
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
index c6203acd4..5729f64cf 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
@@ -42,3 +42,7 @@ qed.
 lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
 #x <arith_l2 //
 qed.
+
+lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
+#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
index ab87ca278..ab9cf4565 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
@@ -199,6 +199,10 @@ lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x <
 ]
 qed-.
 
+lemma le_ylt_trans (x) (y) (z): x ≤ y → yinj y < z → yinj x < z.  
+/3 width=3 by yle_ylt_trans, yle_inj/
+qed-.
+
 lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y.
 #x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
 qed-.
@@ -219,6 +223,10 @@ theorem ylt_trans: Transitive … ylt.
 ]
 qed-.
 
+lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z.  
+/3 width=3 by ylt_trans, ylt_inj/
+qed-.
+
 (* Elimination principles ***************************************************)
 
 fact ynat_ind_lt_le_aux: ∀R:predicate ynat.