(* Note: this is the "big tree" theorem *)
(* Basic_2A1: uses: snv_fwd_fsb *)
lemma cnv_fwd_fsb (h) (a):
- ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ≥[h] 𝐒❪G,L,T❫.
+ ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ≥𝐒[h] ❪G,L,T❫.
#h #a #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
qed-.
(* Forward lemmas with strongly rt-normalizing terms ************************)
lemma cnv_fwd_csx (h) (a):
- ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+ ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
#h #a #G #L #T #H
/3 width=2 by cnv_fwd_fsb, fsb_inv_csx/
qed-.
(* Basic_2A1: uses: nta_fwd_csn *)
theorem nta_fwd_fsb (h) (a) (G) (L):
∀T,U. ❪G,L❫ ⊢ T :[h,a] U →
- ∧∧ ≥[h] 𝐒❪G,L,T❫ & ≥[h] 𝐒❪G,L,U❫.
+ ∧∧ ≥𝐒[h] ❪G,L,T❫ & ≥𝐒[h] ❪G,L,U❫.
#h #a #G #L #T #U #H
elim (cnv_inv_cast … H) #X #HU #HT #_ #_ -X
/3 width=2 by cnv_fwd_fsb, conj/
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ≥[ term 46 h ] 𝐒❪ break term 46 G, break term 46 L, break term 46 T ❫ )"
+notation "hvbox( ≥𝐒[ term 46 h ] ❪ break term 46 G, break term 46 L, break term 46 T ❫ )"
non associative with precedence 45
for @{ 'PRedSubTyStrong $h $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈[ break term 46 h ] 𝐍❪ break term 46 T ❫ )"
+notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈𝐍[ break term 46 h ] break term 46 T )"
non associative with precedence 45
for @{ 'PRedTyNormal $h $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ⬈*[ break term 46 h, break term 46 T ] 𝐒❪ break term 46 L ❫ )"
+notation "hvbox( G ⊢ ⬈*𝐒[ break term 46 h, break term 46 T ] break term 46 L )"
non associative with precedence 45
for @{ 'PRedTySNStrong $h $T $G $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈*[ break term 46 h] 𝐒❪ break term 46 T ❫ )"
+notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈*𝐒[ break term 46 h ] break term 46 T )"
non associative with precedence 45
for @{ 'PRedTyStrong $h $G $L $T }.
(* Properties with strong normalization for unbound rt-transition for terms *)
lemma cpmuwe_total_csx (h) (G) (L):
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃∃T2,n. ❪G,L❫ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃∃T2,n. ❪G,L❫ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
#h #G #L #T1 #H
@(csx_ind_cpxs … H) -T1 #T1 #_ #IHT1
elim (cnuw_dec_ex h G L T1)
qed-.
lemma R_cpmuwe_total_csx (h) (G) (L):
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃n. R_cpmuwe h G L T1 n.
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃n. R_cpmuwe h G L T1 n.
#h #G #L #T1 #H
elim (cpmuwe_total_csx … H) -H #T2 #n #HT12
/3 width=3 by ex_intro (* 2x *)/
(* Basic_1: was just: nf2_sn3 *)
(* Basic_2A1: was: csx_cpre *)
lemma cprre_total_csx (h) (G) (L):
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃T2. ❪G,L❫ ⊢ T1 ➡*𝐍[h,0] T2.
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃T2. ❪G,L❫ ⊢ T1 ➡*𝐍[h,0] T2.
#h #G #L #T1 #H
@(csx_ind … H) -T1 #T1 #_ #IHT1
elim (cnr_dec_teqx h G L T1) [ /3 width=3 by ex_intro, cpmre_intro/ ] *
(* Properties with normal forms *********************************************)
lemma cpxs_cnx (h) (G) (L) (T1):
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫.
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ❪G,L❫ ⊢ ⬈𝐍[h] T1.
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (h) (G) (L):
- ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ → T1 ≛ T2.
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈𝐍[h] T1 → T1 ≛ T2.
#h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.
qed-.
lemma cpxs_fwd_cnx (h) (G) (L):
- ∀T1. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ →
+ ∀T1. ❪G,L❫ ⊢ ⬈𝐍[h] T1 →
∀X2. ❪G,L❫ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
/3 width=5 by cpxs_inv_cnx1, teqx_teqo/ qed-.
(* Basic_1: was just: nf2_iso_appls_lref *)
lemma cpxs_fwd_cnx_vector (h) (G) (L):
- ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ →
+ ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍[h] T →
∀Vs,X2. ❪G,L❫ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #X2 #H
(* 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-.
(* 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
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
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
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:
(* Main properties with atomic arity assignment *****************************)
-theorem aaa_csx: ∀h,G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+theorem aaa_csx (h) (G) (L):
+ ∀T,A. ❪G,L❫ ⊢ T ⁝ A → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
#h #G #L #T #A #H
@(gcr_aaa … (csx_gcp h) (csx_gcr h) … H)
qed.
(* Advanced eliminators *****************************************************)
-fact aaa_ind_csx_aux: ∀h,G,L,A. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ T ⁝ A → Q T.
+fact aaa_ind_csx_aux (h) (G) (L):
+ ∀A. ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ T ⁝ A → Q T.
#h #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
qed-.
-lemma aaa_ind_csx: ∀h,G,L,A. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T.
+lemma aaa_ind_csx (h) (G) (L):
+ ∀A. ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T.
/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
-fact aaa_ind_csx_cpxs_aux: ∀h,G,L,A. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ T ⁝ A → Q T.
+fact aaa_ind_csx_cpxs_aux (h) (G) (L):
+ ∀A. ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ T ⁝ A → Q T.
#h #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
qed-.
(* Basic_2A1: was: aaa_ind_csx_alt *)
-lemma aaa_ind_csx_cpxs: ∀h,G,L,A. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T.
+lemma aaa_ind_csx_cpxs (h) (G) (L):
+ ∀A. ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ T1 ⁝ A →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T.
/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.
(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csx: ∀h,G,L,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma cnx_csx (h) (G) (L):
+ ∀T. ❪G,L❫ ⊢ ⬈𝐍[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
/2 width=1 by NF_to_SN/ qed.
(* Advanced properties ******************************************************)
-lemma csx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪⋆s❫.
+lemma csx_sort (h) (G) (L):
+ ∀s. ❪G,L❫ ⊢ ⬈*𝐒[h] ⋆s.
/3 width=4 by cnx_csx, cnx_sort/ qed.
(* Basic_1: was just: sn3_appls_lref *)
lemma csx_applv_cnx (h) (G) (L):
- ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ →
- ∀Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫.
+ ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍[h] T →
+ ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T.
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
(* Note: strong normalization does not depend on this any more *)
lemma csx_applv_sort (h) (G) (L):
- ∀s,Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.⋆s❫.
+ ∀s,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.⋆s.
/3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.
(* Properties with unbound context-sensitive rt-computation for terms *******)
(* Basic_1: was just: sn3_intro *)
-lemma csx_intro_cpxs: ∀h,G,L,T1.
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫) →
- ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫.
+lemma csx_intro_cpxs (h) (G) (L):
+ ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] T2) →
+ ❪G,L❫ ⊢ ⬈*𝐒[h] T1.
/4 width=1 by cpx_cpxs, csx_intro/ qed-.
(* Basic_1: was just: sn3_pr3_trans *)
-lemma csx_cpxs_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma csx_cpxs_trans (h) (G) (L):
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2.
#h #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2
/2 width=3 by csx_cpx_trans/
qed-.
(* Eliminators with unbound context-sensitive rt-computation for terms ******)
-lemma csx_ind_cpxs_teqx: ∀h,G,L. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀T0. ❪G,L❫ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛ T2 → Q T2.
+lemma csx_ind_cpxs_teqx (h) (G) (L):
+ ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀T0. ❪G,L❫ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛ T2 → Q T2.
#h #G #L #Q #IH #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02
@IH -IH /3 width=3 by csx_cpxs_trans, csx_teqx_trans/ -HT1 #V2 #HTV2 #HnTV2
qed-.
(* Basic_2A1: was: csx_ind_alt *)
-lemma csx_ind_cpxs: ∀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_cpxs (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 #IH #T #HT
@(csx_ind_cpxs_teqx … IH … HT) -IH -HT // (**) (* full auto fails *)
qed-.
(* Advanced properties ******************************************************)
-lemma csx_teqx_trans (h) (G):
- ∀L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma csx_teqx_trans (h) (G) (L):
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
@csx_intro #T1 #HT21 #HnT21 elim (teqx_cpx_trans … HT2 … HT21) -HT21
/4 width=5 by teqx_repl/
qed-.
-lemma csx_cpx_trans (h) (G):
- ∀L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma csx_cpx_trans (h) (G) (L):
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
elim (teqx_dec T1 T2) /3 width=4 by csx_teqx_trans/
qed-.
(* Basic_1: was just: sn3_cast *)
-lemma csx_cast (h) (G):
- ∀L,W. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪W❫ →
- ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓝW.T❫.
+lemma csx_cast (h) (G) (L):
+ ∀W. ❪G,L❫ ⊢ ⬈*𝐒[h] W →
+ ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓝW.T.
#h #G #L #W #HW @(csx_ind … HW) -W
#W #HW #IHW #T #HT @(csx_ind … HT) -T
#T #HT #IHT @csx_intro
(* Basic_1: was just: sn3_abbr *)
(* Basic_2A1: was: csx_lref_bind *)
-lemma csx_lref_pair_drops (h) (G):
- ∀I,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
- ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫.
-#h #G #I #L #K #V #i #HLK #HV
+lemma csx_lref_pair_drops (h) (G) (L):
+ ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
+ ❪G,K❫ ⊢ ⬈*𝐒[h] V → ❪G,L❫ ⊢ ⬈*𝐒[h] #i.
+#h #G #L #I #K #V #i #HLK #HV
@csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H
[ #H destruct elim Hi //
| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
(* Basic_1: was: sn3_gen_def *)
(* Basic_2A1: was: csx_inv_lref_bind *)
-lemma csx_inv_lref_pair_drops (h) (G):
- ∀I,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
- ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
-#h #G #I #L #K #V #i #HLK #Hi
+lemma csx_inv_lref_pair_drops (h) (G) (L):
+ ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V →
+ ❪G,L❫ ⊢ ⬈*𝐒[h] #i → ❪G,K❫ ⊢ ⬈*𝐒[h] V.
+#h #G #L #I #K #V #i #HLK #Hi
elim (lifts_total V (𝐔❨↑i❩))
/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
qed-.
-lemma csx_inv_lref_drops (h) (G):
- ∀L,i. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫ →
+lemma csx_inv_lref_drops (h) (G) (L):
+ ∀i. ❪G,L❫ ⊢ ⬈*𝐒[h] #i →
∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆
| ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I]
- | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
+ | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒[h] V.
#h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
* * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
qed-.
(* Advanced properties ************************************* ****************)
(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_applv_beta (h) (G):
- ∀p,L,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓓ[p]ⓝW.V.T❫ →
- ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓐV.ⓛ[p]W.T❫.
-#h #G #p #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
+lemma csx_applv_beta (h) (G) (L):
+ ∀p,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓓ[p]ⓝW.V.T →
+ ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓐV.ⓛ[p]W.T.
+#h #G #L #p #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
#V0 #Vs #IHV #V #W #T #H1T
lapply (csx_fwd_pair_sn … H1T) #HV0
lapply (csx_fwd_flat_dx … H1T) #H2T
]
qed.
-lemma csx_applv_delta_drops (h) (G):
- ∀I,L,K,V1,i. ⇩[i] L ≘ K.ⓑ[I]V1 →
+lemma csx_applv_delta_drops (h) (G) (L):
+ ∀I,K,V1,i. ⇩[i] L ≘ K.ⓑ[I]V1 →
∀V2. ⇧[↑i] V1 ≘ V2 →
- ∀Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.V2❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.#i❫.
-#h #G #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+ ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.V2 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.#i.
+#h #G #L #I #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ /4 width=11 by csx_inv_lifts, csx_lref_pair_drops, drops_isuni_fwd_drop2/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
qed.
(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta (h) (G):
- ∀p,L,V1b,V2b. ⇧[1] V1b ≘ V2b →
- ∀V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.ⒶV2b.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶV1b.ⓓ[p]V.T❫.
-#h #G #p #L #V1b #V2b * -V1b -V2b /2 width=1 by/
+lemma csx_applv_theta (h) (G) (L):
+ ∀p,V1b,V2b. ⇧[1] V1b ≘ V2b →
+ ∀V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.ⒶV2b.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶV1b.ⓓ[p]V.T.
+#h #G #L #p #V1b #V2b * -V1b -V2b /2 width=1 by/
#V1b #V2b #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
elim H -V1b -V2b /2 width=3 by csx_appl_theta/
qed.
(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_applv_cast (h) (G):
- ∀L,Vs,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.U❫ →
- ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓝU.T❫.
+lemma csx_applv_cast (h) (G) (L):
+ ∀Vs,U. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.U →
+ ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓝU.T.
#h #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
#V #Vs #IHV #U #H1U #T #H1T
lapply (csx_fwd_pair_sn … H1U) #HV
(* Basic_1: was just: sn3_lift *)
(* Basic_2A1: was just: csx_lift *)
-lemma csx_lifts: ∀h,G. d_liftable1 … (csx h G).
+lemma csx_lifts (h) (G):
+ d_liftable1 … (csx h G).
#h #G #K #T #H @(csx_ind … H) -T
#T1 #_ #IH #b #f #L #HLK #U1 #HTU1
@csx_intro #U2 #HU12 #HnU12
(* Basic_1: was just: sn3_gen_lift *)
(* Basic_2A1: was just: csx_inv_lift *)
-lemma csx_inv_lifts: ∀h,G. d_deliftable1 … (csx h G).
+lemma csx_inv_lifts (h) (G):
+ d_deliftable1 … (csx h G).
#h #G #L #U #H @(csx_ind … H) -U
#U1 #_ #IH #b #f #K #HLK #T1 #HTU1
@csx_intro #T2 #HT12 #HnT12
(* Properties with sort-irrelevant equivalence for closures *****************)
-lemma csx_feqx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma csx_feqx_conf (h):
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
/3 width=3 by csx_reqx_conf, csx_teqx_trans/
qed-.
(* Properties with parallel rst-transition for closures *********************)
(* Basic_2A1: was: csx_fpb_conf *)
-lemma csx_fpbq_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≽[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma csx_fpbq_conf (h):
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≽[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
/2 width=6 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_feqx_conf/
qed-.
lemma csx_fqu_conf (h) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
- ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/
| /2 width=3 by csx_fwd_pair_sn/
lemma csx_fquq_conf (h) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
- ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
* #HG #HL #HT destruct //
qed-.
lemma csx_fqup_conf (h) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ →
- ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
/3 width=6 by csx_fqu_conf/
qed-.
lemma csx_fqus_conf (h) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ →
- ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
/3 width=6 by csx_fquq_conf/
qed-.
(* Main properties with generic computation properties **********************)
-theorem csx_gcp: ∀h. gcp (cpx h) teqx (csx h).
+theorem csx_gcp (h):
+ gcp (cpx h) teqx (csx h).
#h @mk_gcp
[ normalize /3 width=13 by cnx_lifts/
| /2 width=4 by cnx_sort/
(* Main properties with generic candidates of reducibility ******************)
-theorem csx_gcr (h): gcr (cpx h) teqx (csx h) (csx h).
+theorem csx_gcr (h):
+ gcr (cpx h) teqx (csx h) (csx h).
#h @mk_gcr
[ //
| #G #L #Vs #Hvs #T #HT #H
(* Properties with unbound parallel rt-transition on all entries ************)
-lemma csx_lpx_conf (h) (G):
- ∀L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ →
- ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_lpx_conf (h) (G) (L1):
+ ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T →
+ ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
#h #G #L1 #T #H @(csx_ind_cpxs … H) -T
/4 width=3 by csx_intro, lpx_cpx_trans/
qed-.
(* Advanced properties ******************************************************)
-lemma csx_abst (h) (G):
- ∀p,L,W. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪W❫ →
- ∀T. ❪G,L.ⓛW❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓛ[p]W.T❫.
-#h #G #p #L #W #HW
+lemma csx_abst (h) (G) (L):
+ ∀p,W. ❪G,L❫ ⊢ ⬈*𝐒[h] W →
+ ∀T. ❪G,L.ⓛW❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓛ[p]W.T.
+#h #G #L #p #W #HW
@(csx_ind … HW) -W #W #_ #IHW #T #HT
@(csx_ind … HT) -T #T #HT #IHT
@csx_intro #X #H1 #H2
]
qed.
-lemma csx_abbr (h) (G):
- ∀p,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ →
- ∀T. ❪G,L.ⓓV❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.T❫.
-#h #G #p #L #V #HV
+lemma csx_abbr (h) (G) (L):
+ ∀p,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V →
+ ∀T. ❪G,L.ⓓV❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.T.
+#h #G #L #p #V #HV
@(csx_ind … HV) -V #V #_ #IHV #T #HT
@(csx_ind_cpxs … HT) -T #T #HT #IHT
@csx_intro #X #H1 #H2
]
qed.
-lemma csx_bind (h) (G):
- ∀p,I,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ →
- ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫.
-#h #G #p * #L #V #HV #T #HT
+lemma csx_bind (h) (G) (L):
+ ∀p,I,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V →
+ ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T.
+#h #G #L #p * #V #HV #T #HT
/2 width=1 by csx_abbr, csx_abst/
qed.
-fact csx_appl_theta_aux (h) (G):
- ∀p,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → ∀V1,V2. ⇧[1] V1 ≘ V2 →
- ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV1.ⓓ[p]V.T❫.
-#h #G #p #L #X #H
+fact csx_appl_theta_aux (h) (G) (L):
+ ∀p,U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → ∀V1,V2. ⇧[1] V1 ≘ V2 →
+ ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T.
+#h #G #L #p #X #H
@(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lapply (csx_fwd_pair_sn … HVT) #HV
lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
]
qed-.
-lemma csx_appl_theta (h) (G):
- ∀p,L,V,V2,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.ⓐV2.T❫ →
- ∀V1. ⇧[1] V1 ≘ V2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV1.ⓓ[p]V.T❫.
+lemma csx_appl_theta (h) (G) (L):
+ ∀p,V,V2,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.ⓐV2.T →
+ ∀V1. ⇧[1] V1 ≘ V2 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T.
/2 width=5 by csx_appl_theta_aux/ qed.
(* Properties with unbound parallel rt-computation on all entries ***********)
-lemma csx_lpxs_conf: ∀h,G,L1,L2,T. ❪G,L1❫ ⊢ ⬈*[h] L2 →
- ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_lpxs_conf (h) (G) (L1):
+ ∀L2,T. ❪G,L1❫ ⊢ ⬈*[h] L2 → ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
#h #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
/3 by lpxs_step_dx, csx_lpx_conf/
qed-.
(* Advanced properties ******************************************************)
-fact csx_appl_beta_aux (h) (G):
- ∀p,L,U1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U1❫ →
- ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.ⓛ[p]W.T1❫.
-#h #G #p #L #X #H @(csx_ind … H) -X
+fact csx_appl_beta_aux (h) (G) (L):
+ ∀p,U1. ❪G,L❫ ⊢ ⬈*𝐒[h] U1 →
+ ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.ⓛ[p]W.T1.
+#h #G #L #p #X #H @(csx_ind … H) -X
#X #HT1 #IHT1 #V #W #T1 #H1 destruct
@csx_intro #X #H1 #H2
elim (cpx_inv_appl1 … H1) -H1 *
qed-.
(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta (h) (G):
- ∀p,L,V,W,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]ⓝW.V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.ⓛ[p]W.T❫.
+lemma csx_appl_beta (h) (G) (L):
+ ∀p,V,W,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]ⓝW.V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.ⓛ[p]W.T.
/2 width=3 by csx_appl_beta_aux/ qed.
(* Advanced forward lemmas **************************************************)
-fact csx_fwd_bind_dx_unit_aux (h) (G):
- ∀L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ →
- ∀p,I,J,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓤ[J]❫ ⊢ ⬈*[h] 𝐒❪T❫.
+fact csx_fwd_bind_dx_unit_aux (h) (G) (L):
+ ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U →
+ ∀p,I,J,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓤ[J]❫ ⊢ ⬈*𝐒[h] T.
#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓑ[p, I]V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2
#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
-lemma csx_fwd_bind_dx_unit (h) (G):
- ∀p,I,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ →
- ∀J. ❪G,L.ⓤ[J]❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_bind_dx_unit (h) (G) (L):
+ ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T →
+ ∀J. ❪G,L.ⓤ[J]❫ ⊢ ⬈*𝐒[h] T.
/2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-.
-lemma csx_fwd_bind_unit (h) (G):
- ∀p,I,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ →
- â\88\80J. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d« â\88§ â\9dªG,L.â\93¤[J]â\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
+lemma csx_fwd_bind_unit (h) (G) (L):
+ ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T →
+ â\88\80J. â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92[h] V & â\9dªG,L.â\93¤[J]â\9d« â\8a¢ â¬\88*ð\9d\90\92[h] T.
/3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-.
(* Properties with restricted refinement for local environments *************)
-lemma csx_lsubr_conf (h) (G):
- ∀L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀L2. L1 ⫃ L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_lsubr_conf (h) (G) (L1):
+ ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ∀L2. L1 ⫃ L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
#h #G #L1 #T #H
@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
@csx_intro #T2 #HT12 #HnT12
(* Properties with sort-irrelevant equivalence for local environments *******)
(* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_reqx_conf: ∀h,G,L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ →
- ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_reqx_conf (h) (G) (L1):
+ ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T →
+ ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
#h #G #L1 #T #H
@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
@csx_intro #T2 #HT12 #HnT12
/5 width=5 by cpx_reqx_conf_sn, csx_teqx_trans, teqx_trans/
qed-.
-(* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_reqx_trans: ∀h,L1,L2,T. L1 ≛[T] L2 →
- ∀G. ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫.
+(* Basic_2A1: uses: csx_lleq_trans *)
+lemma csx_reqx_trans (h) (G) (L2):
+ ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T → ❪G,L1❫ ⊢ ⬈*𝐒[h] T.
/3 width=3 by csx_reqx_conf, reqx_sym/ qed-.
(* Properties with simple terms *********************************************)
-lemma csx_appl_simple: ∀h,G,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → ∀T1.
- (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T2❫) →
- 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T1❫.
+lemma csx_appl_simple (h) (G) (L):
+ ∀V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → ∀T1.
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T2) →
+ 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T1.
#h #G #L #V #H @(csx_ind … H) -V
#V #_ #IHV #T1 #IHT1 #HT1
@csx_intro #X #H1 #H2
(* Basic_1: was just: sn3_appl_appl *)
(* Basic_2A1: was: csx_appl_simple_tsts *)
lemma csx_appl_simple_teqo (h) (G) (L):
- ∀V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T2❫) →
- 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T1❫.
+ ∀V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T2) →
+ 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T1.
#h #G #L #V #H @(csx_ind … H) -V
#V #_ #IHV #T1 #H @(csx_ind … H) -T1
#T1 #H1T1 #IHT1 #H2T1 #H3T1
(* STRONGLY NORMALIZING TERMS VECTORS FOR UNBOUND PARALLEL RT-TRANSITION ****)
-definition csxv: ∀h. relation3 genv lenv (list term) ≝
- λh,G,L. all … (csx h G L).
+definition csxv (h) (G) (L): predicate (list term) ≝
+ all … (csx h G L).
interpretation
"strong normalization for unbound context-sensitive parallel rt-transition (term vector)"
(* Basic inversion lemmas ***************************************************)
-lemma csxv_inv_cons: ∀h,G,L,T,Ts. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T⨮Ts❫ →
- ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Ts❫.
+lemma csxv_inv_cons (h) (G) (L):
+ ∀T,Ts. ❪G,L❫ ⊢ ⬈*𝐒[h] T⨮Ts →
+ ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] T & ❪G,L❫ ⊢ ⬈*𝐒[h] Ts.
normalize // qed-.
(* Basic forward lemmas *****************************************************)
-lemma csx_fwd_applv: ∀h,G,L,T,Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫ →
- ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma csx_fwd_applv (h) (G) (L):
+ ∀T,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T →
+ ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] Vs & ❪G,L❫ ⊢ ⬈*𝐒[h] T.
#h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
#V #Vs #IHVs #HVs
lapply (csx_fwd_pair_sn … HVs) #HV
(* Properties with sn for unbound parallel rt-transition for terms **********)
(* Basic_2A1: was: csx_fpbs_conf *)
-lemma fpbs_csx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫.
+lemma fpbs_csx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2.
#h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
/2 width=5 by csx_fpbq_conf/
qed-.
inductive fsb (h): relation3 genv lenv term ≝
| fsb_intro: ∀G1,L1,T1. (
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → fsb h G2 L2 T2
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → fsb h G2 L2 T2
) → fsb h G1 L1 T1
.
(* Basic eliminators ********************************************************)
(* Note: eliminator with shorter ground hypothesis *)
-(* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***)
-lemma fsb_ind_alt: ∀h. ∀Q: relation3 …. (
- ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → (
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2
- ) → Q G1 L1 T1
- ) →
- ∀G,L,T. ≥[h] 𝐒❪G,L,T❫ → Q G L T.
+(* Note: to be named fsb_ind when fsb becomes a definition like csx, rsx ****)
+lemma fsb_ind_alt (h) (Q:relation3 …):
+ (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ≥𝐒[h] ❪G,L,T❫ → Q G L T.
#h #Q #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsb_intro/
qed-.
(* Main properties with atomic arity assignment for terms *******************)
-theorem aaa_fsb: ∀h,G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ≥[h] 𝐒❪G,L,T❫.
+theorem aaa_fsb (h):
+ ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ≥𝐒[h] ❪G,L,T❫.
/3 width=2 by aaa_csx, csx_fsb/ qed.
(* Advanced eliminators with atomic arity assignment for terms **************)
-fact aaa_ind_fpb_aux: ∀h. ∀Q:relation3 ….
- (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
+fact aaa_ind_fpb_aux (h) (Q:relation3 …):
+ (∀G1,L1,T1,A.
+ ❪G1,L1❫ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
#h #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1
/2 width=2 by fpb_fpbs/
qed-.
-lemma aaa_ind_fpb: ∀h. ∀Q:relation3 ….
- (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
+lemma aaa_ind_fpb (h) (Q:relation3 …):
+ (∀G1,L1,T1,A.
+ ❪G1,L1❫ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
-fact aaa_ind_fpbg_aux: ∀h. ∀Q:relation3 ….
- (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
+fact aaa_ind_fpbg_aux (h) (Q:relation3 …):
+ (∀G1,L1,T1,A.
+ ❪G1,L1❫ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
#h #Q #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1
/2 width=2 by fpbg_fwd_fpbs/
qed-.
-lemma aaa_ind_fpbg: ∀h. ∀Q:relation3 ….
- (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
+lemma aaa_ind_fpbg (h) (Q:relation3 …):
+ (∀G1,L1,T1,A.
+ ❪G1,L1❫ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
/4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-.
(* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
-lemma fsb_inv_csx: ∀h,G,L,T. ≥[h] 𝐒❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+lemma fsb_inv_csx (h):
+ ∀G,L,T. ≥𝐒[h] ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] T.
#h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
qed-.
(* Propreties with context-sensitive stringly rt-normalizing terms **********)
-lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫.
+lemma csx_fsb_fpbs (h):
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫.
#h #G1 #L1 #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
#G0 #L0 #T0 #IHu #H10
]
qed.
-lemma csx_fsb: ∀h,G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ≥[h] 𝐒❪G,L,T❫.
+lemma csx_fsb (h):
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ≥𝐒[h] ❪G,L,T❫.
/2 width=5 by csx_fsb_fpbs/ qed.
(* Advanced eliminators *****************************************************)
-lemma csx_ind_fpb: ∀h. ∀Q:relation3 genv lenv term.
- (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q G L T.
+lemma csx_ind_fpb (h) (Q:relation3 …):
+ (∀G1,L1,T1.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
-lemma csx_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term.
- (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q G L T.
+lemma csx_ind_fpbg (h) (Q:relation3 …):
+ (∀G1,L1,T1.
+ ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.
(* Properties with sort-irrelevant equivalence for closures *****************)
-lemma fsb_feqx_trans: ∀h,G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫.
+lemma fsb_feqx_trans: ∀h,G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫.
#h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12
@fsb_intro #G #L #T #H2
(* Properties with parallel rst-computation for closures ********************)
-lemma fsb_fpbs_trans: ∀h,G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫.
+lemma fsb_fpbs_trans: ∀h,G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫.
#h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
elim (fpbs_inv_fpbg … H12) -H12
(* Properties with proper parallel rst-computation for closures *************)
lemma fsb_intro_fpbg: ∀h,G1,L1,T1. (
- ∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫
- ) → ≥[h] 𝐒❪G1,L1,T1❫.
+ ∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫
+ ) → ≥𝐒[h] ❪G1,L1,T1❫.
/4 width=1 by fsb_intro, fpb_fpbg/ qed.
(* Eliminators with proper parallel rst-computation for closures ************)
lemma fsb_ind_fpbg_fpbs: ∀h. ∀Q:relation3 genv lenv term.
- (∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ →
+ (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
(∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
- ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ →
+ ∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → Q G2 L2 T2.
#h #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
qed-.
lemma fsb_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term.
- (∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ →
+ (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ →
(∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
- ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → Q G1 L1 T1.
+ ∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → Q G1 L1 T1.
#h #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
/3 width=1 by/
qed-.
(* Inversion lemmas with proper parallel rst-computation for closures *******)
lemma fsb_fpbg_refl_false (h) (G) (L) (T):
- ≥[h] 𝐒❪G,L,T❫ → ❪G,L,T❫ >[h] ❪G,L,T❫ → ⊥.
+ ≥𝐒[h] ❪G,L,T❫ → ❪G,L,T❫ >[h] ❪G,L,T❫ → ⊥.
#h #G #L #T #H
@(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
/2 width=5 by/
| jsx_bind: ∀I,K1,K2. jsx h G K1 K2 →
jsx h G (K1.ⓘ[I]) (K2.ⓘ[I])
| jsx_pair: ∀I,K1,K2,V. jsx h G K1 K2 →
- G ⊢ ⬈*[h,V] 𝐒❪K2❫ → jsx h G (K1.ⓑ[I]V) (K2.ⓧ)
+ G ⊢ ⬈*𝐒[h,V] K2 → jsx h G (K1.ⓑ[I]V) (K2.ⓧ)
.
interpretation
]
qed-.
-lemma jsx_inv_atom_sn (h) (G): ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆.
+lemma jsx_inv_atom_sn (h) (G):
+ ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆.
/2 width=5 by jsx_inv_atom_sn_aux/ qed-.
fact jsx_inv_bind_sn_aux (h) (G):
∀L1,L2. G ⊢ L1 ⊒[h] L2 →
∀I,K1. L1 = K1.ⓘ[I] →
∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I]
- | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & I = BPair J V & L2 = K2.ⓧ.
+ | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & I = BPair J V & L2 = K2.ⓧ.
#h #G #L1 #L2 * -L1 -L2
[ #J #L1 #H destruct
| #I #K1 #K2 #HK12 #J #L1 #H destruct /3 width=3 by ex2_intro, or_introl/
lemma jsx_inv_bind_sn (h) (G):
∀I,K1,L2. G ⊢ K1.ⓘ[I] ⊒[h] L2 →
∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I]
- | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & I = BPair J V & L2 = K2.ⓧ.
+ | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & I = BPair J V & L2 = K2.ⓧ.
/2 width=3 by jsx_inv_bind_sn_aux/ qed-.
(* Advanced inversion lemmas ************************************************)
lemma jsx_inv_pair_sn (h) (G):
∀I,K1,L2,V. G ⊢ K1.ⓑ[I]V ⊒[h] L2 →
∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓑ[I]V
- | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & L2 = K2.ⓧ.
+ | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & L2 = K2.ⓧ.
#h #G #I #K1 #L2 #V #H elim (jsx_inv_bind_sn … H) -H *
[ /3 width=3 by ex2_intro, or_introl/
| #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
lemma jsx_csx_conf (h) (G):
∀L1,L2. G ⊢ L1 ⊒[h] L2 →
- ∀T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫.
+ ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
(* Properties with strongly rt-normalizing referred local environments ******)
(* Note: Try by induction on the 2nd premise by generalizing V with f *)
lemma rsx_jsx_trans (h) (G):
- ∀L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ →
- ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒❪L2❫.
+ ∀L1,V. G ⊢ ⬈*𝐒[h,V] L1 →
+ ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*𝐒[h,V] L2.
#h #G #L1 #V @(fqup_wf_ind_eq (Ⓕ) … G L1 V) -G -L1 -V
#G0 #L0 #V0 #IH #G #L1 * *
[ //
∀L1,L2. G ⊢ L1 ⊒[h] L2 →
∀f. 𝐔❪f❫ → ∀I,K1,V. ⇩*[b,f]L1 ≘ K1.ⓑ[I]V →
∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V
- | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*[h,V] 𝐒❪K2❫.
+ | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*𝐒[h,V] K2.
#h #b #G #L1 #L2 #H elim H -L1 -L2
[ #f #_ #J #Y1 #X1 #H
lapply (drops_inv_atom1 … H) -H * #H #_ destruct
(* Forward lemmas with restricted refinement for local environments *********)
-lemma jsx_fwd_lsubr (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2.
+lemma jsx_fwd_lsubr (h) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2.
#h #G #L1 #L2 #H elim H -L1 -L2
/2 width=1 by lsubr_bind, lsubr_unit/
qed-.
(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
lemma rsx_cpx_trans_jsx (h) (G):
∀L0,T1,T2. ❪G,L0❫ ⊢ T1 ⬈[h] T2 →
- ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫.
+ ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L.
#h #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2
[ //
| //
(* Basic_2A1: uses: lsx_cpx_trans_O *)
lemma rsx_cpx_trans (h) (G):
∀L,T1,T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 →
- G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫.
+ G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L.
/3 width=6 by rsx_cpx_trans_jsx, jsx_refl/ qed-.
lemma rsx_cpxs_trans (h) (G):
∀L,T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 →
- G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫.
+ G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L.
#h #G #L #T1 #T2 #H
@(cpxs_ind_dx ???????? H) -T1 //
/3 width=3 by rsx_cpx_trans/
SN … (lpx h G) (reqx T).
interpretation
- "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
- 'PRedTySNStrong h T G L = (rsx h G T L).
+ "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
+ 'PRedTySNStrong h T G L = (rsx h G T L).
(* Basic eliminators ********************************************************)
(* Basic_2A1: uses: lsx_ind *)
-lemma rsx_ind (h) (G) (T) (Q:predicate lenv):
- (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
- Q L1
+lemma rsx_ind (h) (G) (T) (Q:predicate …):
+ (∀L1. G ⊢ ⬈*𝐒[h,T] L1 →
+ (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
+ Q L1
) →
- ∀L. G ⊢ ⬈*[h,T] 𝐒❪L❫ → Q L.
+ ∀L. G ⊢ ⬈*𝐒[h,T] L → Q L.
#h #G #T #Q #H0 #L1 #H elim H -L1
/5 width=1 by SN_intro/
qed-.
(* Basic_2A1: uses: lsx_intro *)
lemma rsx_intro (h) (G) (T):
∀L1.
- (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*[h,T] 𝐒❪L2❫) →
- G ⊢ ⬈*[h,T] 𝐒❪L1❫.
+ (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*𝐒[h,T] L2) →
+ G ⊢ ⬈*𝐒[h,T] L1.
/5 width=1 by SN_intro/ qed.
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
lemma rsx_fwd_pair_sn (h) (G):
- ∀I,L,V,T. G ⊢ ⬈*[h,②[I]V.T] 𝐒❪L❫ →
- G ⊢ ⬈*[h,V] 𝐒❪L❫.
+ ∀I,L,V,T. G ⊢ ⬈*𝐒[h,②[I]V.T] L →
+ G ⊢ ⬈*𝐒[h,V] L.
#h #G #I #L #V #T #H
@(rsx_ind … H) -L #L1 #_ #IHL1
@rsx_intro #L2 #HL12 #HnL12
(* Basic_2A1: uses: lsx_fwd_flat_dx *)
lemma rsx_fwd_flat_dx (h) (G):
- ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ →
- G ⊢ ⬈*[h,T] 𝐒❪L❫.
+ ∀I,L,V,T. G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L →
+ G ⊢ ⬈*𝐒[h,T] L.
#h #G #I #L #V #T #H
@(rsx_ind … H) -L #L1 #_ #IHL1
@rsx_intro #L2 #HL12 #HnL12
qed-.
fact rsx_fwd_pair_aux (h) (G):
- ∀L. G ⊢ ⬈*[h,#0] 𝐒❪L❫ →
- ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀L. G ⊢ ⬈*𝐒[h,#0] L →
+ ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K.
#h #G #L #H
@(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
/5 width=5 by lpx_pair, rsx_intro, reqx_fwd_zero_pair/
qed-.
lemma rsx_fwd_pair (h) (G):
- ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K.
/2 width=4 by rsx_fwd_pair_aux/ qed-.
(* Basic inversion lemmas ***************************************************)
(* Basic_2A1: uses: lsx_inv_flat *)
lemma rsx_inv_flat (h) (G):
- ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ →
- ∧∧ G ⊢ ⬈*[h,V] 𝐒❪L❫ & G ⊢ ⬈*[h,T] 𝐒❪L❫.
+ ∀I,L,V,T. G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L →
+ ∧∧ G ⊢ ⬈*𝐒[h,V] L & G ⊢ ⬈*𝐒[h,T] L.
/3 width=3 by rsx_fwd_pair_sn, rsx_fwd_flat_dx, conj/ qed-.
(* Basic_2A1: removed theorems 9:
(* Forward lemmas with strongly rt-normalizing terms ************************)
fact rsx_fwd_lref_pair_csx_aux (h) (G):
- ∀L. G ⊢ ⬈*[h,#0] 𝐒❪L❫ →
- ∀I,K,V. L = K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
+ ∀L. G ⊢ ⬈*𝐒[h,#0] L →
+ ∀I,K,V. L = K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*𝐒[h] V.
#h #G #L #H
@(rsx_ind … H) -L #L #_ #IH #I #K #V1 #H destruct
@csx_intro #V2 #HV12 #HnV12
qed-.
lemma rsx_fwd_lref_pair_csx (h) (G):
- ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
+ ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*𝐒[h] V.
/2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-.
lemma rsx_fwd_lref_pair_csx_drops (h) (G):
- ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫.
+ ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L → ❪G,K❫ ⊢ ⬈*𝐒[h] V.
#h #G #I #K #V #i elim i -i
[ #L #H >(drops_fwd_isid … H) -H
/2 width=2 by rsx_fwd_lref_pair_csx/
(* Inversion lemmas with strongly rt-normalizing terms **********************)
lemma rsx_inv_lref_pair (h) (G):
- ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ →
- ∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V →
+ ∧∧ ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K.
/3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-.
lemma rsx_inv_lref_pair_drops (h) (G):
- ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
- ∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L →
+ ∧∧ ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K.
/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
lemma rsx_inv_lref_drops (h) (G):
- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
+ ∀L,i. G ⊢ ⬈*𝐒[h,#i] L →
∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆
| ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I]
- | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K.
#h #G #L #i #H elim (drops_F_uni L i)
[ /2 width=1 by or3_intro0/
| * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
(* Note: swapping the eliminations to avoid rsx_cpx_trans: no solution found *)
(* Basic_2A1: uses: lsx_lref_be_lpxs *)
lemma rsx_lref_pair_lpxs (h) (G):
- ∀K1,V. ❪G,K1❫ ⊢ ⬈*[h] 𝐒❪V❫ →
- ∀K2. G ⊢ ⬈*[h,V] 𝐒❪K2❫ → ❪G,K1❫ ⊢ ⬈*[h] K2 →
- ∀I. G ⊢ ⬈*[h,#0] 𝐒❪K2.ⓑ[I]V❫.
+ ∀K1,V. ❪G,K1❫ ⊢ ⬈*𝐒[h] V →
+ ∀K2. G ⊢ ⬈*𝐒[h,V] K2 → ❪G,K1❫ ⊢ ⬈*[h] K2 →
+ ∀I. G ⊢ ⬈*𝐒[h,#0] K2.ⓑ[I]V.
#h #G #K1 #V #H
@(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H
@(rsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
qed.
lemma rsx_lref_pair (h) (G):
- ∀K,V. ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫ → ∀I. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫.
+ ∀K,V. ❪G,K❫ ⊢ ⬈*𝐒[h] V → G ⊢ ⬈*𝐒[h,V] K → ∀I. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V.
/2 width=3 by rsx_lref_pair_lpxs/ qed.
(* Basic_2A1: uses: lsx_lref_be *)
lemma rsx_lref_pair_drops (h) (G):
- ∀K,V. ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫ →
- ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
+ ∀K,V. ❪G,K❫ ⊢ ⬈*𝐒[h] V → G ⊢ ⬈*𝐒[h,V] K →
+ ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L.
#h #G #K #V #HV #HK #I #i elim i -i
[ #L #H >(drops_fwd_isid … H) -H /2 width=1 by rsx_lref_pair/
| #i #IH #L #H
(* Main properties with strongly rt-normalizing terms ***********************)
(* Basic_2A1: uses: csx_lsx *)
-theorem csx_rsx (h) (G): ∀L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → G ⊢ ⬈*[h,T] 𝐒❪L❫.
+theorem csx_rsx (h) (G):
+ ∀L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → G ⊢ ⬈*𝐒[h,T] L.
#h #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T
#Z #Y #X #IH #G #L * *
[ //
(* Note: this uses length *)
(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *)
-lemma rsx_lifts (h) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒❪L❫).
+lemma rsx_lifts (h) (G):
+ d_liftable1_isuni … (λL,T. G ⊢ ⬈*𝐒[h,T] L).
#h #G #K #T #H @(rsx_ind … H) -K
#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rsx_intro
#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12)
(* Inversion lemmas on relocation *******************************************)
(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *)
-lemma rsx_inv_lifts (h) (G): d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒❪L❫).
+lemma rsx_inv_lifts (h) (G):
+ d_deliftable1_isuni … (λL,T. G ⊢ ⬈*𝐒[h,T] L).
#h #G #L #U #H @(rsx_ind … H) -L
#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rsx_intro
#K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_lref_free *)
-lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
+lemma rsx_lref_atom_drops (h) (G):
+ ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → G ⊢ ⬈*𝐒[h,#i] L.
#h #G #L1 #i #HL1
@(rsx_lifts … (#0) … HL1) -HL1 //
qed.
(* Basic_2A1: uses: lsx_lref_skip *)
-lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
+lemma rsx_lref_unit_drops (h) (G):
+ ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*𝐒[h,#i] L.
#h #G #I #L1 #K1 #i #HL1
@(rsx_lifts … (#0) … HL1) -HL1 //
qed.
(* Basic_2A1: uses: lsx_fwd_lref_be *)
lemma rsx_fwd_lref_pair_drops (h) (G):
- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
- ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀L,i. G ⊢ ⬈*𝐒[h,#i] L →
+ ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K.
#h #G #L #i #HL #I #K #V #HLK
lapply (rsx_inv_lifts … HL … HLK … (#0) ?) -L
/2 width=2 by rsx_fwd_pair/
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_atom *)
-lemma lfsx_atom (h) (G) (T): G ⊢ ⬈*[h,T] 𝐒❪⋆❫.
+lemma lfsx_atom (h) (G) (T): G ⊢ ⬈*𝐒[h,T] ⋆.
#h #G #T
@rsx_intro #Y #H #HnT
lapply (lpx_inv_atom_sn … H) -H #H destruct
(* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *)
(* Note: the old proof without the exclusion binder requires lreq *)
lemma rsx_fwd_bind_dx_void (h) (G):
- ∀p,I,L,V,T. G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫ → G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫.
+ ∀p,I,L,V,T. G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L → G ⊢ ⬈*𝐒[h,T] L.ⓧ.
#h #G #p #I #L #V #T #H
@(rsx_ind … H) -L #L1 #_ #IH
@rsx_intro #Y #H #HT
(* Basic_2A1: uses: lsx_inv_bind *)
lemma rsx_inv_bind_void (h) (G):
- ∀p,I,L,V,T. G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫ →
- ∧∧ G ⊢ ⬈*[h,V] 𝐒❪L❫ & G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫.
+ ∀p,I,L,V,T. G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L →
+ ∧∧ G ⊢ ⬈*𝐒[h,V] L & G ⊢ ⬈*𝐒[h,T] L.ⓧ.
/3 width=4 by rsx_fwd_pair_sn, rsx_fwd_bind_dx_void, conj/ qed-.
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_sort *)
-lemma rsx_sort (h) (G): ∀L,s. G ⊢ ⬈*[h,⋆s] 𝐒❪L❫.
+lemma rsx_sort (h) (G): ∀L,s. G ⊢ ⬈*𝐒[h,⋆s] L.
#h #G #L1 #s @rsx_intro #L2 #H #Hs
elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_sort_length/
qed.
(* Basic_2A1: uses: lsx_gref *)
-lemma rsx_gref (h) (G): ∀L,l. G ⊢ ⬈*[h,§l] 𝐒❪L❫.
+lemma rsx_gref (h) (G): ∀L,l. G ⊢ ⬈*𝐒[h,§l] L.
#h #G #L1 #s @rsx_intro #L2 #H #Hs
elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_gref_length/
qed.
-lemma rsx_unit (h) (G): ∀I,L. G ⊢ ⬈*[h,#0] 𝐒❪L.ⓤ[I]❫.
+lemma rsx_unit (h) (G): ∀I,L. G ⊢ ⬈*𝐒[h,#0] L.ⓤ[I].
#h #G #I #L1 @rsx_intro
#Y #HY #HnY elim HnY -HnY
elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct
(* Basic_2A1: uses: lsx_intro_alt *)
lemma rsx_intro_lpxs (h) (G):
- ∀L1,T. (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*[h,T] 𝐒❪L2❫) →
- G ⊢ ⬈*[h,T] 𝐒❪L1❫.
+ ∀L1,T. (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*𝐒[h,T] L2) →
+ G ⊢ ⬈*𝐒[h,T] L1.
/4 width=1 by lpx_lpxs, rsx_intro/ qed-.
(* Basic_2A1: uses: lsx_lpxs_trans *)
lemma rsx_lpxs_trans (h) (G):
- ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- ∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫.
+ ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 →
+ ∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → G ⊢ ⬈*𝐒[h,T] L2.
#h #G #L1 #T #HL1 #L2 #H @(lpxs_ind_dx … H) -L2
/2 width=3 by rsx_lpx_trans/
qed-.
(* Eliminators with unbound rt-computation for full local environments ******)
lemma rsx_ind_lpxs_reqx (h) (G) (T) (Q:predicate lenv):
- (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
- Q L1
+ (∀L1. G ⊢ ⬈*𝐒[h,T] L1 →
+ (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
+ Q L1
) →
- ∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
+ ∀L1. G ⊢ ⬈*𝐒[h,T] L1 →
∀L0. ❪G,L1❫ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[T] L2 → Q L2.
#h #G #T #Q #IH #L1 #H @(rsx_ind … H) -L1
#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
(* Basic_2A1: uses: lsx_ind_alt *)
lemma rsx_ind_lpxs (h) (G) (T) (Q:predicate lenv):
- (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
- Q L1
+ (∀L1. G ⊢ ⬈*𝐒[h,T] L1 →
+ (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) →
+ Q L1
) →
- ∀L. G ⊢ ⬈*[h,T] 𝐒❪L❫ → Q L.
+ ∀L. G ⊢ ⬈*𝐒[h,T] L → Q L.
#h #G #T #Q #IH #L #HL
@(rsx_ind_lpxs_reqx … IH … HL) -IH -HL // (**) (* full auto fails *)
qed-.
(* Advanced properties ******************************************************)
fact rsx_bind_lpxs_aux (h) (G):
- ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ →
- ∀Y,T. G ⊢ ⬈*[h,T] 𝐒❪Y❫ →
+ ∀p,I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 →
+ ∀Y,T. G ⊢ ⬈*𝐒[h,T] Y →
∀L2. Y = L2.ⓑ[I]V → ❪G,L1❫ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫.
+ G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L2.
#h #G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1
#L1 #_ #IHL1 #Y #T #H @(rsx_ind_lpxs … H) -Y
#Y #HY #IHY #L2 #H #HL12 destruct
(* Basic_2A1: uses: lsx_bind *)
lemma rsx_bind (h) (G):
- ∀p,I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ →
- ∀T. G ⊢ ⬈*[h,T] 𝐒❪L.ⓑ[I]V❫ →
- G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫.
+ ∀p,I,L,V. G ⊢ ⬈*𝐒[h,V] L →
+ ∀T. G ⊢ ⬈*𝐒[h,T] L.ⓑ[I]V →
+ G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L.
/2 width=3 by rsx_bind_lpxs_aux/ qed.
(* Basic_2A1: uses: lsx_flat_lpxs *)
lemma rsx_flat_lpxs (h) (G):
- ∀I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ →
- ∀L2,T. G ⊢ ⬈*[h,T] 𝐒❪L2❫ → ❪G,L1❫ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L2❫.
+ ∀I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 →
+ ∀L2,T. G ⊢ ⬈*𝐒[h,T] L2 → ❪G,L1❫ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L2.
#h #G #I #L1 #V #H @(rsx_ind_lpxs … H) -L1
#L1 #HL1 #IHL1 #L2 #T #H @(rsx_ind_lpxs … H) -L2
#L2 #HL2 #IHL2 #HL12 @rsx_intro_lpxs
(* Basic_2A1: uses: lsx_flat *)
lemma rsx_flat (h) (G):
- ∀I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ →
- ∀T. G ⊢ ⬈*[h,T] 𝐒❪L❫ → G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫.
+ ∀I,L,V. G ⊢ ⬈*𝐒[h,V] L →
+ ∀T. G ⊢ ⬈*𝐒[h,T] L → G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L.
/2 width=3 by rsx_flat_lpxs/ qed.
fact rsx_bind_lpxs_void_aux (h) (G):
- ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ →
- ∀Y,T. G ⊢ ⬈*[h,T] 𝐒❪Y❫ →
+ ∀p,I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 →
+ ∀Y,T. G ⊢ ⬈*𝐒[h,T] Y →
∀L2. Y = L2.ⓧ → ❪G,L1❫ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫.
+ G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L2.
#h #G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1
#L1 #_ #IHL1 #Y #T #H @(rsx_ind_lpxs … H) -Y
#Y #HY #IHY #L2 #H #HL12 destruct
qed-.
lemma rsx_bind_void (h) (G):
- ∀p,I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ →
- ∀T. G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫ →
- G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫.
+ ∀p,I,L,V. G ⊢ ⬈*𝐒[h,V] L →
+ ∀T. G ⊢ ⬈*𝐒[h,T] L.ⓧ →
+ G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L.
/2 width=3 by rsx_bind_lpxs_void_aux/ qed.
(* Basic_2A1: uses: lsx_lleq_trans *)
lemma rsx_reqx_trans (h) (G):
- ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- ∀L2. L1 ≛[T] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫.
+ ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 →
+ ∀L2. L1 ≛[T] L2 → G ⊢ ⬈*𝐒[h,T] L2.
#h #G #L1 #T #H @(rsx_ind … H) -L1
#L1 #_ #IHL1 #L2 #HL12 @rsx_intro
#L #HL2 #HnL2 elim (reqx_lpx_trans … HL2 … HL12) -HL2
(* Basic_2A1: uses: lsx_lpx_trans *)
lemma rsx_lpx_trans (h) (G):
- ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ →
- ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫.
+ ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 →
+ ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → G ⊢ ⬈*𝐒[h,T] L2.
#h #G #L1 #T #H @(rsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
elim (reqx_dec L1 L2 T) /3 width=4 by rsx_reqx_trans/
qed-.
(* Basic_1: was: cpcs_dec *)
lemma csx_cpcs_dec (h) (G) (L):
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∀T2. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫ →
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∀T2. ❪G,L❫ ⊢ ⬈*𝐒[h] T2 →
Decidable … (❪G,L❫ ⊢ T1 ⬌*[h] T2).
#h #G #L #T1 #HT1 #T2 #HT2
elim (cprre_total_csx … HT1) -HT1 #U1 #HTU1
(* Basic inversion lemmas ***************************************************)
-lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]V.T❫ →
- â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªVâ\9d« â\88§ â\9dªG,L.â\93\9bVâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªTâ\9d«.
+lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓛ[p]V.T →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] V & â\9dªG,L.â\93\9bVâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] T.
#h #p #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (ⓛ[p]V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2
| #T2 #HT2 lapply (HVT1 (ⓛ[p]V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2
qed-.
(* Basic_2A1: was: cnx_inv_abbr *)
-lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪-ⓓV.T❫ →
- â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªVâ\9d« â\88§ â\9dªG,L.â\93\93Vâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªTâ\9d«.
+lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] -ⓓV.T →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] V & â\9dªG,L.â\93\93Vâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] T.
#h #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2
| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2
qed-.
(* Basic_2A1: was: cnx_inv_eps *)
-lemma cnx_inv_cast: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓝV.T❫ → ⊥.
+lemma cnx_inv_cast: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓝV.T → ⊥.
#h #G #L #V #T #H lapply (H T ?) -H
/2 width=6 by cpx_eps, teqx_inv_pair_xy_y/
qed-.
(* Basic properties *********************************************************)
-lemma cnx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈[h] 𝐍❪⋆s❫.
+lemma cnx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈𝐍[h] ⋆s.
#h #G #L #s #X #H elim (cpx_inv_sort1 … H) -H
/2 width=1 by teqx_sort/
qed.
-lemma cnx_abst: ∀h,p,G,L,W,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪W❫ → ❪G,L.ⓛW❫ ⊢ ⬈[h] 𝐍❪T❫ →
- ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]W.T❫.
+lemma cnx_abst: ∀h,p,G,L,W,T. ❪G,L❫ ⊢ ⬈𝐍[h] W → ❪G,L.ⓛW❫ ⊢ ⬈𝐍[h] T →
+ ❪G,L❫ ⊢ ⬈𝐍[h] ⓛ[p]W.T.
#h #p #G #L #W #T #HW #HT #X #H
elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@teqx_pair [ @HW | @HT ] // (**) (* auto fails because δ-expansion gets in the way *)
(* Advanced inversion lemmas ************************************************)
-lemma cnx_inv_abbr_pos (h) (G) (L): ∀V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪+ⓓV.T❫ → ⊥.
+lemma cnx_inv_abbr_pos (h) (G) (L):
+ ∀V,T. ❪G,L❫ ⊢ ⬈𝐍[h] +ⓓV.T → ⊥.
#h #G #L #V #U1 #H
elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
elim (teqx_dec U1 U2) #HnU12 [ -HU12 | -HTU2 ]
(* Advanced properties ******************************************************)
-lemma cnx_teqx_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ →
- ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T2❫.
+lemma cnx_teqx_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈𝐍[h] T1 →
+ ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈𝐍[h] T2.
#h #G #L #T1 #HT1 #T2 #HT12 #T #HT2
elim (teqx_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0
lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by teqx_repl/ (**) (* full auto fails *)
(* Properties with generic slicing ******************************************)
-lemma cnx_lref_atom: ∀h,G,L,i. ⇩[i] L ≘ ⋆ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫.
+lemma cnx_lref_atom: ∀h,G,L,i. ⇩[i] L ≘ ⋆ → ❪G,L❫ ⊢ ⬈𝐍[h] #i.
#h #G #L #i #Hi #X #H elim (cpx_inv_lref1_drops … H) -H // *
#I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
qed.
-lemma cnx_lref_unit: ∀h,I,G,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫.
+lemma cnx_lref_unit: ∀h,I,G,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → ❪G,L❫ ⊢ ⬈𝐍[h] #i.
#h #I #G #L #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // *
#Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct
qed.
(* Inversion lemmas with generic slicing ************************************)
(* Basic_2A1: was: cnx_inv_delta *)
-lemma cnx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫ → ⊥.
+lemma cnx_inv_lref_pair:
+ ∀h,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈𝐍[h] #i → ⊥.
#h #I #G #L #K #V #i #HLK #H
elim (lifts_total V (𝐔❨↑i❩)) #W #HVW
lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
(* Inversion lemmas with simple terms ***************************************)
-lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫ →
- ∧∧ ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ & ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ & 𝐒❪T❫.
+lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓐV.T →
+ ∧∧ ❪G,L❫ ⊢ ⬈𝐍[h] V & ❪G,L❫ ⊢ ⬈𝐍[h] T & 𝐒❪T❫.
#h #G #L #V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2
#H elim (teqx_inv_pair … H) -H //
(* Properties with simple terms *********************************************)
-lemma cnx_appl_simple: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → 𝐒❪T❫ →
- ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫.
+lemma cnx_appl_simple: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] V → ❪G,L❫ ⊢ ⬈𝐍[h] T → 𝐒❪T❫ →
+ ❪G,L❫ ⊢ ⬈𝐍[h] ⓐV.T.
#h #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H //
#V0 #T0 #HV0 #HT0 #H destruct
@teqx_pair [ @HV | @HT ] // (**) (* auto fails because δ-expansion gets in the way *)
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
- [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?] 𝐒❪?,?,?❫ )" "fsb_feqx" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
+ [ [ "strongly normalizing for closures" ] "fsb" + "( ≥𝐒[?] ❪?,?,?❫ )" "fsb_feqx" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
[ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ >[?] ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥[?] ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
[ { "unbound context-sensitive parallel rt-computation" * } {
[ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ]
- [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒❪?❫ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
- [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*[?] 𝐒❪?❫ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*[?] 𝐒❪?❫ )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqx" + "csx_feqx" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
+ [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*𝐒[?,?] ? )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
+ [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*𝐒[?] ? )" "csx_cnx_vector" + "csx_csx_vector" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒[?] ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqx" + "csx_feqx" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
[ [ "for lenvs on all entries" ] "lpxs" + "( ❪?,?❫ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_reqx" + "lpxs_feqx" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( ❪?,?❫ ⊢ ? ⬈*[?] ? )" * ]
[ [ "for terms" ] "cpxs" + "( ❪?,?❫ ⊢ ? ⬈*[?] ? )" "cpxs_teqx" + "cpxs_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_reqx" + "cpxs_feqx" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
[ { "unbound context-sensitive parallel rt-transition" * } {
- [ [ "normal form for terms" ] "cnx" + "( ❪?,?❫ ⊢ ⬈[?] 𝐍❪?❫ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ]
+ [ [ "normal form for terms" ] "cnx" + "( ❪?,?❫ ⊢ ⬈𝐍[?] ? )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ]
[ [ "for lenvs on referred entries" ] "rpx" + "( ❪?,?❫ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_reqx" + "rpx_lpx" + "rpx_rpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( ❪?,?❫ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_reqx" + "lpx_aaa" * ]
[ [ "for binders" ] "cpx_ext" + "( ❪?,?❫ ⊢ ? ⬈[?] ? )" * ]
projects / helm.git / commitdiff