(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "ground/arith/nat_lt_plus.ma".
include "ground/relocation/rtmap_basic_at.ma".
include "ground/relocation/pstream_after.ma".

(* RELOCATION P-STREAM ******************************************************)

(* Properties on basic relocation (specific) **********************************)

lemma apply_basic_lt: ∀m,n,i. ninj i ≤ m → 𝐛❨m,n❩@❨i❩ = i.
/3 width=1 by at_inv_total, gr_pat_basic_lt/ qed-.

lemma apply_basic_ge: ∀m,n,i. m < ninj i → 𝐛❨m,n❩@❨i❩ = i+n.
/3 width=1 by at_inv_total, gr_pat_basic_ge/ qed-.

(* Main properties on basic relocation (specific) *****************************)

theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
                    ∀h1,h2. 𝐛❨d2,h2❩∘𝐛❨d1,h1❩ ≡ 𝐛❨d1+h2,h1❩∘𝐛❨d2,h2❩.
#d1 #d2 #Hd21 #h1 #h2
@nstream_inv_eq
@nstream_eq_inv_ext #i
<compose_apply <compose_apply
elim (nat_split_lt_ge d2 i) #Hd2
[ elim (nat_split_lt_ge d1 i) -Hd21 #Hd1
  [ >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2) >apply_basic_ge
    [ >apply_basic_ge // >nrplus_inj_sn /2 width=1 by nlt_plus_bi_sn/
    | >nrplus_inj_sn /2 width=2 by nlt_plus_dx_dx/
    ]
  | >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2)
    >apply_basic_lt // >nrplus_inj_sn /2 width=1 by nle_plus_bi_dx/
  ]
| lapply (nle_trans … Hd2 … Hd21) -Hd21 #Hd1
  >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2)
  >apply_basic_lt /2 width=1 by nle_plus_dx_dx/
]
qed-.