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 "basic_2/relocation/lreq_lreq.ma".
16 include "basic_2/relocation/frees_frees.ma".
17 include "basic_2/relocation/freq.ma".
19 (* RANGED EQUIVALENCE FOR CLOSURES *****************************************)
21 (* Main properties **********************************************************)
23 theorem freq_trans: tri_transitive … freq.
24 #G1 #G #L1 #L #T1 #T * -G -L -T
25 #L #f1 #H1T11 #Hf1 #G2 #L2 #T2 * -G2 -L2 -T2 #L2 #f2 #HT12 #Hf2
26 lapply (frees_lreq_conf … H1T11 … Hf1) #HT11
27 lapply (frees_mono … HT12 … HT11) -HT11 -HT12
28 /4 width=7 by fleq_intro, lreq_eq_repl_back, lreq_trans/
31 theorem freq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2.
32 ⦃G, L, T⦄ ≡ ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄.
33 /3 width=5 by freq_trans, freq_sym/ qed-.
35 theorem freq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T.
36 ⦃G1, L1, T1⦄ ≡ ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄.
37 /3 width=5 by freq_trans, freq_sym/ qed-.