+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/isfinite_1.ma".
-include "ground_2/relocation/rtmap_fcla.ma".
-
-(* RELOCATION MAP ***********************************************************)
-
-definition isfin: predicate rtmap ā
- Ī»f. ān. šāŖfā« ā n.
-
-interpretation "test for finite colength (rtmap)"
- 'IsFinite f = (isfin f).
-
-(* Basic eliminators ********************************************************)
-
-lemma isfin_ind (R:predicate rtmap): (āf. šāŖfā« ā R f) ā
- (āf. š
āŖfā« ā R f ā R (ā«Æf)) ā
- (āf. š
āŖfā« ā R f ā R (āf)) ā
- āf. š
āŖfā« ā R f.
-#R #IH1 #IH2 #IH3 #f #H elim H -H
-#n #H elim H -f -n /3 width=2 by ex_intro/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma isfin_inv_push: āg. š
āŖgā« ā āf. ā«Æf = g ā š
āŖfā«.
-#g * /3 width=4 by fcla_inv_px, ex_intro/
-qed-.
-
-lemma isfin_inv_next: āg. š
āŖgā« ā āf. āf = g ā š
āŖfā«.
-#g * #n #H #f #H0 elim (fcla_inv_nx ā¦ H ā¦ H0) -g
-/2 width=2 by ex_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma isfin_eq_repl_back: eq_repl_back ā¦ isfin.
-#f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
-qed-.
-
-lemma isfin_eq_repl_fwd: eq_repl_fwd ā¦ isfin.
-/3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
-
-lemma isfin_isid: āf. šāŖfā« ā š
āŖfā«.
-/3 width=2 by fcla_isid, ex_intro/ qed.
-
-lemma isfin_push: āf. š
āŖfā« ā š
āŖā«Æfā«.
-#f * /3 width=2 by fcla_push, ex_intro/
-qed.
-
-lemma isfin_next: āf. š
āŖfā« ā š
āŖāfā«.
-#f * /3 width=2 by fcla_next, ex_intro/
-qed.
-
-(* Properties with iterated push ********************************************)
-
-lemma isfin_pushs: ān,f. š
āŖfā« ā š
āŖā«Æ*[n]fā«.
-#n elim n -n /3 width=3 by isfin_push/
-qed.
-
-(* Inversion lemmas with iterated push **************************************)
-
-lemma isfin_inv_pushs: ān,g. š
āŖā«Æ*[n]gā« ā š
āŖgā«.
-#n elim n -n /3 width=3 by isfin_inv_push/
-qed.
-
-(* Properties with tail *****************************************************)
-
-lemma isfin_tl: āf. š
āŖfā« ā š
āŖā«±fā«.
-#f elim (pn_split f) * #g #H #Hf destruct
-/3 width=3 by isfin_inv_push, isfin_inv_next/
-qed.
-
-(* Inversion lemmas with tail ***********************************************)
-
-lemma isfin_inv_tl: āf. š
āŖā«±fā« ā š
āŖfā«.
-#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
-qed-.
-
-(* Inversion lemmas with iterated tail **************************************)
-
-lemma isfin_inv_tls: ān,f. š
āŖā«±*[n]fā« ā š
āŖfā«.
-#n elim n -n /3 width=1 by isfin_inv_tl/
-qed-.