(* *)
(**************************************************************************)
+include "ground/relocation/mr2_at.ma".
+include "ground/relocation/mr2_plus.ma".
include "basic_2A/notation/relations/rliftstar_3.ma".
include "basic_2A/substitution/lift.ma".
-include "basic_2A/multiple/mr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
-inductive lifts: list2 nat nat → relation term ≝
+inductive lifts: mr2 → relation term ≝
| lifts_nil : ∀T. lifts (◊) T T
| lifts_cons: ∀T1,T,T2,cs,l,m.
- ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2
+ ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2
.
interpretation "generic relocation (term)"
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
- ∀l,m,tl. cs = {l, m} @ tl →
+ ∀l,m,tl. cs = ❨l, m❩; tl →
∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
#T1 #T2 #cs * -T1 -T2 -cs
[ #T #l #m #tl #H destruct
/2 width=3 by ex2_intro/
qed-.
-lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[{l, m} @ cs] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩; cs] T1 ≡ T2 →
∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
/2 width=3 by lifts_inv_cons_aux/ qed-.
-(* Basic_1: was: lift1_sort *)
lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
#T2 #k #cs elim cs -cs
[ #H <(lifts_inv_nil … H) -H //
]
qed-.
-(* Basic_1: was: lift1_lref *)
lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
- â\88\83â\88\83i2. @â¦\83i1, csâ¦\84 â\89¡ i2 & T2 = #i2.
+ â\88\83â\88\83i2. @â\9dªi1, csâ\9d« â\89\98 i2 & T2 = #i2.
#T2 #cs elim cs -cs
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
| #l #m #cs #IH #i1 #H
]
qed-.
-(* Basic_1: was: lift1_bind *)
lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
T2 = ⓑ{a,I} V2. U2.
]
qed-.
-(* Basic_1: was: lift1_flat *)
lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
T2 = ⓕ{I} V2. U2.