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/pr_map.ma".
18 (* DIVERGENCE CONDITION FOR PARTIAL RELOCATION MAPS *************************)
21 coinductive pr_isd: predicate pr_map ā
23 | pr_isd_next (f) (g):
24 pr_isd f ā āf = g ā pr_isd g
28 "divergence condition (partial relocation maps)"
29 'PredicateOmega f = (pr_isd f).
31 (* Basic inversions *********************************************************)
34 lemma pr_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 pr_isd_inv_next (g): šāØgā© ā āf. āf = g ā šāØfā©.
43 #g #H elim (pr_isd_inv_gen ā¦ H) -H
44 #f #Hf * -g #g #H >(eq_inv_pr_next_bi ā¦ H) -H //
47 (*** isdiv_inv_push *)
48 lemma pr_isd_inv_push (g): šāØgā© ā āf. ā«Æf = g ā ā„.
49 #g #H elim (pr_isd_inv_gen ā¦ H) -H
50 #f #Hf * -g #g #H elim (eq_inv_pr_push_next ā¦ H)