include "ground/notation/relations/predicate_omega_1.ma".
include "ground/relocation/gr_map.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
(*** isdiv *)
coinductive gr_isd: predicate gr_map ā
"divergence condition (generic relocation maps)"
'PredicateOmega f = (gr_isd f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isdiv_inv_gen *)
lemma gr_isd_inv_gen (g): šāŖgā« ā āāf. šāŖfā« & āf = g.
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** isdiv_inv_next *)
lemma gr_isd_inv_next (g): šāŖgā« ā āf. āf = g ā šāŖfā«.