include "ground/notation/relations/predicate_t_1.ma".
include "ground/relocation/gr_pat.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
(*** istot *)
definition gr_ist: predicate gr_map ā
"totality condition (generic relocation maps)"
'PredicateT f = (gr_ist f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** istot_inv_push *)
lemma gr_ist_inv_push (g): šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
#j #Hg elim (gr_pat_inv_next ā¦ Hg ā¦ H) -Hg -H /2 width=2 by ex_intro/
qed-.
-(* Properties on tl *********************************************************)
+(* Constructions with gr_tl *************************************************)
(*** istot_tl *)
lemma gr_ist_tl (f): šāŖfā« ā šāŖā«±fā«.