inductive at: list2 nat nat → relation nat ≝
| at_nil: ∀i. at ⟠ i i
| at_lt : ∀des,d,e,i1,i2. i1 < d →
- at des i1 i2 → at ({d, e} :: des) i1 i2
+ at des i1 i2 → at ({d, e} @ des) i1 i2
| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
- at des (i1 + e) i2 → at ({d, e} :: des) i1 i2
+ at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
.
interpretation "application (generic relocation with pairs)"
/2 width=3/ qed-.
fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
- ∀d,e,des0. des = {d, e} :: des0 →
+ ∀d,e,des0. des = {d, e} @ des0 →
i1 < d ∧ @[i1] des0 ≡ i2 ∨
d ≤ i1 ∧ @[i1 + e] des0 ≡ i2.
#des #i1 #i2 * -des -i1 -i2
]
qed.
-lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
i1 < d ∧ @[i1] des ≡ i2 ∨
d ≤ i1 ∧ @[i1 + e] des ≡ i2.
/2 width=3/ qed-.
-lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
i1 < d → @[i1] des ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
elim (lt_refl_false … Hd)
qed-.
-lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
d ≤ i1 → @[i1 + e] des ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1