(**************************************************************************)
include "basic_2/substitution/lift_neg.ma".
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/drop_drop.ma".
include "basic_2/multiple/llpx_sn.ma".
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
(* alternative definition of llpx_sn (recursive) *)
inductive llpx_sn_alt_r (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
| llpx_sn_alt_r_intro: ∀L1,L2,T,d.
- (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
+ (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
) →
- (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt_r R 0 V1 K1 K2
+ (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt_r R 0 V1 K1 K2
) → |L1| = |L2| → llpx_sn_alt_r R d T L1 L2
.
(* Compact definition of llpx_sn_alt_r **************************************)
lemma llpx_sn_alt_r_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
- (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2
) → llpx_sn_alt_r R d T L1 L2.
#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_intro // -HL12
lemma llpx_sn_alt_r_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
(∀L1,L2,T,d. |L1| = |L2| → (
- â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2
) → S d T L1 L2) →
∀L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → S d T L1 L2.
lemma llpx_sn_alt_r_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 →
|L1| = |L2| ∧
- â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2.
#R #L1 #L2 #T #d #H @(llpx_sn_alt_r_ind_alt … H) -L1 -L2 -T -d
#L1 #L2 #T #d #HL12 #IH @conj // -HL12
[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
/3 width=9 by nlift_bind_sn, and3_intro/
| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
- lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
- lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
+ lapply (drop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
+ lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/
@nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
]
lemma llpx_sn_alt_r_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt_r R d (#i) L1 L2 →
∨∨ |L1| ≤ i ∧ |L2| ≤ i
| yinj i < d
- | â\88\83â\88\83I,K1,K2,V1,V2. â\87©[i] L1 ≡ K1.ⓑ{I}V1 &
- â\87©[i] L2 ≡ K2.ⓑ{I}V2 &
+ | â\88\83â\88\83I,K1,K2,V1,V2. â¬\87[i] L1 ≡ K1.ⓑ{I}V1 &
+ â¬\87[i] L2 ≡ K2.ⓑ{I}V2 &
llpx_sn_alt_r R (yinj 0) V1 K1 K2 &
R K1 V1 V2 & d ≤ yinj i.
#R #L1 #L2 #d #i #H elim (llpx_sn_alt_r_inv_alt … H) -H
#HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
elim (ylt_split i d) /3 width=1 by or3_intro1/
-#Hdi #HL1 elim (ldrop_O1_lt (Ⓕ) … HL1)
-#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt (Ⓕ) L2 i) //
+#Hdi #HL1 elim (drop_O1_lt (Ⓕ) … HL1)
+#I1 #K1 #V1 #HLK1 elim (drop_O1_lt (Ⓕ) L2 i) //
#I2 #K2 #V2 #HLK2 elim (IH … HLK1 HLK2) -IH
/3 width=9 by nlift_lref_be_SO, or3_intro2, ex5_5_intro/
qed-.
llpx_sn_alt_r R d (#i) L1 L2.
#R #L1 #L2 #d #i #HL1 #_ #HL12 @llpx_sn_alt_r_intro_alt // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #j #_ #H #HLK1 elim (H (#(i-1))) -H
-lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
+lapply (drop_fwd_length_lt2 … HLK1) -HLK1
/3 width=3 by lift_lref_ge_minus, lt_to_le_to_lt/
qed.
lemma llpx_sn_alt_r_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
- â\87©[i] L1 â\89¡ K1.â\93\91{I}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I}V2 →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I}V2 →
llpx_sn_alt_r R 0 V1 K1 K2 → R K1 V1 V2 →
llpx_sn_alt_r R d (#i) L1 L2.
#R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_r_intro_alt
[ lapply (llpx_sn_alt_r_fwd_length … HK12) -HK12 #HK12
- @(ldrop_fwd_length_eq2 … HLK1 HLK2) normalize //
+ @(drop_fwd_length_eq2 … HLK1 HLK2) normalize //
| #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #Hdj #H #HLY1 #HLY2
elim (lt_or_eq_or_gt i j) #Hij destruct
[ elim (H (#i)) -H /2 width=1 by lift_lref_lt/
- | lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
- lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by and3_intro/
+ | lapply (drop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
+ lapply (drop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by and3_intro/
| elim (H (#(i-1))) -H /2 width=1 by lift_lref_ge_minus/
]
]
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
elim (nlift_inv_bind … HnVT) -HnVT #H
[ elim (IHV … HLK1 … HLK2) -IHV /2 width=2 by and3_intro/
-| elim IHT -IHT /2 width=12 by ldrop_drop, yle_succ, and3_intro/
+| elim IHT -IHT /2 width=12 by drop_drop, yle_succ, and3_intro/
]
qed.
#HL12 elim (llpx_sn_alt_r_fwd_lref … H) -H
[ * /2 width=1 by llpx_sn_free/
| /2 width=1 by llpx_sn_skip/
- | * /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+ | * /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
]
| #a #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_r_inv_bind … H) -H
/3 width=1 by llpx_sn_bind/
(* Alternative definition of llpx_sn (recursive) ****************************)
lemma llpx_sn_intro_alt_r: ∀R,L1,L2,T,d. |L1| = |L2| →
- (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ (â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2
) → llpx_sn R d T L1 L2.
#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_inv_lpx_sn
lemma llpx_sn_ind_alt_r: ∀R. ∀S:relation4 ynat term lenv lenv.
(∀L1,L2,T,d. |L1| = |L2| → (
- â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
) → S d T L1 L2) →
∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
lemma llpx_sn_inv_alt_r: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
|L1| = |L2| ∧
- â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â\87§[i, 1] U ≡ T → ⊥) →
- â\87©[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I2}V2 →
+ â\88\80I1,I2,K1,K2,V1,V2,i. d â\89¤ yinj i â\86\92 (â\88\80U. â¬\86[i, 1] U ≡ T → ⊥) →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I1}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I2}V2 →
∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H
#H elim (llpx_sn_alt_r_inv_alt … H) -H