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/relocation/pr_nat.ma".
16 include "ground/relocation/pr_after_pat.ma".
18 (* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
20 (* Destructions with pr_nat *************************************************)
22 lemma pr_after_nat_des (l) (l1):
23 ∀f. @§❨l1, f❩ ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
24 ∃∃l2. @§❨l1, f1❩ ≘ l2 & @§❨l2, f2❩ ≘ l.
25 #l #l1 #f #H1 #f2 #f1 #Hf
26 elim (pr_after_pat_des … H1 … Hf) -f #i2 #H1 #H2
27 /2 width=3 by ex2_intro/
30 lemma pr_after_des_nat (l) (l2) (l1):
31 ∀f1,f2. @§❨l1, f1❩ ≘ l2 → @§❨l2, f2❩ ≘ l →
32 ∀f. f2 ⊚ f1 ≘ f → @§❨l1, f❩ ≘ l.
33 /2 width=6 by pr_after_des_pat/ qed-.
35 lemma pr_after_des_nat_sn (l1) (l):
36 ∀f. @§❨l1, f❩ ≘ l → ∀f1,l2. @§❨l1, f1❩ ≘ l2 →
37 ∀f2. f2 ⊚ f1 ≘ f → @§❨l2, f2❩ ≘ l.
38 /2 width=6 by pr_after_des_pat_sn/ qed-.
40 lemma pr_after_des_nat_dx (l) (l2) (l1):
41 ∀f,f2. @§❨l1, f❩ ≘ l → @§❨l2, f2❩ ≘ l →
42 ∀f1. f2 ⊚ f1 ≘ f → @§❨l1, f1❩ ≘ l2.
43 /2 width=6 by pr_after_des_pat_dx/ qed-.