]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_after_basic.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_after_basic.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/arith/nat_le_pred.ma".
16 include "ground/relocation/pr_basic.ma".
17 include "ground/relocation/pr_after_uni.ma".
18
19 (* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
20
21 (* Constructions with pr_basic **********************************************)
22
23 (*** after_basic_rc *)
24 lemma after_basic_rc (d2) (d1):
25       d1 ≤ d2 → ∀h2,h1.d2 ≤ h1+d1 → 𝐛❨d2,h2❩ ⊚ 𝐛❨d1,h1❩ ≘ 𝐛❨d1,h1+h2❩.
26 #d2 #d1 @(nat_ind_2_succ … d2 d1) -d2 -d1
27 [ #d1 #H #h2 #h1 #_
28   <(nle_inv_zero_dx … H) -d1 //
29 | #d2 #IH #_ #h2 #h1 <nplus_zero_dx #H
30   elim (nle_inv_succ_sn … H) -H #Hd2 #Hh1
31   >Hh1 -Hh1 <nplus_succ_sn
32   /3 width=7 by pr_after_push/
33 | #d2 #d1 #IH #H1 #h2 #h1 <nplus_succ_dx #H2
34   lapply (nle_inv_succ_bi … H1) -H1 #H1
35   lapply (nle_inv_succ_bi … H2) -H2 #H2
36   /3 width=7 by pr_after_refl/
37 ]
38 qed.