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/grammar/term_vector.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 inductive at: list2 nat nat → relation nat ≝
28 | at_nil: ∀i. at ⟠ i i
29 | at_lt : ∀des,d,e,i1,i2. i1 < d →
30 at des i1 i2 → at ({d, e} :: des) i1 i2
31 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
32 at des (i1 + e) i2 → at ({d, e} :: des) i1 i2
35 interpretation "application (generic relocation with pairs)"
36 'RAt i1 des i2 = (at des i1 i2).
38 inductive minuss: nat → relation (list2 nat nat) ≝
39 | minuss_nil: ∀i. minuss i ⟠ ⟠
40 | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
41 minuss i ({d, e} :: des1) ({d - i, e} :: des2)
42 | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
43 minuss i ({d, e} :: des1) des2
46 interpretation "minus (generic relocation with pairs)"
47 'RMinus des1 i des2 = (minuss i des1 des2).