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/notation/relations/predicate_i_1.ma".
16 include "ground/relocation/pr_map.ma".
18 (* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
21 coinductive pr_isi: predicate pr_map ≝
23 | pr_isi_push (f) (g):
24 pr_isi f → ⫯f = g → pr_isi g
28 "identity condition (partial relocation maps)"
29 'PredicateI f = (pr_isi f).
31 (* Basic inversions *********************************************************)
34 lemma pr_isi_inv_gen (g): 𝐈❨g❩ → ∃∃f. 𝐈❨f❩ & ⫯f = g.
36 #f #g #Hf /2 width=3 by ex2_intro/
39 (* Advanced inversions ******************************************************)
42 lemma pr_isi_inv_push (g): 𝐈❨g❩ → ∀f. ⫯f = g → 𝐈❨f❩.
44 elim (pr_isi_inv_gen … H) -H #f #Hf
46 >(eq_inv_pr_push_bi … H) -H //
50 lemma pr_isi_inv_next (g): 𝐈❨g❩ → ∀f. ↑f = g → ⊥.
52 elim (pr_isi_inv_gen … H) -H #f #Hf
53 * -g #g #H elim (eq_inv_pr_next_push … H)