rtm_step (mk_rtm (G. ⓛV) u E S (§p))
(mk_rtm G u E S V)
| rtm_tau : ∀G,u,E,S,W,T.
- rtm_step (mk_rtm G u E S (â\93£W. T))
+ rtm_step (mk_rtm G u E S (â\93\9dW. T))
(mk_rtm G u E S T)
| rtm_appl : ∀G,u,E,S,V,T.
rtm_step (mk_rtm G u E S (ⓐV. T))
(* Main properties **********************************************************)
theorem fsubst_delift: ∀K,V,T,L,d.
- ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
+ ⇩[0, d] L ≡ K. ⓓV → L ⊢ T ▼*[d, 1] ≡ [d ← V] T.
#K #V #T elim T -T
[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
elim (lt_or_eq_or_gt i d) #Hid
(* Main inversion properties ************************************************)
theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
- L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
+ L ⊢ T1 ▼*[d, 1] ≡ T2 → [d ← V] T1 = T2.
#K #V #T1 elim T1 -T1
[ * #i #L #T2 #d #HLK #H
[ -HLK >(delift_inv_sort1 … H) -H //
csubc/drop1 drop1_csubc_trans
csubc/drop drop_csubc_trans
-csubt/clear csubt_clear_conf
csubt/csuba csubt_csuba
-csubt/drop csubt_drop_flat
-csubt/drop csubt_drop_abbr
-csubt/drop csubt_drop_abst
csubt/fwd csubt_gen_abbr
csubt/fwd csubt_gen_abst
-csubt/fwd csubt_gen_flat
-csubt/fwd csubt_gen_bind
-csubt/getl csubt_getl_abbr
-csubt/getl csubt_getl_abst
csubt/pc3 csubt_pr2
csubt/pc3 csubt_pc3
-csubt/props csubt_refl
-csubt/ty3 csubt_ty3
-csubt/ty3 csubt_ty3_ld
+
csubv/clear csubv_clear_conf
csubv/clear csubv_clear_conf_void
csubv/drop csubv_drop_conf
∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
definition S6 ≝ λRP,C:lenv→predicate term.
- â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93£W. T).
+ â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93\9dW. T).
definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
qed-.
(* Basic_1: was: pr3_gen_cast *)
-lemma cprs_inv_cast1: â\88\80L,W1,T1,U2. L â\8a¢ â\93£W1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
- â\88\83â\88\83W2,T2. L â\8a¢ W1 â\9e¡* W2 & L â\8a¢ T1 â\9e¡* T2 & U2 = â\93£W2.T2.
+lemma cprs_inv_cast1: â\88\80L,W1,T1,U2. L â\8a¢ â\93\9dW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
+ â\88\83â\88\83W2,T2. L â\8a¢ W1 â\9e¡* W2 & L â\8a¢ T1 â\9e¡* T2 & U2 = â\93\9dW2.T2.
#L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
#U2 #U #_ #HU2 * /3 width=3/ *
#W #T #HW1 #HT1 #H destruct
(* Basic_1: was only: pr3_gen_cabbr *)
lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
- ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
- ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 [d, e] ≡ T2.
+ ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
]
qed-.
-lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93£W. T ➡* U →
- â\93£W. T ≃ U ∨ L ⊢ T ➡* U.
+lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93\9dW. T ➡* U →
+ â\93\9dW. T ≃ U ∨ L ⊢ T ➡* U.
#L #W #T #U #H
elim (cprs_inv_cast1 … H) -H /2 width=1/ *
#W0 #T0 #_ #_ #H destruct /2 width=1/
qed-.
(* Basic_1: was: pr3_iso_appls_cast *)
-lemma cprs_fwd_tau_vector: â\88\80L,Vs,W,T,U. L â\8a¢ â\92¶Vs. â\93£W. T ➡* U →
- â\92¶Vs. â\93£W. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
+lemma cprs_fwd_tau_vector: â\88\80L,Vs,W,T,U. L â\8a¢ â\92¶Vs. â\93\9dW. T ➡* U →
+ â\92¶Vs. â\93\9dW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/
#V #Vs #IHVs #W #T #U #H
elim (cprs_inv_appl1 … H) -H *
qed.
(* Basic_1: was: sn3_cast *)
-lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93£W. T.
+lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93\9dW. T.
#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_cast1 … H1) -H1
(* Basic_1: was: sn3_appls_cast *)
lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W →
∀Vs,T. L ⊢ ⬇* ⒶVs. T →
- L â\8a¢ â¬\87* â\92¶Vs. â\93£W. T.
+ L â\8a¢ â¬\87* â\92¶Vs. â\93\9dW. T.
#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
#V #Vs #IHV #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV
--- /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/dynamic/nta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Note: may not be transitive *)
+inductive lsubn (h:sh): relation lenv ≝
+| lsubn_atom: lsubn h (⋆) (⋆)
+| lsubn_pair: ∀I,L1,L2,W. lsubn h L1 L2 → lsubn h (L1. ⓑ{I} W) (L2. ⓑ{I} W)
+| lsubn_abbr: ∀L1,L2,V,W. ⦃h, L1⦄ ⊢ V : W → ⦃h, L2⦄ ⊢ V : W →
+ lsubn h L1 L2 → lsubn h (L1. ⓓV) (L2. ⓛW)
+.
+
+interpretation
+ "local environment refinement (native type assigment)"
+ 'CrSubEqN h L1 L2 = (lsubn h L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubn_inv_atom1_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#h #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubn_inv_atom1: ∀h,L2. h ⊢ ⋆ :⊑ L2 → L2 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubn_inv_pair1_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. h ⊢ K1 :⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W &
+ h ⊢ K1 :⊑ K2 & L2 = K2. ⓛW & I = Abbr.
+#h #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubn_inv_pair1: ∀h,I,K1,L2,V. h ⊢ K1. ⓑ{I} V :⊑ L2 →
+ (∃∃K2. h ⊢ K1 :⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W &
+ h ⊢ K1 :⊑ K2 & L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubn_inv_atom2_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#h #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubc_inv_atom2: ∀h,L1. h ⊢ L1 :⊑ ⋆ → L1 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubn_inv_pair2_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+ (∃∃K1. h ⊢ K1 :⊑ K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W &
+ h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst.
+#h #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
+]
+qed.
+
+(* Basic_1: was: csubt_gen_bind *)
+lemma lsubn_inv_pair2: ∀h,I,L1,K2,W. h ⊢ L1 :⊑ K2. ⓑ{I} W →
+ (∃∃K1. h ⊢ K1 :⊑ K2 & L1 = K1. ⓑ{I} W) ∨
+ ∃∃K1,V. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W &
+ h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst.
+/2 width=3/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: csubt_refl *)
+lemma lsubn_refl: ∀h,L. h ⊢ L :⊑ L.
+#h #L elim L -L // /2 width=1/
+qed.
+
+(* Basic_1: removed theorems 6:
+ csubt_gen_flat csubt_drop_flat csubt_clear_conf
+ csubt_getl_abbr csubt_getl_abst csubt_ty3_ld
+*)
--- /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/dynamic/lsubn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubn_ldrop_O1_conf: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. h ⊢ K1 :⊑ K2 & ⇩[0, e] L2 ≡ K2.
+#h #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+| #L1 #L2 #V #W #H1VW #H2VW #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+]
+qed.
+
+(* Note: the constant 0 cannot be generalized *)
+(* Basic_1: was only: csubt_drop_abbr csubt_drop_abst *)
+lemma lsubn_ldrop_O1_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. h ⊢ K1 :⊑ K2 & ⇩[0, e] L1 ≡ K1.
+#h #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V #W #H1VW #H2VW #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+]
+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/dynamic/nta_nta.ma".
+include "basic_2/dynamic/lsubn_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Properties concerning atomic arity assignment ****************************)
+
+(* Note: the corresponding confluence property does not hold *)
+(* Basic_1: was: csubt_ty3 *)
+axiom lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 →
+ ⦃h, L1⦄ ⊢ T : U.
+(*
+#h #L2 #T #U #H elim H -L2 -T -U
+[ //
+| #L2 #K2 #V2 #W2 #U2 #i #HLK2 #_ #WU2 #IHVW2 #L1 #HL12
+ elim (lsubn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubn_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct /3 width=6/
+ | #V1 #_ #_ #_ #_ #H destruct
+ ]
+| #L2 #K2 #W2 #V2 #U2 #i #HLK2 #_ #HWU2 #IHWV2 #L1 #HL12
+ elim (lsubn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubn_inv_pair2 … H) -H * #K1 [ | -IHWV2 ]
+ [ #HK12 #H destruct /3 width=6/
+ | #V1 #H1V1W2 #_ #_ #H #_ destruct /2 width=6/
+ ]
+| /4 width=2/
+| /3 width=1/
+| /3 width=2/
+| /3 width=1/
+]
+qed.
+*)
nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93£U. T) U
+| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93\9dU. T) U
| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
nta h L T U2
.
(* Basic_1: was: ty3_cast *)
lemma nta_cast_old: ∀h,L,W,T,U.
- â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : â\93£W.U.
+ â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : â\93\9dW.U.
/4 width=3/ qed.
(* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : T0.
+lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : T0.
/3 width=2/ qed.
(* Basic_1: removed theorems 4:
ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
| ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W →
ntaa h L (ⓐV.T) (ⓐV.U)
-| ntaa_cast: â\88\80L,T,U,W. ntaa h L T U â\86\92 ntaa h L U W â\86\92 ntaa h L (â\93£U. T) U
+| ntaa_cast: â\88\80L,T,U,W. ntaa h L T U â\86\92 ntaa h L U W â\86\92 ntaa h L (â\93\9dU. T) U
| ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 →
ntaa h L T U2
.
) →
(∀L,T,U,W.
⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
- R L T U â\86\92 R L U W â\86\92 R L (â\93£U.T) U
+ R L T U â\86\92 R L U W â\86\92 R L (â\93\9dU.T) U
) →
(∀L,T,U1,U2,V2.
⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
qed-.
-fact nta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\80X,Y. T = â\93£Y.X →
+fact nta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\80X,Y. T = â\93\9dY.X →
⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
#h #L #T #U #H elim H -L -T -U
[ #L #k #X #Y #H destruct
qed.
(* Basic_1: was: ty3_gen_cast *)
-lemma nta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93£Y.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+lemma nta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
/2 width=3/ qed-.
(* Advanced forvard lemmas **************************************************)
(* Advanced properties ******************************************************)
lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U →
- â¦\83h, Lâ¦\84 â\8a¢ â\93£W.T : U.
+ â¦\83h, Lâ¦\84 â\8a¢ â\93\9dW.T : U.
#h #L #T #W #U #HTW #HTU
lapply (nta_mono … HTW … HTU) #HWU
elim (nta_fwd_correct … HTU) -HTU /3 width=3/
(* Note: this is known as the substitution lemma *)
(* Basic_1: was only: ty3_gen_cabbr *)
lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
- ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 →
+ ∀L2,d,e. ≼ [d, e] L1 → L1 ▼*[d, e] ≡ L2 →
∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
- L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
+ L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
[ /2 width=5/
| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12
lemma nta_ldrop_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
∀L2,d,e. ≼ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
- L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2.
+ L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
/3 width=1/ qed.
(* Basic_1: was only: pc3_gen_cabbr *)
lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 →
- ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
- ∀T2. L ⊢ U2 [d, e] ≡ T2 → K ⊢ T1 ⬌* T2.
+ ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
+ ∀T2. L ⊢ U2 ▼*[d, e] ≡ T2 → K ⊢ T1 ⬌* T2.
#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2
elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2
elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT
--- /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/dynamic/lsubn_nta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Main properties **********************************************************)
+
+(* Note: new property *)
+theorem lsubn_trans: ∀h,L1,L. h ⊢ L1 :⊑ L → ∀L2. h ⊢ L :⊑ L2 → h ⊢ L1 :⊑ L2.
+#h #L1 #L #H elim H -L1 -L
+[ #X #H >(lsubn_inv_atom1 … H) -H //
+| #I #L1 #L #V #HL1 #H1W #IHL1 #X #H
+ elim (lsubn_inv_pair1 … H) -H * #L2
+ [ #HL2 #H #H2W destruct /4 width=1/
+ | #W #H1VW #H2VW #HL2 #H1 #H2 destruct /3 width=3/
+ ]
+| #L1 #L #V1 #W1 #H1VW1 #H2VW1 #HL1 #IHL1 #X #H
+ elim (lsubn_inv_pair1 … H) -H * #L2
+ [ #HL2 #H #HW destruct /3 width=1/
+ | #V #_ #_ #_ #_ #H destruct
+ ]
+]
+qed.
d: abbreviation
f: flat
l: abstraction
-t: native type annotation
+n: native type annotation
non associative with precedence 55
for @{ 'SnAppl $T1 $T2 }.
-notation "hvbox( â\93£ term 55 T1 . break term 55 T2 )"
+notation "hvbox( â\93\9d term 55 T1 . break term 55 T2 )"
non associative with precedence 55
for @{ 'SnCast $T1 $T2 }.
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
-notation "hvbox( T1 break [ d , break e ] ≡ break term 46 T2 )"
+notation "hvbox( T1 break ▼* [ d , break e ] ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break ▼* [ d , break e ] ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
-notation "hvbox( T1 break [ d , break e ] ≡ ≡ break term 46 T2 )"
+notation "hvbox( T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $T1 $d $e $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ ≡ break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
qed.
lemma cpr_cast: ∀L,V,T1,T2.
- L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â\93£V. T1 ➡ T2.
+ L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â\93\9dV. T1 ➡ T2.
#L #V #T1 #T2 * /3 width=3/
qed.
qed-.
(* Basic_1: was: pr2_gen_cast *)
-lemma cpr_inv_cast1: â\88\80L,V1,T1,U2. L â\8a¢ â\93£V1. T1 ➡ U2 → (
+lemma cpr_inv_cast1: â\88\80L,V1,T1,U2. L â\8a¢ â\93\9dV1. T1 ➡ U2 → (
∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
- U2 = â\93£V2. T2
+ U2 = â\93\9dV2. T2
) ∨ L ⊢ T1 ➡ U2.
#L #V1 #T1 #U2 * #X #H #HU2
elim (tpr_inv_cast1 … H) -H /3 width=3/
(* Basic_1: was only: pr2_gen_cabbr *)
lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 →
- ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
- ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2.
+ ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
+ ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
#L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT
elim (le_or_ge (|L|) d) #Hd
* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
-lemma tif_inv_cast: â\88\80V,T. ð\9d\90\88â¦\83â\93£V.T⦄ → ⊥.
+lemma tif_inv_cast: â\88\80V,T. ð\9d\90\88â¦\83â\93\9dV.T⦄ → ⊥.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
]
qed.
-lemma tnf_inv_cast: â\88\80V,T. ð\9d\90\8dâ¦\83â\93£V.T⦄ → ⊥.
+lemma tnf_inv_cast: â\88\80V,T. ð\9d\90\8dâ¦\83â\93\9dV.T⦄ → ⊥.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@discr_tpair_xy_y //
qed-.
tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
-| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93£V. T1) T2
+| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93\9dV. T1) T2
.
interpretation
qed-.
(* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93£V1. T1 ➡ U2 →
- (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93£V2. T2)
+lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93\9dV1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93\9dV2. T2)
∨ T1 ➡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=5/
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3:
(* Properties on inverse basic term relocation ******************************)
-lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 [d, e] ≡ T1 →
- ∃∃T2. T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2.
+lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e] ≡ T1 →
+ ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
#U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
elim (tpr_inv_lift … HWU1 … HTW1) -W1 /3 width=5/
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 →
- â\88\83â\88\83X. â\93£V1. T1 ➡ X & X2 ➡ X.
+ â\88\83â\88\83X. â\93\9dV1. T1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/
qed.
| trf_appl_sn: ∀V,T. trf V → trf (ⓐV. T)
| trf_appl_dx: ∀V,T. trf T → trf (ⓐV. T)
| trf_abbr : ∀V,T. trf (ⓓV. T)
-| trf_cast : â\88\80V,T. trf (â\93£V. T)
+| trf_cast : â\88\80V,T. trf (â\93\9dV. T)
| trf_beta : ∀V,W,T. trf (ⓐV. ⓛW. T)
.
| aaa_abst: ∀L,V,T,B,A.
aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛV. T) (②B. A)
| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
-| aaa_cast: â\88\80L,V,T,A. aaa L V A â\86\92 aaa L T A â\86\92 aaa L (â\93£V. T) A
+| aaa_cast: â\88\80L,V,T,A. aaa L V A â\86\92 aaa L T A â\86\92 aaa L (â\93\9dV. T) A
.
interpretation "atomic arity assignment (term)"
∃∃B. L ⊢ V ⁝ B & L ⊢ T ⁝ ②B. A.
/2 width=3/ qed-.
-fact aaa_inv_cast_aux: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80W,U. T = â\93£W. U →
+fact aaa_inv_cast_aux: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80W,U. T = â\93\9dW. U →
L ⊢ W ⁝ A ∧ L ⊢ U ⁝ A.
#L #T #A * -L -T -A
[ #L #k #W #U #H destruct
]
qed.
-lemma aaa_inv_cast: â\88\80L,W,T,A. L â\8a¢ â\93£W. T ⁝ A →
+lemma aaa_inv_cast: â\88\80L,W,T,A. L â\8a¢ â\93\9dW. T ⁝ A →
L ⊢ W ⁝ A ∧ L ⊢ T ⁝ A.
/2 width=3/ qed-.
sta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
| sta_appl: ∀L,V,T,U. sta h L T U →
sta h L (ⓐV.T) (ⓐV.U)
-| sta_cast: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93£W. T) U
+| sta_cast: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93\9dW. T) U
.
interpretation "static type assignment (term)"
∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
/2 width=3/ qed-.
-fact sta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93£Y.X →
+fact sta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93\9dY.X →
⦃h, L⦄ ⊢ X • U.
#h #L #T #U * -L -T -U
[ #L #k #X #Y #H destruct
qed.
(* Basic_1: was: sty0_gen_cast *)
-lemma sta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93£Y.X • U → ⦃h, L⦄ ⊢ X • U.
+lemma sta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dY.X • U → ⦃h, L⦄ ⊢ X • U.
/2 width=4/ qed-.
(* Basic properties *********************************************************)
lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
- ∀L. L ⊢ T2 [d, e] ≡ T1.
+ ∀L. L ⊢ T2 ▼*[d, e] ≡ T1.
/2 width=3/ qed.
-lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T.
+lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T.
/2 width=3/ qed.
-lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
- ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡ T2.
+lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 →
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼*[d, e] ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
-lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k [d, e] ≡ ⋆k.
+lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ ⋆k.
/2 width=3/ qed.
-lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i [d, e] ≡ #i.
+lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i ▼*[d, e] ≡ #i.
/3 width=3/ qed.
-lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i [d, e] ≡ #(i - e).
+lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i ▼*[d, e] ≡ #(i - e).
/3 width=3/ qed.
-lemma delift_gref: ∀L,d,e,p. L ⊢ §p [d, e] ≡ §p.
+lemma delift_gref: ∀L,d,e,p. L ⊢ §p ▼*[d, e] ≡ §p.
/2 width=3/ qed.
lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
- L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2.
+ L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 →
+ L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
qed.
lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 →
- L ⊢ ⓕ{I} V1. T1 [d, e] ≡ ⓕ{I} V2. T2.
+ L ⊢ V1 ▼*[d, e] ≡ V2 → L ⊢ T1 ▼*[d, e] ≡ T2 →
+ L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ ⓕ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k.
+lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ U2 → U2 = ⋆k.
#L #U2 #d #e #k * #U #HU
>(tpss_inv_sort1 … HU) -HU #HU2
>(lift_inv_sort2 … HU2) -HU2 //
qed-.
-lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p.
+lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p ▼*[d, e] ≡ U2 → U2 = §p.
#L #U #d #e #p * #U #HU
>(tpss_inv_gref1 … HU) -HU #HU2
>(lift_inv_gref2 … HU2) -HU2 //
qed-.
-lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
- L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
+lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ U2 →
+ ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 &
+ L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 &
U2 = ⓑ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
qed-.
-lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
- L ⊢ T1 [d, e] ≡ T2 &
+lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ U2 →
+ ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 &
+ L ⊢ T1 ▼*[d, e] ≡ T2 &
U2 = ⓕ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct
elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
qed-.
-lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2.
+lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2.
#L #T1 #T2 #d * #T #HT1
>(tpss_inv_refl_O2 … HT1) -HT1 #HT2
>(lift_inv_refl_O2 … HT2) -HT2 //
(* Basic properties *********************************************************)
-lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 →
- ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
+lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 →
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼▼*[d, e] ≡ T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
]
qed.
-lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡≡ T2.
+lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼▼*[d, e] ≡ T2.
#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1
[ * #i #IH #T2 #d #e #H
[ >(delift_inv_sort1 … H) -H //
(* Basic inversion lemmas ***************************************************)
-lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡≡ T2 → L ⊢ T1 [d, e] ≡ T2.
+lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 ▼▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
qed-.
(∀L,d,e,k. R d e L (⋆k) (⋆k)) →
(∀L,d,e,i. i < d → R d e L (#i) (#i)) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
- ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ≡ V2 →
+ ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▼*[O, d + e - i - 1] ≡ V2 →
⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
) →
(∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
(∀L,d,e,p. R d e L (§p) (§p)) →
- (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
- L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ≡ T2 → R d e L V1 V2 →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 →
+ L.ⓑ{I}V2 ⊢ T1 ▼*[d + 1, e] ≡ T2 → R d e L V1 V2 →
R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
) →
- (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
- L⊢ T1 [d, e] ≡ T2 → R d e L V1 V2 →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 →
+ L⊢ T1 ▼*[d, e] ≡ T2 → R d e L V1 V2 →
R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
) →
- ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ≡ T2 → R d e L T1 T2.
+ ∀d,e,L,T1,T2. L ⊢ T1 ▼*[d, e] ≡ T2 → R d e L T1 T2.
#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e
// /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/
qed-.
(* Main properties **********************************************************)
theorem delift_mono: ∀L,T,T1,T2,d,e.
- L ⊢ T [d, e] ≡ T1 → L ⊢ T [d, e] ≡ T2 → T1 = T2.
+ L ⊢ T ▼*[d, e] ≡ T1 → L ⊢ T ▼*[d, e] ≡ T2 → T1 = T2.
#L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2
elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2
lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct
(* Advanced properties ******************************************************)
lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
- ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 →
- ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2.
+ ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 →
+ ⇧[0, d] V2 ≡ U2 → L ⊢ #i ▼*[d, e] ≡ U2.
#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
elim (lift_total V 0 (i+1)) #U #HVU
lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
(* Advanced inversion lemmas ************************************************)
-lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
+lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → i < d → U2 = #i.
#L #U2 #i #d #e * #U #HU #HU2 #Hid
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct >(lift_inv_lref2_lt … HU2) //
]
qed-.
-lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i ▼*[d, e] ≡ U2 →
d ≤ i → i < d + e →
∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
+ K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
⇧[0, d] V2 ≡ U2.
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
]
qed-.
-lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
d + e ≤ i → U2 = #(i - e).
#L #U2 #i #d #e * #U #HU #HU2 #Hdei
elim (tpss_inv_lref1 … HU) -HU
]
qed-.
-lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 →
∨∨ (i < d ∧ U2 = #i)
| (∃∃K,V1,V2. d ≤ i & i < d + e &
⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
+ K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
⇧[0, d] V2 ≡ U2
)
| (d + e ≤ i ∧ U2 = #(i - e)).
(* Properties on basic term relocation **************************************)
-lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
- L ⊢ U1 [dt, et] ≡ U2.
+ L ⊢ U1 ▼*[dt, et] ≡ U2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
qed.
-lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
- L ⊢ U1 [dt, et + e] ≡ T2.
+ L ⊢ U1 ▼*[dt, et + e] ≡ T2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
qed.
-lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 →
∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- L ⊢ U1 [dt + e, et] ≡ U2.
+ L ⊢ U1 ▼*[dt + e, et] ≡ U2.
#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
elim (lift_total T d e) #U #HTU
lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
qed.
-lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 [i, d + e - i] ≡ T →
+lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T →
∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
- L ⊢ T1 [d, e] ≡ T2.
+ L ⊢ T1 ▼*[d, e] ≡ T2.
#L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide
lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10
lapply (lift_trans_be … HT2 … HT0 ? ?) -T //
(* Properties on partial unfold on local environments ***********************)
-lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 →
- ∀K. L ▶* [d, e] K → K ⊢ T1 [d, e] ≡ T2.
+lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 →
+ ∀K. L ▶* [d, e] K → K ⊢ T1 ▼*[d, e] ≡ T2.
#L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK
elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0
lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/
qed.
lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K →
- ∀T1,T2. K ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡ T2.
+ ∀T1,T2. K ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2.
#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
qed.
(* Properties on partial unfold on terms ************************************)
lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2.
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/
qed.
lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
- ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2.
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=3/ qed.
lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/
qed.
lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=6/ qed.
lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/
qed.
lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=3/ qed.
lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
+ ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T.
#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/
qed.
lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
+ ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T.
/3 width=3/ qed.
lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
+ ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T.
#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/
qed.
lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
+ ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T.
/3 width=3/ qed.
#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL10 #H1 #H2 destruct
+| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
- elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
+ elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tpss_fwd_tw … HV01) #H2
lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
(* Basic properties *********************************************************)
-lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 [d, e] ≡ L2.
+lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 ▼*[d, e] ≡ L2.
/2 width=3/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 [0, e] ≡ L2 → 0 < e →
- K1 [0, e - 1] ≡ L2.
+lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 ▼*[0, e] ≡ L2 → 0 < e →
+ K1 ▼*[0, e - 1] ≡ L2.
#I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e
elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct
lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/
(* Inversion lemmas on inverse basic term relocation ************************)
-lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 [d, e] ≡ L2 → 0 < d →
- ∃∃K2,V2. K1 [d - 1, e] ≡ K2 &
- K1 ⊢ V1 [d - 1, e] ≡ V2 &
+lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 ▼*[d, e] ≡ L2 → 0 < d →
+ ∃∃K2,V2. K1 ▼*[d - 1, e] ≡ K2 &
+ K1 ⊢ V1 ▼*[d - 1, e] ≡ V2 &
L2 = K2. ⓑ{I} V2.
#I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e
elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
(* Properties on inverse basic term relocation ******************************)
-lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 →
- ∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2.
+lemma thin_delift1: ∀L1,L2,d,e. L1 ▼*[d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 ▼*[d, e] ≡ V2 →
+ ∀I. L1.ⓑ{I}V1 ▼*[d + 1, e] ≡ L2.ⓑ{I}V2.
#L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I
elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0
elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // <minus_n_n #X #H1 #H2
qed.
lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K → d + e ≤ dd →
∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K → d + e ≤ dd →
∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=3/ qed.
lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K →
d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee
lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
qed.
lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
- ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
+ ∀K. L ▼*[dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
- L ⊢ U2 [dd, ee] ≡ T2.
+ L ⊢ U2 ▼*[dd, ee] ≡ T2.
/3 width=3/ qed.
(* Properties on local environment slicing **********************************)
-lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
#L0 #L1 #d1 #e1 * /3 width=8 by ltpss_ldrop_conf_ge, ldrop_conf_ge/
qed.
-lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 [0, d1 + e1 - e2] ≡ L & ⇩[0, d1] L1 ≡ L.
+ ∃∃L. L2 ▼*[0, d1 + e1 - e2] ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
elim (ltpss_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
qed.
-lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▼*[d1, e1] ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 [d1 - e2, e1] ≡ L & ⇩[0, e2] L1 ≡ L.
+ ∃∃L. L2 ▼*[d1 - e2, e1] ≡ L & ⇩[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
elim (ltpss_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
qed.
-lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≡ L0 →
+lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▼*[d1, e1] ≡ L0 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
lapply (ltpss_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
qed.
-lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≡ L0 →
+lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▼*[d1, e1] ≡ L0 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L [d1 - e2, e1] ≡ L2 & ⇩[0, e2] L1 ≡ L.
+ ∃∃L. L ▼*[d1 - e2, e1] ≡ L2 & ⇩[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
elim (ltpss_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
["("; "❨"; "❪"; "❲"; "（"; ];
[")"; "❩"; "❫"; "❳"; "）"; ];
["["; "〚"; ] ;
- ["]"; "〛"; ] ;
+ ["]"; "〛"; ] ;
["{"; "❴"; "⦃" ] ;
["}"; "❵"; "⦄" ] ;
["□"; "◽"; "▪"; "◾"; ];
["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
- ["▸"; "►"; "▶"; ] ;
- [">"; "〉"; "»"; "❭"; "❯"; "❱"; ] ;
+ [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ;
["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ;
["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;
- ["T"; "𝕋"; "𝐓"; "Ⓣ"; ] ;
+ ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ;
["u"; "𝕦"; "𝐮"; "ⓤ"; ] ;
["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ;
- ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; ] ;
+ ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ;
["V"; "𝕍"; "𝐕"; "Ⓥ"; ] ;
["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; "ⓦ"; ] ;
["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; "Ⓦ"; ] ;
projects / helm.git / commitdiff