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_omega_1.ma".
16 include "ground/relocation/gr_map.ma".
18 (* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
21 coinductive gr_isd: predicate gr_map ≝
23 | gr_isd_next (f) (g):
24 gr_isd f → ↑f = g → gr_isd g
28 "divergence condition (generic relocation maps)"
29 'PredicateOmega f = (gr_isd f).
31 (* Basic inversion lemmas ***************************************************)
34 lemma gr_isd_inv_gen (g): 𝛀❪g❫ → ∃∃f. 𝛀❪f❫ & ↑f = g.
36 #f #g #Hf * /2 width=3 by ex2_intro/
39 (* Advanced inversion lemmas ************************************************)
41 (*** isdiv_inv_next *)
42 lemma gr_isd_inv_next (g): 𝛀❪g❫ → ∀f. ↑f = g → 𝛀❪f❫.
43 #g #H elim (gr_isd_inv_gen … H) -H
44 #f #Hf * -g #g #H >(eq_inv_gr_next_bi … H) -H //
47 (*** isdiv_inv_push *)
48 lemma gr_isd_inv_push (g): 𝛀❪g❫ → ∀f. ⫯f = g → ⊥.
49 #g #H elim (gr_isd_inv_gen … H) -H
50 #f #Hf * -g #g #H elim (eq_inv_gr_push_next … H)