]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_isu.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_isu.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/relations/predicate_u_1.ma".
16 include "ground/relocation/pr_isi.ma".
17
18 (* UNIFORMITY CONDITION FOR PARTIAL RELOCATION MAPS *************************)
19
20 (*** isuni *)
21 inductive pr_isu: predicate pr_map ā‰
22 (*** isuni_isid *)
23 | pr_isu_isi (f): šˆāØfā© ā†’ pr_isu f
24 (*** isuni_next *)
25 | pr_isu_next (f): pr_isu f ā†’ āˆ€g. ā†‘f = g ā†’ pr_isu g
26 .
27
28 interpretation
29   "uniformity condition (partial relocation maps)"
30   'PredicateU f = (pr_isu f).
31
32 (* Basic inversions *********************************************************)
33
34 (*** isuni_inv_push *)
35 lemma pr_isu_inv_push (g): š”āØgā© ā†’ āˆ€f. ā«Æf = g ā†’ šˆāØfā©.
36 #g * -g
37 [ /2 width=3 by pr_isi_inv_push/
38 | #f #_ #g #H #x #Hx destruct
39   elim (eq_inv_pr_push_next ā€¦ Hx)
40 ]
41 qed-.
42
43 (*** isuni_inv_next *)
44 lemma pr_isu_inv_next (g): š”āØgā© ā†’ āˆ€f. ā†‘f = g ā†’ š”āØfā©.
45 #g * -g #f #Hf
46 [ #x #Hx elim (pr_isi_inv_next ā€¦ Hf ā€¦ Hx)
47 | #g #H #x #Hx destruct
48   >(eq_inv_pr_next_bi ā€¦ Hx) -x //
49 ]
50 qed-.
51
52 (* Basic destructions *******************************************************)
53
54 (*** isuni_fwd_push *)
55 lemma pr_isu_fwd_push (g): š”āØgā© ā†’ āˆ€f. ā«Æf = g ā†’ š”āØfā©.
56 /3 width=3 by pr_isu_inv_push, pr_isu_isi/ qed-.