]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isf.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sor_isf.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_isf_eq.ma".
16 include "ground/relocation/pr_sor_fcla.ma".
17
18 (* RELATIONAL UNION FOR PARTIAL RELOCATION MAPS *****************************)
19
20 (* Constructions with pr_isf ************************************************)
21
22 (*** sor_isfin_ex *)
23 lemma pr_sor_isf_bi:
24       โˆ€f1,f2. ๐…โจf1โฉ โ†’ ๐…โจf2โฉ โ†’ โˆƒโˆƒf. f1 โ‹“ f2 โ‰˜ f & ๐…โจfโฉ.
25 #f1 #f2 * #n1 #H1 * #n2 #H2 elim (pr_sor_fcla_bi โ€ฆ H1 โ€ฆ H2) -H1 -H2
26 /3 width=4 by ex2_intro, ex_intro/
27 qed-.
28
29 (* Destructions with pr_isf *************************************************)
30
31 (*** sor_fwd_isfin_sn *)
32 lemma pr_sor_des_isf_sn:
33       โˆ€f. ๐…โจfโฉ โ†’ โˆ€f1,f2. f1 โ‹“ f2 โ‰˜ f โ†’ ๐…โจf1โฉ.
34 #f * #n #Hf #f1 #f2 #H
35 elim (pr_sor_des_fcla_sn โ€ฆ Hf โ€ฆ H) -f -f2 /2 width=2 by ex_intro/
36 qed-.
37
38 (*** sor_fwd_isfin_dx *)
39 lemma pr_sor_des_isf_dx:
40       โˆ€f. ๐…โจfโฉ โ†’ โˆ€f1,f2. f1 โ‹“ f2 โ‰˜ f โ†’ ๐…โจf2โฉ.
41 #f * #n #Hf #f1 #f2 #H
42 elim (pr_sor_des_fcla_dx โ€ฆ Hf โ€ฆ H) -f -f1 /2 width=2 by ex_intro/
43 qed-.
44
45 (* Inversions with pr_isf ***************************************************)
46
47 (*** sor_isfin *)
48 lemma pr_sor_inv_isf_bi:
49       โˆ€f1,f2. ๐…โจf1โฉ โ†’ ๐…โจf2โฉ โ†’ โˆ€f. f1 โ‹“ f2 โ‰˜ f โ†’ ๐…โจfโฉ.
50 #f1 #f2 #Hf1 #Hf2 #f #Hf elim (pr_sor_isf_bi โ€ฆ Hf1 โ€ฆ Hf2) -Hf1 -Hf2
51 /3 width=6 by pr_sor_mono, pr_isf_eq_repl_back/
52 qed-.
53
54 (*** sor_inv_isfin3 *)
55 lemma pr_sor_inv_isf:
56       โˆ€f1,f2,f. f1 โ‹“ f2 โ‰˜ f โ†’ ๐…โจfโฉ โ†’
57       โˆงโˆง ๐…โจf1โฉ & ๐…โจf2โฉ.
58 /3 width=4 by pr_sor_des_isf_dx, pr_sor_des_isf_sn, conj/ qed-.