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): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«±f❫.
+lemma gr_ist_tl (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«°f❫.
#f cases (gr_map_split_tl f) *
/2 width=3 by gr_ist_inv_next, gr_ist_inv_push/
qed.