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/relocation/rtmap_basic_after.ma".
16 include "static_2/notation/relations/rlift_4.ma".
17 include "static_2/relocation/lifts.ma".
19 (* GENERIC RELOCATION FOR TERMS *********************************************)
21 interpretation "basic relocation (term)"
22 'RLift m n T1 T2 = (lifts (basic m n) T1 T2).
24 (* Properties with basic relocation *****************************************)
26 lemma lifts_lref_lt (m,n,i): i < m → ⇧[m,n] #i ≘ #i.
27 /3 width=1 by lifts_lref, pr_pat_basic_lt/ qed.
29 lemma lifts_lref_ge (m,n,i): m ≤ i → ⇧[m,n] #i ≘ #(n+i).
30 /3 width=1 by lifts_lref, pr_pat_basic_ge/ qed.
32 lemma lifts_lref_ge_minus (m,n,i): n+m ≤ i → ⇧[m,n] #(i-n) ≘ #i.
34 >(nplus_minus_sn_refl_sn i n) in ⊢ (???%);
35 /3 width=2 by lifts_lref_ge, nle_minus_dx_dx, nle_inv_plus_sn_dx/