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 "ground/notation/relations/ratsucc_3.ma".
16 include "ground/arith/nat_plus.ma".
17 include "ground/arith/nat_lt.ma".
18 include "ground/relocation/fr2_map.ma".
20 (* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
23 inductive fr2_nat: fr2_map → relation nat ≝
28 | fr2_nat_lt (f) (d) (h) (l1) (l2):
29 l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩◗f) l1 l2
31 | fr2_nat_ge (f) (d) (h) (l1) (l2):
32 d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩◗f) l1 l2
36 "non-negative relational application (finite relocation maps with pairs)"
37 'RAtSucc l1 f l2 = (fr2_nat f l1 l2).
39 (* Basic inversions *********************************************************)
42 lemma fr2_nat_inv_empty (l1) (l2):
43 @↑❨l1, 𝐞❩ ≘ l2 → l1 = l2.
44 #l1 #l2 @(insert_eq_1 … (𝐞))
47 | #f #d #h #l1 #l2 #_ #_ #H destruct
48 | #f #d #h #l1 #l2 #_ #_ #H destruct
53 lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2):
54 @↑❨l1, ❨d,h❩◗f❩ ≘ l2 →
55 ∨∨ ∧∧ l1 < d & @↑❨l1, f❩ ≘ l2
56 | ∧∧ d ≤ l1 & @↑❨l1+h, f❩ ≘ l2.
57 #g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g))
60 | #f1 #d1 #h1 #l1 #l2 #Hld1 #Hl12 #H destruct /3 width=1 by or_introl, conj/
61 | #f1 #d1 #h1 #l1 #l2 #Hdl1 #Hl12 #H destruct /3 width=1 by or_intror, conj/
66 lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2):
67 @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @↑❨l1, f❩ ≘ l2.
69 elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d
70 elim (nlt_ge_false … Hl1d Hdl1)
74 lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2):
75 @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @↑❨l1+h, f❩ ≘ l2.
77 elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1
78 elim (nlt_ge_false … Hl1d Hdl1)