]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sdj_isi.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/relocation/pr_isi.ma".
16 include "ground/relocation/pr_sdj.ma".
17
18 (* DISJOINTNESS FOR PARTIAL RELOCATION MAPS *********************************)
19
20 (* Constructions with pr_isi ************************************************)
21
22 (*** sdj_isid_dx *)
23 corec lemma pr_sdj_isi_dx:
24             ∀f2. 𝐈❨f2❩ → ∀f1. f1 ∥ f2.
25 #f2 * -f2
26 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1) *
27 /3 width=5 by pr_sdj_next_push, pr_sdj_push_bi/
28 qed.
29
30 (*** sdj_isid_sn *)
31 corec lemma pr_sdj_isi_sn:
32             ∀f1. 𝐈❨f1❩ → ∀f2. f1 ∥ f2.
33 #f1 * -f1
34 #f1 #g1 #Hf1 #H1 #f2 cases (pr_map_split_tl f2) *
35 /3 width=5 by pr_sdj_push_next, pr_sdj_push_bi/
36 qed.
37
38 (* Inversions with pr_isi ***************************************************)
39
40 (*** sdj_inv_refl *)
41 corec lemma pr_sdj_inv_refl:
42             ∀f. f ∥ f →  𝐈❨f❩.
43 #f cases (pr_map_split_tl f) #Hf #H
44 [ lapply (pr_sdj_inv_push_bi … H … Hf Hf) -H /3 width=3 by pr_isi_push/
45 | elim (pr_sdj_inv_next_bi … H … Hf Hf)
46 ]
47 qed-.