We parametrize applicability condition with a generic subset of numbers.
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Properties with evaluation for t-bound rt-transition on terms ************)
+(* Properties with t-bound evaluation on terms ******************************)
lemma cnv_cpme_trans (a) (h) (n) (G) (L):
∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
#a #h #n #G #L #T0 #HT0 #T1 #HT01 #T2 * #HT02 #HT2
elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 <minus_n_n #T0 #HT10 #HT20
lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
-/2 width=1 by conj/
+/2 width=1 by cpme_intro/
qed-.
(* Main properties with evaluation for t-bound rt-transition on terms *****)
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Properties with head evaluation for t-bound rt-transition on terms *******)
+(* Properties with t-unbound whd evaluation on terms ************************)
lemma cnv_cpmuwe_trans (a) (h) (G) (L):
∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n.
/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
-axiom cnv_R_cpmuwe_dec (a) (h) (G) (L):
- ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
-
(* Main inversions with head evaluation for t-bound rt-transition on terms **)
theorem cnv_cpmuwe_mono (a) (h) (G) (L):
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpme_aaa.ma".
+include "basic_2/rt_computation/cnuw_cnuw.ma".
+include "basic_2/rt_computation/cpmuwe.ma".
+include "basic_2/dynamic/cnv_cpme.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Advanced Properties with t-unbound whd evaluation on terms ***************)
+
+lemma cnv_R_cpmuwe_dec (a) (h) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
+#a #h #G #L #T1 #HT1 #n
+elim (cnv_fwd_aaa … HT1) #A #HA
+elim (cpme_total_aaa h n … HA) -HA #T2 #HT12
+elim (cnuw_dec h G L T2) #HnT1
+[ /5 width=3 by cpme_fwd_cpms, cpmuwe_intro, ex_intro, or_introl/
+| @or_intror * #T3 * #HT13 #HT3
+ lapply (cnv_cpme_cpms_conf … HT1 … HT13 … HT12) -a -T1 #HT32
+ /4 width=9 by cpme_fwd_cpms, cnuw_cpms_trans/
+]
+qed-.
include "basic_2/rt_computation/cpmuwe_cpmuwe.ma".
include "basic_2/rt_equivalence/cpes_cpes.ma".
-include "basic_2/dynamic/cnv_cpmuwe.ma".
+include "basic_2/dynamic/cnv_cpmuwe.ma". (**) (* should be included by the next *)
+include "basic_2/dynamic/cnv_cpmuwe_cpme.ma".
include "basic_2/dynamic/cnv_cpes.ma".
include "basic_2/dynamic/cnv_preserve_cpes.ma".
"normality for t-unbound weak head context-sensitive parallel rt-transition (term)"
'PRedITNormal h G L T = (cnuw h G L T).
-lemma cpm_inv_lref1_ctop (n) (h) (G):
- ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
-#n #h #G #X2 * [| #i ] #H
-[ elim (cpm_inv_zero1 … H) -H *
- [ #H1 #H2 destruct /2 width=1 by conj/
- | #Y #X1 #X2 #_ #_ #H destruct
- | #m #Y #X1 #X2 #_ #_ #H destruct
- ]
-| elim (cpm_inv_lref1 … H) -H *
- [ #H1 #H2 destruct /2 width=1 by conj/
- | #Z #Y #X0 #_ #_ #H destruct
- ]
-]
-qed.
-
-lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
- ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
-#n #h #I #G #K #X2 #H
-elim (cpm_inv_zero1 … H) -H *
-[ #H1 #H2 destruct /2 width=1 by conj/
-| #Y #X1 #X2 #_ #_ #H destruct
-| #m #Y #X1 #X2 #_ #_ #H destruct
-]
-qed.
-
-lemma cpms_inv_lref1_ctop (n) (h) (G):
- ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0.
-#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
- elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct
- /2 width=1 by conj/
-]
-qed-.
-
-lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G):
- ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0.
-#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
- elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct
- /2 width=1 by conj/
-]
-qed-.
-
-lemma cpms_inv_gref1 (n) (h) (G) (L):
- ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0.
-#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
- elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct
- /2 width=1 by conj/
-]
-qed-.
-
(* Basic properties *********************************************************)
lemma cnuw_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⋆s.
∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓝV.T → ⊥.
#h #G #L #V #T #H
lapply (H 0 T ?) [ /3 width=1 by cpm_cpms, cpm_eps/ ] -H #H
-/2 width=3 by tweq_inv_cast_sn_XY_Y/
+/2 width=3 by tweq_inv_cast_xy_y/
qed-.
(* Basic forward lemmas *****************************************************)
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cnuw.ma".
+include "basic_2/rt_computation/cnuw_simple.ma".
+include "basic_2/rt_computation/cnuw_drops.ma".
include "basic_2/rt_computation/cprs_tweq.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
#h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23
/4 width=5 by cpms_trans, tweq_canc_sn/
qed-.
+
+lemma cnuw_dec_ex (h) (G) (L):
+ ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1
+ | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & (T1 ≅ T2 → ⊥).
+#h #G #L #T1 elim T1 -T1 *
+[ #s /3 width=5 by cnuw_sort, or_introl/
+| #i elim (drops_F_uni L i)
+ [ /3 width=7 by cnuw_atom_drops, or_introl/
+ | * * [ #I | * #V ] #K #HLK
+ [ /3 width=8 by cnuw_unit_drops, or_introl/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpms_delta_drops/ ] #H
+ lapply (tweq_inv_lref_sn … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpms_ell_drops/ ] #H
+ lapply (tweq_inv_lref_sn … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ ]
+ ]
+| #l /3 width=5 by cnuw_gref, or_introl/
+| #p * [ cases p ] #V1 #T1 #_ #_
+ [ elim (cprs_abbr_pos_twneq h G L V1 T1) #T2 #HT12 #HnT12
+ /4 width=4 by ex2_2_intro, or_intror/
+ | /3 width=5 by cnuw_abbr_neg, or_introl/
+ | /3 width=5 by cnuw_abst, or_introl/
+ ]
+| * #V1 #T1 #_ #IH
+ [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
+ [ elim IH -IH
+ [ /3 width=6 by cnuw_appl_simple, or_introl/
+ | * #n #T2 #HT12 #HnT12 -HT1
+ @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpms_appl_dx/ ] #H
+ lapply (tweq_inv_appl_bi … H) -H /2 width=1 by/
+ ]
+ | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+ @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpms_theta/ ] #H
+ elim (tweq_inv_appl_sn … H) -H #X1 #X2 #_ #H destruct
+ | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpms_beta/ ] #H
+ elim (tweq_inv_appl_sn … H) -H #X1 #X2 #_ #H destruct
+ ]
+ | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpms_eps/ ] #H
+ /2 width=4 by tweq_inv_cast_xy_y/
+ ]
+]
+qed-.
+
+lemma cnuw_dec (h) (G) (L): ∀T. Decidable (⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T).
+#h #G #L #T1
+elim (cnuw_dec_ex h G L T1)
+[ /2 width=1 by or_introl/
+| * #n #T2 #HT12 #nT12 /4 width=2 by or_intror/
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/cpr_tdeq.ma".
-include "basic_2/rt_computation/cnuw_simple.ma".
-include "basic_2/rt_computation/cnuw_drops.ma".
-include "basic_2/rt_computation/cnuw_cnuw.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
-
-(* Properties with context-free sort-irrelevant equivalence for terms *******)
-
-lemma cnuw_dec_tdeq (h) (G) (L):
- ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1
- | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
-#h #G #L #T1 elim T1 -T1 *
-[ #s /3 width=5 by cnuw_sort, or_introl/
-| #i elim (drops_F_uni L i)
- [ /3 width=7 by cnuw_atom_drops, or_introl/
- | * * [ #I | * #V ] #K #HLK
- [ /3 width=8 by cnuw_unit_drops, or_introl/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- ]
- ]
-| #l /3 width=5 by cnuw_gref, or_introl/
-| #p * [ cases p ] #V1 #T1 #_ #_
- [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2
- elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
- [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
- @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
- /2 width=7 by tdeq_lifts_inv_pair_sn/
- | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- | /3 width=5 by cnuw_abbr_neg, or_introl/
- | /3 width=5 by cnuw_abst, or_introl/
- ]
-| * #V1 #T1 #_ #IH
- [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
- [ elim IH -IH
- [ /3 width=6 by cnuw_appl_simple, or_introl/
- | * #n #T2 #HT12 #HnT12
- @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
- elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
- ]
- | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
- @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- ]
- | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
- /2 width=4 by tdeq_inv_pair_xy_y/
- ]
-]
-qed-.
interpretation "evaluation for t-bound context-sensitive parallel rt-transition (term)"
'PRedEval h n G L T1 T2 = (cpme h n G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpme_intro (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃T2⦄ → ⦃G,L⦄⊢T1➡*[h,n]𝐍⦃T2⦄.
+/2 width=1 by conj/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpme_fwd_cpms (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄⊢T1➡*[h,n]𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 * //
+qed-.
elim (cpm_inv_sort1 … HX2) -HX2 #H #_ destruct //
qed-.
+lemma cpms_inv_lref1_ctop (n) (h) (G):
+ ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_gref1 (n) (h) (G) (L):
+ ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0.
+#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+ elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
lemma cpms_inv_cast1 (h) (n) (G) (L):
∀W1,T1,X2. ⦃G,L⦄ ⊢ ⓝW1.T1 ➡*[n,h] X2 →
∨∨ ∃∃W2,T2. ⦃G,L⦄ ⊢ W1 ➡*[n,h] W2 & ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓝW2.T2
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/cpm_cpx.ma".
-include "basic_2/rt_computation/csx.ma".
-include "basic_2/rt_computation/cnuw_tdeq.ma".
+include "static_2/syntax/tweq_tdeq.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+include "basic_2/rt_computation/cpms_cpxs.ma".
+include "basic_2/rt_computation/cnuw_cnuw.ma".
include "basic_2/rt_computation/cpmuwe.ma".
(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************)
lemma cpmuwe_total_csx (h) (G) (L):
∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
#h #G #L #T1 #H
-@(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnuw_dec_tdeq h G L T1)
+@(csx_ind_cpxs … H) -T1 #T1 #_ #IHT1
+elim (cnuw_dec_ex h G L T1)
[ -IHT1 #HT1 /3 width=4 by cpmuwe_intro, ex1_2_intro/
| * #n1 #T0 #HT10 #HnT10
- elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
- #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmuwe_intro, ex1_2_intro/
+ elim (IHT1 … T0) -IHT1
+ [ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_trans, cpmuwe_intro, ex1_2_intro/
+ | /3 width=1 by tdeq_tweq/
+ | /2 width=2 by cpms_fwd_cpxs/
+ ]
]
qed-.
∀T1,T0. ⦃G,L⦄ ⊢T1 ➡*[n,h] T0 →
∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄.
#h #n #G #L #T1 #T0 #HT10 #T2 * #HT02 #HT2
-/3 width=3 by cpms_cprs_trans, conj/
+/3 width=3 by cpms_cprs_trans, cpme_intro/
qed-.
#h #G #L #T0 #T1 #HT01 #T2 * #HT02 #HT2
elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20
lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
-/2 width=1 by conj/
+/2 width=1 by cpme_intro/
qed-.
(* Main properties *********************************************************)
∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄.
#h #G #L #T1 #H
@(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, conj/ ] *
+elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, cpme_intro/ ] *
#T0 #HT10 #HnT10
elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
-#T2 * /4 width=3 by cprs_step_sn, ex_intro, conj/
+#T2 * /4 width=3 by cprs_step_sn, ex_intro, cpme_intro/
qed-.
elim (tweq_dec U1 U2) [ #HpU12 | -HTU2 #HnU12 ]
[ @(ex2_intro … T2) (**) (* full auto not tried *)
[ /3 width=6 by cpms_zeta, cpms_step_sn, cpm_bind/
- | /4 width=6 by tweq_inv_abbr_pos_sn_X_lifts_Y_Y, tweq_canc_sn, tweq_abbr_pos/
+ | /4 width=6 by tweq_inv_abbr_pos_x_lifts_y_y, tweq_canc_sn, tweq_abbr_pos/
]
| /4 width=3 by cpm_cpms, cpm_bind, tweq_inv_abbr_pos_bi, ex2_intro/
]
]
qed-.
+lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ➡[n,h] T2 →
∨∨ T2 = #(↑i) ∧ n = 0
| ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ➡[n,h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
]
qed-.
+lemma cpm_inv_lref1_ctop (n) (h) (G):
+ ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 * [| #i ] #H
+[ elim (cpm_inv_zero1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpm_inv_lref1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+
lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G,L⦄ ⊢ §l ➡[n,h] T2 → T2 = §l ∧ n = 0.
#n #h #G #L #T2 #l * #c #Hc #H elim (cpg_inv_gref1 … H) -H
#H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/
<table name="basic_2_sum"/>
<subsection name="B">Stage "B"</subsection>
+ <news class="beta" date="2019 September 3.">
+ Applicability condition is now parametrized
+ with a generic subset of numbers.
+ </news>
<news class="beta" date="2019 June 2.">
- Parametrized applicability condition
+ Applicability condition parametrized
+ with an initial interval of numbers
allows λδ-2B to generalize both λδ-2A and λδ-1B.
</news>
<news class="beta" date="2019 April 16.">
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
}
]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
[ [ "t-unbound whd evaluation for terms" ] "cpmuwe ( ⦃?,?⦄ ⊢ ? ⬌*𝐍𝐖*[?,?] ? )" "cpmuwe_csx" + "cpmuwe_cpmuwe" * ]
- [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_tdeq" + "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ]
-
- [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
+ [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ]
+ [ [ "t-bpund evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
[ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
}
]
]
qed-.
-lemma tweq_inv_abbr_pos_sn_X_lifts_Y_Y (T) (f:rtmap):
+lemma tweq_inv_abbr_pos_x_lifts_y_y (T) (f:rtmap):
∀V,U. +ⓓV.U ≅ T → ⬆*[f]T ≘ U → ⊥.
@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
#T elim T -T //
qed.
+lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
+#I #V #T /2 width=1 by le_S_S/
+qed.
+
(* Basic_1: removed theorems 11:
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
include "static_2/notation/relations/approxeq_2.ma".
include "static_2/syntax/term_weight.ma".
-lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
-#I #V #T /2 width=1 by le_S_S/
-qed.
-
(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
inductive tweq: relation term ≝
/2 width=1 by conj/
qed-.
-lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥.
+lemma tweq_inv_cast_xy_y: ∀T,V. ⓝV.T ≅ T → ⊥.
@(f_ind … tw) #n #IH #T #Hn #V #H destruct
elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
/2 width=4 by/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/syntax/tdeq.ma".
+include "static_2/syntax/tweq.ma".
+
+(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
+
+(* Properties with sort-irrelevant equivalence for terms ********************)
+
+lemma tdeq_tweq: ∀T1,T2. T1 ≛ T2 → T1 ≅ T2.
+#T1 #T2 #H elim H -T1 -T2 [||| * [ #p ] * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT ]
+[ /1 width=1 by tweq_sort/
+| /1 width=1 by tweq_lref/
+| /1 width=1 by tweq_gref/
+| cases p -p /2 width=1 by tweq_abbr_pos, tweq_abbr_neg/
+| /1 width=1 by tweq_abst/
+| /2 width=1 by tweq_appl/
+| /2 width=1 by tweq_cast/
+]
+qed.
}
]
[ { "sort-irrelevant whd equivalence" * } {
- [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tueq" * ]
+ [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tdeq" + "tweq_tueq" * ]
}
]
[ { "sort-irrelevant equivalence" * } {
projects / helm.git / commitdiff