(*** istot *)
definition pr_ist: predicate pr_map ≝
- λf. â\88\80i. â\88\83j. @â\9dªi,fâ\9d« ≘ j.
+ λf. â\88\80i. â\88\83j. @â\9d¨i,fâ\9d© ≘ j.
interpretation
"totality condition (partial relocation maps)"
(* Basic inversions *********************************************************)
(*** istot_inv_push *)
-lemma pr_ist_inv_push (g): ð\9d\90\93â\9dªgâ\9d« â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\93â\9dªfâ\9d«.
+lemma pr_ist_inv_push (g): ð\9d\90\93â\9d¨gâ\9d© â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\93â\9d¨fâ\9d©.
#g #Hg #f #H #i elim (Hg (↑i)) -Hg
#j #Hg elim (pr_pat_inv_succ_push … Hg … H) -Hg -H /2 width=3 by ex_intro/
qed-.
(*** istot_inv_next *)
-lemma pr_ist_inv_next (g): ð\9d\90\93â\9dªgâ\9d« â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\93â\9dªfâ\9d«.
+lemma pr_ist_inv_next (g): ð\9d\90\93â\9d¨gâ\9d© â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\93â\9d¨fâ\9d©.
#g #Hg #f #H #i elim (Hg i) -Hg
#j #Hg elim (pr_pat_inv_next … Hg … H) -Hg -H /2 width=2 by ex_intro/
qed-.
(* Basic constructions ******************************************************)
-lemma pr_ist_push (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«¯fâ\9d«.
+lemma pr_ist_push (f): ð\9d\90\93â\9d¨fâ\9d© â\86\92 ð\9d\90\93â\9d¨â«¯fâ\9d©.
#f #Hf *
[ /3 width=2 by pr_pat_refl, ex_intro/
| #i elim (Hf i) -Hf /3 width=8 by pr_pat_push, ex_intro/
]
qed.
-lemma pr_ist_next (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ\86\91fâ\9d«.
+lemma pr_ist_next (f): ð\9d\90\93â\9d¨fâ\9d© â\86\92 ð\9d\90\93â\9d¨â\86\91fâ\9d©.
#f #Hf #i elim (Hf i) -Hf
/3 width=6 by pr_pat_next, ex_intro/
qed.
(* Constructions with pr_tl *************************************************)
(*** istot_tl *)
-lemma pr_ist_tl (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«°fâ\9d«.
+lemma pr_ist_tl (f): ð\9d\90\93â\9d¨fâ\9d© â\86\92 ð\9d\90\93â\9d¨â«°fâ\9d©.
#f cases (pr_map_split_tl f) *
/2 width=3 by pr_ist_inv_next, pr_ist_inv_push/
qed.