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 inversions *********************************************************)
34 lemma gr_isd_inv_gen (g): šāŖgā« ā āāf. šāŖfā« & āf = g.
36 #f #g #Hf * /2 width=3 by ex2_intro/
39 (* Advanced inversions ******************************************************)
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)