| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. â\93\9bV1) (L2.â\93\91{I} V2)
+ lsubs 0 (e + 1) (L1. â\93\91{I}V1) (L2. â\93\9bV2)
| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
.
"local environment refinement (substitution)"
'SubEq L1 d e L2 = (lsubs d e L1 L2).
-definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L1,s1,s2. R L1 s1 s2 →
- ∀L2,d,e. L1 ≼ [d, e] L2 → R L2 s1 s2.
+definition lsubs_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L2,s1,s2. R L2 s1 s2 →
+ ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
(* Basic properties *********************************************************)
qed.
lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
- L1. â\93\9bV1 â\89¼ [0, e] L2.â\93\91{I} V2.
+ L1. â\93\91{I}V1 â\89¼ [0, e] L2. â\93\9bV2.
#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
qed.
lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
- L1. â\93\91{I}V â\89¼ [0, e] L2.â\93\93V.
+ L1. â\93\93V â\89¼ [0, e] L2. â\93\91{I}V.
* /2 width=1/ qed.
lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
]
qed.
-lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R L))).
#S #R #HR #L1 #s1 #s2 #H elim H -s2
[ /3 width=5/
| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
L2 = ⋆ ∨ (d = 0 ∧ e = 0).
/2 width=3/ qed-.
-fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
- ∀K1,V. L1 = K1.ⓓV → d = 0 → 0 < e →
- ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubs_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
+ ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #K1 #V #H destruct
| #L1 #L2 #K1 #V #_ #_ #H
]
qed.
-lemma lsubs_inv_abbr1: ∀K1,L2,V,e. K1.ⓓV ≼ [0, e] L2 → 0 < e →
- ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
+ ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
/2 width=5/ qed-.
-fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
- ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
- ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
]
qed.
-lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
- ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
/2 width=5/ qed-.
(* Basic forward lemmas *****************************************************)