Set Implicit Arguments.
Require Import Metatheory LambdaES_Defs LambdaES_Infrastructure.
Require Import Rewriting_defs LambdaJ_ndr LambdaES_occ LambdaJ_Rules.

Theorem full_composition : forall t u, term (t[u]) -> (t[u]) -->j* (t^^u).
Proof.

  intro t.
  assert (exists n, bv_occ t = n).
    exists* (bv_occ t).
  destruct H as [n].
  gen t.
  induction n using nat_ind_lambda_j ; intros .

    apply one_step_reduction.
    apply redex.
    unfold open.
    rewrite <- open_rec_term with (k:=0) (u:=u); [|term_solver].
    apply* rule_w.
    term_solver.

    apply one_step_reduction.
    apply redex.
    apply* rule_d.
    term_solver.

    assert (term u) as term_u by term_solver.
    pick_fresh a. pick_fresh b.
    assert (body t) as body_t by term_solver.
    assert (bv_occ t = fv_occ a (t^a)) as bv_fv by (autorewrite with bv_occ_rewrite ; auto with arith).
    assert (n1+n2 = fv_occ a (t ^ a)) by omega.
    assert(1 < fv_occ a (t ^ a)) by omega.
    clear bv_fv.
    assert (n1 <= fv_occ a (t ^ a)) by omega.
    destruct (ndr_n_exists (t^a) a b (n1) H5) as [t'].

    apply transitive_closure_composition with (u := ((close ((close t' a)[u]) b) [u])).
      apply one_step_reduction.
      apply redex.
      apply rule_c ; eauto using term_sub_to_body, term_sub_to_term.
        omega.
        unfolds ndr. exists (n1). splits*. omega.

      assert (term t') as term_t' by term_solver.
      apply transitive_closure_composition with (u:= (close (close t' a [u]) b)^^u).
        apply IHn1.
          bv_occ_solver.
          term_solver.

         rewrite <- subst_as_close_open ; auto with term_building_db.
         simpl.
         pattern ([b ~> u]u).
         rewrite subst_fresh ; auto.
         rewrite subst_close ; auto ; [|VSD.fsetdec].

         apply transitive_closure_composition with (u:=close ([b~>u]t') a ^^ u).
           apply IHn2.
             bv_occ_solver.
             term_solver.

           rewrite <- subst_as_close_open; auto with term_building_db.
           replace (t^^u) with ([a ~> u]([b ~> u]t')). apply reflexive_reduction.
           apply ndr_n_close_open with (n:=n1) ; auto.
           VSD.fsetdec.
Qed.