(**************************************************************************)
(*       ___                                                              *)
(*      ||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/ynat/ynat_max.ma".
include "basic_2/substitution/drop_drop.ma".
include "basic_2/multiple/frees.ma".

(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)

(* Advanced properties ******************************************************)

lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
#L #U @(f2_ind … rfw … L U) -L -U
#x #IH #L * *
[ -IH /3 width=5 by frees_inv_sort, or_intror/
| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
  [ -x @or_intror #H elim (ylt_yle_false … Hji)
    lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
  | -x /2 width=1 by or_introl/
  | elim (ylt_split j l) #Hli
    [ -x @or_intror #H elim (ylt_yle_false … Hji)
      lapply (frees_inv_lref_skip … H ?) -L //
    | elim (lt_or_ge j (|L|)) #Hj
      [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
        elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
        @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
        lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/  
      | -x @or_intror #H elim (ylt_yle_false … Hji)
        lapply (frees_inv_lref_free … H ?) -l //
      ]
    ]
  ]
| -IH /3 width=5 by frees_inv_gref, or_intror/
| #a #I #W #U #Hx #l #i destruct
  elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
  elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
  @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
| #I #W #U #Hx #l #i destruct
  elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
  elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
  @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
]
qed-.

lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
               (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
lapply (yle_inv_inj … Hlj) -Hlj #Hlj
elim (le_to_or_lt_eq … Hlj) -Hlj
[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
| -Hji -HnU #H destruct
  lapply (drop_mono … HLK0 … HLK) #H destruct -I
  elim HnW0 -L -U -HnW0 //
]
qed.

(* Note: lemma 1250 *)
lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
                       L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
qed.