(* 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 ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 →
+ ⇧[0, d] V2 ≡ U2 → L ⊢ ▼*[d, e] #i ≡ 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
qed.
fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
- ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+ ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
#L #T @(cw_wf_ind … L T) -L -T #L #T #IH * * /2 width=2/
[ #i #d #e #Hde #HL #H destruct
elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
lapply (lt_to_le_to_lt … Hide Hde) #Hi
- elim (ldrop_O1 … Hi) -Hi #I #K #V1 #HLK
+ elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
elim (IH … HKL … HK ?) -IH -HKL -HK
[3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
elim (lift_total V2 0 d) /3 width=7/
-| #I #V1 #T1 #d #e #Hde #HL #H destruct
+| #a #I #V1 #T1 #d #e #Hde #HL #H destruct
elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12
lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
qed.
lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
- ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+ ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
/2 width=2/ qed-.
(* 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 ⊢ ▼*[d, e] #i ≡ 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 ⊢ ▼*[d, e] #i ≡ U2 →
d ≤ i → i < d + e →
∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
- K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 &
+ K ⊢ ▼*[0, d + e - i - 1] V1 ≡ 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 ⊢ ▼*[d, e] #i ≡ 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 ⊢ ▼*[d, e] #i ≡ 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 ⊢ ▼*[0, d + e - i - 1] V1 ≡ 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 ⊢ ▼*[dt, et] T1 ≡ 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 ⊢ ▼*[dt, et] U1 ≡ 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 ⊢ ▼*[dt, et] T1 ≡ 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 ⊢ ▼*[dt, et + e] U1 ≡ 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 ⊢ ▼*[dt, et] T1 ≡ 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 ⊢ ▼*[dt + e, et] U1 ≡ 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_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 →
+lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ ▼*[d, e] U1 ≡ T2 →
∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2.
#L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1
lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct
lapply (lift_inj … HTU1 … HTU2) -U2 //
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 ⊢ ▼*[i, d + e - i] T1 ≡ T →
∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
- L ⊢ T1 ▼*[d, e] ≡ T2.
+ L ⊢ ▼*[d, e] T1 ≡ 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 //