+++ /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/notation/relations/rcolength_2.ma".
-include "ground/relocation/rtmap_isid.ma".
-
-(* RELOCATION MAP ***********************************************************)
-
-inductive fcla: relation2 rtmap nat ā
-| fcla_isid: āf. šāŖfā« ā fcla f (š)
-| fcla_push: āf,n. fcla f n ā fcla (ā«Æf) n
-| fcla_next: āf,n. fcla f n ā fcla (āf) (ān)
-.
-
-interpretation "finite colength assignment (rtmap)"
- 'RCoLength f n = (fcla f n).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma fcla_inv_px: āg,m. šāŖgā« ā m ā āf. ā«Æf = g ā šāŖfā« ā m.
-#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
-#g #m #_ #f #H elim (discr_push_next ā¦ H)
-qed-.
-
-lemma fcla_inv_nx: āg,m. šāŖgā« ā m ā āf. āf = g ā
- āān. šāŖfā« ā n & ān = m.
-#g #m * -g -m /2 width=3 by ex2_intro/
-[ #g #Hg #f #H elim (isid_inv_next ā¦ H) -H //
-| #g #m #_ #f #H elim (discr_next_push ā¦ H)
-]
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cla_inv_nn: āg,m. šāŖgā« ā m ā āf,n. āf = g ā ān = m ā šāŖfā« ā n.
-#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
-#x #Hf #H destruct <(eq_inv_nsucc_bi ā¦ H) -n //
-qed-.
-
-lemma cla_inv_np: āg,m. šāŖgā« ā m ā āf. āf = g ā š = m ā ā„.
-#g #m #H #f #H1 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
-#x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
-qed-.
-
-lemma fcla_inv_xp: āg,m. šāŖgā« ā m ā š = m ā šāŖgā«.
-#g #m #H elim H -g -m /3 width=3 by isid_push/
-#g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc ā¦ H)
-qed-.
-
-lemma fcla_inv_isid: āf,n. šāŖfā« ā n ā šāŖfā« ā š = n.
-#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
-#f #n #_ #_ #H elim (isid_inv_next ā¦ H) -H //
-qed-.
-
-(* Main forward lemmas ******************************************************)
-
-theorem fcla_mono: āf,n1. šāŖfā« ā n1 ā ān2. šāŖfā« ā n2 ā n1 = n2.
-#f #n #H elim H -f -n
-[ /2 width=3 by fcla_inv_isid/
-| /3 width=3 by fcla_inv_px/
-| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx ā¦ H) -H [2,3 : // ]
- #g #Hf #H destruct >IH //
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma fcla_eq_repl_back: ān. eq_repl_back ā¦ (Ī»f. šāŖfā« ā n).
-#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
-#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px ā¦ H) | elim (eq_inv_nx ā¦ H) ] -H
-/3 width=3 by fcla_push, fcla_next/
-qed-.
-
-lemma fcla_eq_repl_fwd: ān. eq_repl_fwd ā¦ (Ī»f. šāŖfā« ā n).
-#n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/
-qed-.