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_isf.ma".
16 include "ground/relocation/pr_coafter_isi.ma".
17 include "ground/relocation/pr_coafter_ist_isi.ma".
18 include "ground/relocation/pr_sor_isi.ma".
20 (* RELATIONAL UNION FOR PARTIAL RELOCATION MAPS *****************************)
22 (* Constructions with pr_coafter and pr_ist and pr_isf **********************)
25 lemma pr_sor_coafter_dx_tans:
26 ∀f. 𝐅❨f❩ → ∀f2. 𝐓❨f2❩ → ∀f1. f2 ~⊚ f1 ≘ f → ∀f1a,f1b. f1a ⋓ f1b ≘ f1 →
27 ∃∃fa,fb. f2 ~⊚ f1a ≘ fa & f2 ~⊚ f1b ≘ fb & fa ⋓ fb ≘ f.
29 [ #f #Hf #f2 #Hf2 #f1 #Hf #f1a #f1b #Hf1
30 lapply (pr_coafter_des_ist_sn_isi … Hf ??) -Hf // #H2f1
31 elim (pr_sor_inv_isi … Hf1) -Hf1 //
32 /3 width=5 by pr_coafter_isi_dx, pr_sor_idem, ex3_2_intro/
33 | #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
34 elim (pr_coafter_inv_push … H1) -H1 [1,3: * |*: // ]
35 [ #g2 #g1 #Hf #Hgf2 #Hgf1
36 elim (pr_sor_inv_push … H2) -H2 [ |*: // ] #ga #gb #Hg1
37 lapply (pr_ist_inv_push … Hf2 … Hgf2) -Hf2 #Hg2
38 elim (IH … Hf … Hg1) // -f1 -g1 -IH -Hg2
39 /3 width=11 by pr_coafter_refl, pr_sor_push_bi, ex3_2_intro/
41 lapply (pr_ist_inv_next … Hf2 … Hgf2) -Hf2 #Hg2
42 elim (IH … Hf … H2) // -f1 -IH -Hg2
43 /3 width=11 by pr_coafter_next, pr_sor_push_bi, ex3_2_intro/
45 | #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
46 elim (pr_coafter_inv_next … H1) -H1 [ |*: // ] #g2 #g1 #Hf #Hgf2 #Hgf1
47 lapply (pr_ist_inv_push … Hf2 … Hgf2) -Hf2 #Hg2
48 elim (pr_sor_inv_next … H2) -H2 [1,3,4: * |*: // ] #ga #gb #Hg1
49 elim (IH … Hf … Hg1) // -f1 -g1 -IH -Hg2
50 /3 width=11 by pr_coafter_refl, pr_coafter_push, pr_sor_next_push, pr_sor_push_next, pr_sor_next_bi, ex3_2_intro/
54 (*** coafter_inv_sor *)
55 lemma pr_sor_coafter_div:
56 ∀f. 𝐅❨f❩ → ∀f2. 𝐓❨f2❩ → ∀f1. f2 ~⊚ f1 ≘ f → ∀fa,fb. fa ⋓ fb ≘ f →
57 ∃∃f1a,f1b. f2 ~⊚ f1a ≘ fa & f2 ~⊚ f1b ≘ fb & f1a ⋓ f1b ≘ f1.
59 [ #f #Hf #f2 #Hf2 #f1 #H1f #fa #fb #H2f
60 elim (pr_sor_inv_isi … H2f) -H2f //
61 lapply (pr_coafter_des_ist_sn_isi … H1f ??) -H1f //
62 /3 width=5 by ex3_2_intro, pr_coafter_isi_dx, pr_sor_isi_bi_isi/
63 | #f #_ #IH #f2 #Hf2 #f1 #H1 #fa #fb #H2
64 elim (pr_sor_inv_push … H2) -H2 [ |*: // ] #ga #gb #H2f
65 elim (pr_coafter_inv_push … H1) -H1 [1,3: * |*: // ] #g2 [ #g1 ] #H1f #Hgf2
66 [ lapply (pr_ist_inv_push … Hf2 … Hgf2) | lapply (pr_ist_inv_next … Hf2 … Hgf2) ] -Hf2 #Hg2
67 elim (IH … Hg2 … H1f … H2f) -f -Hg2
68 /3 width=11 by pr_sor_push_bi, ex3_2_intro, pr_coafter_refl, pr_coafter_next/
69 | #f #_ #IH #f2 #Hf2 #f1 #H1 #fa #fb #H2
70 elim (pr_coafter_inv_next … H1) -H1 [ |*: // ] #g2 #g1 #H1f #Hgf2
71 lapply (pr_ist_inv_push … Hf2 … Hgf2) -Hf2 #Hg2
72 elim (pr_sor_inv_next … H2) -H2 [1,3,4: * |*: // ] #ga #gb #H2f
73 elim (IH … Hg2 … H1f … H2f) -f -Hg2
74 /3 width=11 by pr_sor_next_push, pr_sor_push_next, pr_sor_next_bi, ex3_2_intro, pr_coafter_refl, pr_coafter_push/