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_2/relocation/rtmap_id.ma".
16 include "basic_2/grammar/cl_restricted_weight.ma".
17 include "basic_2/relocation/frees.ma".
19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
21 (* Advanced properties ******************************************************)
23 lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
24 @(f2_ind … rfw) #n #IH #L *
25 [ cases L -L /3 width=2 by frees_atom, ex_intro/
27 [ #s #Hn destruct elim (IH L (⋆s)) -IH /3 width=2 by frees_sort, ex_intro/
28 | * [2: #i ] #Hn destruct
29 [ elim (IH L (#i)) -IH /3 width=2 by frees_lref, ex_intro/
30 | elim (IH L V) -IH /3 width=2 by frees_zero, ex_intro/
32 | #l #Hn destruct elim (IH L (§l)) -IH /3 width=2 by frees_gref, ex_intro/
34 | * [ #p ] #I #V #T #Hn destruct elim (IH L V) // #f1 #HV
35 [ elim (IH (L.ⓑ{I}V) T) -IH // #f2 #HT
36 elim (sor_isfin_ex f1 (⫱f2))
37 /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
38 | elim (IH L T) -IH // #f2 #HT
39 elim (sor_isfin_ex f1 f2)
40 /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/