1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/unfold/gr2.ma".
17 (* GENERIC RELOCATION WITH PAIRS ********************************************)
19 let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
21 | cons2 d e des ⇒ {d + i, e} :: pluss des i
24 interpretation "plus (generic relocation with pairs)"
25 'plus x y = (pluss x y).
27 (* Basic inversion lemmas ***************************************************)
29 lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠.
31 #d #e #des #H destruct
34 lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} :: des2 →
35 ∃∃des1. des1 + i = des2 & des = {d - i, e} :: des1.
36 #i #d #e #des2 * normalize
38 | #d1 #e1 #des1 #H destruct /2 width=3/