]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / fr2_append.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/notation/functions/black_circle_2.ma".
16 include "ground/relocation/fr2_map.ma".
17
18 (* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************)
19
20 (* Note: this is reverse compose *)
21 (*** fr2_append *)
22 rec definition fr2_append f1 f2 on f1 ≝ match f1 with
23 [ fr2_empty        ⇒ f2
24 | fr2_lcons d h f1 ⇒ ❨d, h❩◗ fr2_append f1 f2
25 ].
26
27 interpretation
28   "append (finite relocation maps with pairs)" 
29   'BlackCircle f1 f2 = (fr2_append f1 f2).
30
31 (* Basic constructions ******************************************************)
32
33 (*** mr2_append_nil *)
34 lemma fr2_append_empty (f2):
35       f2 = 𝐞 ● f2.
36 // qed.
37
38 (*** mr2_append_cons *)
39 lemma fr2_append_lcons (d) (h) (f1) (f2):
40       ❨d, h❩◗ (f1 ● f2) = (❨d, h❩◗ f1) ● f2.
41 // qed.