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 (* Notes: this replaces lemma 1400 concluding the "big tree" theorem *)
24 lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
25 @(f2_ind … rfw) #n #IH #L *
26 [ cases L -L /3 width=2 by frees_atom, ex_intro/
28 [ #s #Hn destruct elim (IH L (⋆s)) -IH /3 width=2 by frees_sort, ex_intro/
29 | * [2: #i ] #Hn destruct
30 [ elim (IH L (#i)) -IH /3 width=2 by frees_lref, ex_intro/
31 | elim (IH L V) -IH /3 width=2 by frees_zero, ex_intro/
33 | #l #Hn destruct elim (IH L (§l)) -IH /3 width=2 by frees_gref, ex_intro/
35 | * [ #p ] #I #V #T #Hn destruct elim (IH L V) // #f1 #HV
36 [ elim (IH (L.ⓑ{I}V) T) -IH // #f2 #HT
37 elim (sor_isfin_ex f1 (⫱f2))
38 /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
39 | elim (IH L T) -IH // #f2 #HT
40 elim (sor_isfin_ex f1 f2)
41 /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/