matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_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_2/relocation/rtmap_basic.ma".
  16 include "ground_2/relocation/nstream_after.ma".
  17
  18 (* RELOCATION N-STREAM ******************************************************)
  19
  20 (* Specific properties on basic relocation **********************************)
  21
  22 lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❴m,n❵@❴i❵ = i.
  23 /3 width=1 by at_inv_total, at_basic_lt/ qed-.
  24
  25 lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❴m,n❵@❴i❵ = n+i.
  26 /3 width=1 by at_inv_total, at_basic_ge/ qed-.
  27
  28 (* Specific main properties on basic relocation *****************************)
  29
  30 theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
  31                     ∀h1,h2. 𝐁❴d2,h2❵∘𝐁❴d1,h1❵ ≡ 𝐁❴h2+d1,h1❵∘𝐁❴d2,h2❵.
  32 #d1 #d2 #Hd21 #h1 #h2
  33 @nstream_inv_eq
  34 @nstream_eq_inv_ext #i
  35 <compose_apply <compose_apply
  36 elim (lt_or_ge i d2) #Hd2
  37 [ lapply (lt_to_le_to_lt … Hd2 Hd21) -Hd21 #Hd1
  38   >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2) >apply_basic_lt
  39   /2 width=1 by le_plus_a/
  40 | elim (lt_or_ge i d1) -Hd21 #Hd1
  41   [ >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2) >apply_basic_lt
  42     /2 width=1 by monotonic_lt_plus_r/
  43   | >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2)
  44     >apply_basic_ge [2: /2 width=1 by le_plus_a/ ]
  45     >apply_basic_ge /2 width=1 by monotonic_le_plus_r/
  46   ]
  47 ]
  48 qed-.