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_f_1.ma".
16 include "ground/relocation/gr_fcla.ma".
18 (* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
21 definition gr_isf: predicate gr_map ≝
25 "finite colength condition (generic relocation maps)"
26 'PredicateF f = (gr_isf f).
28 (* Basic eliminators ********************************************************)
31 lemma gr_isf_ind (Q:predicate …):
33 (∀f. 𝐅❪f❫ → Q f → Q (⫯f)) →
34 (∀f. 𝐅❪f❫ → Q f → Q (↑f)) →
36 #Q #IH1 #IH2 #IH3 #f #H elim H -H
37 #n #H elim H -f -n /3 width=2 by ex_intro/
40 (* Basic inversion lemmas ***************************************************)
42 (*** isfin_inv_push *)
43 lemma gr_isf_inv_push (g): 𝐅❪g❫ → ∀f. ⫯f = g → 𝐅❪f❫.
44 #g * /3 width=4 by gr_fcla_inv_push, ex_intro/
47 (*** isfin_inv_next *)
48 lemma gr_isf_inv_next (g): 𝐅❪g❫ → ∀f. ↑f = g → 𝐅❪f❫.
49 #g * #n #H #f #H0 elim (gr_fcla_inv_next … H … H0) -g
50 /2 width=2 by ex_intro/
53 (* Basic properties *********************************************************)
56 lemma gr_isf_isi (f): 𝐈❪f❫ → 𝐅❪f❫.
57 /3 width=2 by gr_fcla_isi, ex_intro/ qed.
60 lemma gr_isf_push (f): 𝐅❪f❫ → 𝐅❪⫯f❫.
61 #f * /3 width=2 by gr_fcla_push, ex_intro/
65 lemma gr_isf_next (f): 𝐅❪f❫ → 𝐅❪↑f❫.
66 #f * /3 width=2 by gr_fcla_next, ex_intro/