(* *)
(**************************************************************************)
+include "ground/xoa/ex_4_3.ma".
+include "ground/relocation/mr2_minus.ma".
include "basic_2A/notation/relations/rdropstar_3.ma".
include "basic_2A/notation/relations/rdropstar_4.ma".
include "basic_2A/substitution/drop.ma".
-include "basic_2A/multiple/mr2_minus.ma".
include "basic_2A/multiple/lifts_vector.ma".
(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
-inductive drops (s:bool): list2 nat nat → relation lenv ≝
-| drops_nil : ∀L. drops s (◊) L L
+inductive drops (s:bool): mr2 → relation lenv ≝
+| drops_nil : ∀L. drops s (𝐞) L L
| drops_cons: ∀L1,L,L2,cs,l,m.
- drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2
+ drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩◗ cs) L1 L2
.
interpretation "iterated slicing (local environment) abstract"
(* Basic inversion lemmas ***************************************************)
-fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = ◊ → L1 = L2.
+fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = 𝐞 → L1 = L2.
#L1 #L2 #s #cs * -L1 -L2 -cs //
#L1 #L #L2 #l #m #cs #_ #_ #H destruct
qed-.
-(* Basic_1: was: drop1_gen_pnil *)
-lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, ◊] L1 ≡ L2 → L1 = L2.
+lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, 𝐞] L1 ≡ L2 → L1 = L2.
/2 width=4 by drops_inv_nil_aux/ qed-.
fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
- ∀l,m,tl. cs = {l, m} @ tl →
+ ∀l,m,tl. cs = ❨l, m❩◗ tl →
∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
#L1 #L2 #s #cs * -L1 -L2 -cs
[ #L #l #m #tl #H destruct
]
qed-.
-(* Basic_1: was: drop1_gen_pcons *)
-lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, {l, m} @ cs] L1 ≡ L2 →
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩◗ cs] L1 ≡ L2 →
∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
/2 width=3 by drops_inv_cons_aux/ qed-.
-lemma drops_inv_skip2: â\88\80I,s,cs,cs2,i. cs â\96 i â\89¡ cs2 →
+lemma drops_inv_skip2: â\88\80I,s,cs,cs2,i. cs â\96 i â\89\98 cs2 →
∀L1,K2,V2. ⬇*[s, cs2] L1 ≡ K2. ⓑ{I} V2 →
- â\88\83â\88\83K1,V1,cs1. cs + 1 â\96 i + 1 â\89¡ cs1 + 1 &
+ â\88\83â\88\83K1,V1,cs1. cs + 1 â\96 i + 1 â\89\98 cs1 + 1 &
⬇*[s, cs1] K1 ≡ K2 &
⬆*[cs1] V2 ≡ V1 &
L1 = K1. ⓑ{I} V1.
(* Basic properties *********************************************************)
-(* Basic_1: was: drop1_skip_bind *)
lemma drops_skip: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → ∀V1,V2. ⬆*[cs] V2 ≡ V1 →
∀I. ⬇*[s, cs + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
#L1 #L2 #s #cs #H elim H -L1 -L2 -cs
#R #s #HR #L #K #cs #HLK #Ts #Us #H elim H -Ts -Us normalize //
#Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/
qed.
-
-(* Basic_1: removed theorems 1: drop1_getl_trans *)