matita/matita/contribs/lambdadelta/ground/relocation/gr_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/gr_basic.ma".
  17 include "ground/relocation/gr_after_uni.ma".
  18
  19 (* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
  20
  21 (* Constructions with gr_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 gr_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 gr_after_refl/
  37 ]
  38 qed.