+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions
(* 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/
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/
(* *)
(**************************************************************************)
+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".
(* 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)
'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 ***************************************************)
/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
(* 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-.
(* *)
(**************************************************************************)
+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 ******************************)
(* 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-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cpms_cpms.ma".
include "basic_2/rt_equivalence/cpes.ma".
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].
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):
(∀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)
) →
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".
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 *
∀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 →
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
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
| #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/
]
| #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/
[ #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
'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 *********************************************************)
(* 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/
(* 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/
/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/
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 *)
∃∃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-.
<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.">
(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
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-.
]
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-.
]
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.
projects / helm.git / commitdiff