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/arith/nat_le_pred.ma".
16 include "ground/relocation/rtmap_after_uni.ma".
17 include "ground/relocation/rtmap_basic.ma".
19 (* RELOCATION MAP ***********************************************************)
21 (* Properties with composition **********************************************)
23 lemma after_basic_rc (m2,m1):
24 m1 ≤ m2 → ∀n2,n1.m2 ≤ n1+m1 → 𝐁❨m2,n2❩ ⊚ 𝐁❨m1,n1❩ ≘ 𝐁❨m1,n1+n2❩.
25 #m2 #m1 @(nat_ind_2_succ … m2 m1) -m2 -m1
27 <(nle_inv_zero_dx … H) -m1 //
28 | #m2 #IH #_ #n2 #n1 <nplus_zero_dx #H
29 elim (nle_inv_succ_sn … H) -H #Hm2 #Hn1
30 >Hn1 -Hn1 <nplus_succ_sn
31 /3 width=7 by after_push/
32 | #m2 #m1 #IH #H1 #n2 #n1 <nplus_succ_dx #H2
33 lapply (nle_inv_succ_bi … H1) -H1 #H1
34 lapply (nle_inv_succ_bi … H2) -H2 #H2
35 /3 width=7 by after_refl/