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_2/relocation/rtmap_basic.ma".
16 include "ground_2/relocation/nstream_after.ma".
18 (* RELOCATION N-STREAM ******************************************************)
20 (* Specific properties on basic relocation **********************************)
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-.
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-.
28 (* Specific main properties on basic relocation *****************************)
30 theorem basic_swap: ād1,d2. d2 ā¤ d1 ā
31 āh1,h2. šā“d2,h2āµāšā“d1,h1āµ ā” šā“h2+d1,h1āµāšā“d2,h2āµ.
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/