Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base CFP Linearity TailRecursion Congruence.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fact tailrec_subst_trace_compose1 n s xi1 sigma f
  : TC s xi1
    → (∀ i, i ≥ n → sigma i = (ids (f i)))
    → boundT n xi1
    → TC s.[sigma] (ren_trace f xi1).
Proof.
  intros. general induction H; eauto using TC.
  - simpl. inv H1.
    rewrite H0; try omega.
    constructor.
  - simpl. inv H1.
    rewrite H0; try omega.
    constructor.
  - asimpl. rewrite ren_concat_distribute.
    decide (partial xi1).
    + rewrite concat_partial_absorb_right; eauto using ren_partial_preserve.
      rewrite <- concat_partial_absorb_right with (xi2 := P); eauto using ren_partial_preserve.
      constructor; eauto using TC.
      apply IHTC1 with (n:= n); eauto. apply boundT_concat_decompose_left with (xi2:= xi2). eauto.
    + constructor; eauto.
      × apply IHTC1 with (n:= n); eauto.
        apply boundT_concat_decompose_left with (xi2:= xi2). eauto.
      × apply IHTC2 with (n:= n); eauto.
        apply not_partial_total in n0.
        apply boundT_concat_decompose_right with (xi1:= xi1); eauto.
  - asimpl. constructor. rewrite up_change.
    rewrite <- subst_Fix_distribute.
    apply IHTC with (n:= n); eauto.
Qed.

Fact tailrec_subst_trace_compose2 s xi1 f sigma x n xi2
  : TC s xi1
    → (∀ i, i ≥ n → sigma i = (ids (f i)))
    → x < n
    → terminal x xi1
    → boundT n (butLast xi1)
    → TC (sigma x) xi2
    → TC s.[sigma] (concat (butLast (ren_trace f xi1)) xi2).
Proof.
  intros. general induction H; eauto using TC.
  - inv H2.
  - simpl. inv H2; eauto.
    inv H8.
  - destruct (terminal_concat_decompose H3) as [[A B] | [A B] ].
    + destruct A as [A1 | [A2 | A3]].
      × rewrite concat_partial_absorb_right in H3; eauto.
        setoid_rewrite concat_partial_absorb_right at 2; eauto.
        assert (partial (butLast (ren_trace f xi1))).
        { rewrite ren_butLast_distribute. apply ren_partial_preserve.
          apply butLast_partial_preserve. eauto. }
        rewrite concat_partial_absorb_right; eauto.
        asimpl. rewrite <- concat_partial_absorb_right with (xi2:= P); eauto.
        constructor; eauto using TC.
        rewrite <- concat_partial_absorb_right with (xi2:= P); eauto.
        apply IHTC1 with (x:= x) (n:= n); eauto using TC.
        rewrite concat_partial_absorb_right in H4; eauto.
      × asimpl. rewrite A2 in H3. rewrite <- concat_T_iden_right in H3.
        rewrite A2. rewrite <- concat_T_iden_right.
        setoid_rewrite concat_T_iden_right at 1.
        constructor; eauto.
        { apply IHTC1 with (x:= x) (n:= n); eauto.
          rewrite A2 in H4. rewrite <- concat_T_iden_right in H4.
          eauto. }
        {rewrite A2 in H0. apply subst_trace_construct with (xi:= T); eauto using substT. }
      × asimpl. rewrite <- concat_partial_absorb_right with (xi2:= P).
        { constructor; eauto using TC.
          rewrite A3. rewrite ren_butLast_distribute.
          rewrite butLast_P_distribute. rewrite ren_concat_distribute.
          rewrite <- ren_butLast_distribute.
          rewrite concat_partial_absorb_right.
          - apply IHTC1 with (x:= x) (n:= n); eauto.
            + rewrite A3 in H4. rewrite butLast_P_distribute in H4.
              apply boundT_concat_decompose_left in H4. eauto.
            + simpl. eauto using TC.
          - simpl. apply concat_P_partial_right. }
        { rewrite concat_partial_absorb_right.
          - apply butLast_partial_preserve.
            apply ren_partial_preserve. rewrite A3.
            apply concat_P_partial_right.
          - apply butLast_partial_preserve.
            apply ren_partial_preserve. rewrite A3.
            apply concat_P_partial_right. }
    + simpl. rewrite ren_concat_distribute.
      rewrite butLast_concat_distribute.
      { rewrite concat_assoc. constructor.
        - apply tailrec_subst_trace_compose1 with (n:= n); eauto.
          rewrite butLast_concat_distribute in H4; eauto.
          + apply boundT_concat_decompose_left in H4. eauto.
          + apply terminal_composed with (x:= x). eauto.
        - apply IHTC2 with (x:= x) (n:= n); eauto.
          rewrite butLast_concat_distribute in H4; eauto.
          + apply boundT_concat_decompose_right in H4; eauto.
          + apply terminal_composed with (x:= x). eauto. }
      { apply ren_composed_preserve. apply terminal_composed with (x:= x). eauto. }
      { apply ren_total_preserve. eauto. }
  - asimpl. constructor. rewrite up_change. asimpl in IHTC.
    assert (s.[CFPFix s.[up sigma] .: sigma] = s.[CFPFix s/].[sigma]).
    { asimpl. eauto. }
    rewrite H5. apply IHTC with (x:= x) (n:= n); eauto.
Qed.

Fact tailrec_subst_trace_decompose n s sigma f xi
  : tailrec n s
    → TCsubst s sigma xi
    → (∀ i, i ≥ n → sigma i = (ids (f i)))
    → (∃ xi', TC s xi' ∧ xi = ren_trace f xi' ∧ boundT n xi')
       ∨ (∃ xi1 xi2 x,
              TC s xi1
              ∧ TC (sigma x) xi2
              ∧ terminal x xi1
              ∧ x < n
              ∧ xi = concat (butLast (ren_trace f xi1)) xi2
              ∧ boundT n (butLast xi1)).
Proof.
  intros. general induction H0.
  - left. ∃ P. split; eauto using TC, boundT.
  - left. ∃ T. split; eauto using TC, boundT.
  - decide (x < n).
    + right. ∃ (V x T), xi, x.
      split; eauto using TC. split; eauto. split; eauto using terminal.
      split; eauto. split; eauto. constructor.
    + left. rewrite H1 in H; try omega.
      inv H.
      × ∃ P. split; eauto using TC. split; eauto using boundT.
      × ∃ (V x P). split; eauto using TC. split; eauto using boundT.
        constructor; eauto using boundT. omega.
      × ∃ (V x T). split; eauto using TC. split; eauto using boundT.
        constructor; eauto using boundT. omega.
  - inv H.
    destruct (IHTCsubst1 n f H5 H1) as [[xiC1 [A1 [B1 C1]]] | [xiA1 [xiB1 [x [C1 [D1 [E1 [F1 [G1 I1]]]]]]]]].
    + destruct (IHTCsubst2 n f H6 H1) as [[xiC2 [A2 [B2 C2]]] | [xiA2 [xiB2 [x2 [C2 [D2 [E2 [F2 [G2 I2]]]]]]]]].
      { left. ∃ (concat xiC1 xiC2). split; eauto using TC.
        split; eauto.
        - rewrite B1. rewrite B2.
          rewrite ren_concat_distribute. eauto.
        - apply boundT_concat_compose; eauto. }
      { decide (partial xiC1).
        - left. ∃ xiC1. split.
          + rewrite <- concat_partial_absorb_right with (xi2:= P); eauto.
            constructor; eauto using TC.
          + rewrite concat_partial_absorb_right; eauto.
            rewrite B1. apply ren_partial_preserve. eauto.
        - apply not_partial_total in n0.
          right.
          ∃ (concat xiC1 xiA2), xiB2, x2.
          split; eauto using TC. split; eauto.
          split; eauto using terminal.
          + apply terminal_concat_compose with (n:= n); eauto.
          + split; eauto.
            split.
            × rewrite G2. rewrite ren_concat_distribute.
              rewrite butLast_concat_distribute; eauto.
              { rewrite concat_assoc. rewrite <- B1. eauto. }
              { apply ren_composed_preserve. apply terminal_composed with (x:= x2). eauto. }
              { apply ren_total_preserve. eauto. }
            × rewrite butLast_concat_distribute; eauto using terminal_composed.
              apply boundT_concat_compose; eauto. }
    + apply bound_boundT with (xi:= xiA1) in H3; eauto.
      exfalso. eapply terminal_boundT_contradict with (n:= n) (x:= x) (xi:= xiA1); eauto.
  - inv H.
    destruct (IHTCsubst n f H5 H1) as [[xiC [A [B I]]] | [xiA [xiB [x [C [D [E [F [G I]]]]]]]]].
    + left. ∃ xiC. split; eauto using TC.
    + right. ∃ xiA, xiB, x. split; eauto using TC.
  - inv H.
    destruct (IHTCsubst n f H6 H1) as [[xiC [A [B I]]] | [xiA [xiB [x [C [D [E [F [G I]]]]]]]]].
    + left. ∃ xiC. split; eauto using TC.
    + right. ∃ xiA, xiB, x. split; eauto using TC.
  - destruct (IHTCsubst n f) as [[xiC [A [B I]]] | [xiA [xiB [x [C [D [E [F [G I]]]]]]]]]; eauto.
    + inv H. rewrite substPos_zero_extens.
      apply tailrec_subst_preserve; eauto. omega.
    + left. ∃ xiC. split; eauto using TC.
    + right. ∃ xiA, xiB, x. split; eauto using TC.
Qed.

Fixpoint linearize (n:nat) (s u: cfp) :=
  match s with
  | CFPEps ⇒ u
  | (CFPVar x) ⇒ if (decision (x < n)) then (CFPVar x) else (CFPSeq (CFPVar x) u)
  | (CFPSeq s t) ⇒ linearize n s (linearize n t u)
  | (CFPChoice s t) ⇒ CFPChoice (linearize n s u) (linearize n t u)
  | (CFPFix s) ⇒ CFPFix (linearize (S n) s u.[ren(+1)])
  end.

Lemma linearize_tailrec n s u
  : tailrec n s
    → tailrec n u
    → tailrec n (linearize n s u).
Proof.
  intros. general induction H; eauto using tailrec.
  - simpl. decide (m < n); eauto using tailrec.
    constructor; eauto using tailrec.
    constructor 3. omega.
  - simpl. constructor. apply IHtailrec. apply tailrec_ren_preserve with (n:= n); eauto; intros; simpl; omega.
Qed.

Lemma linearize_lin n s u
  : tailrec n s
    → lin n u
    → lin n (linearize n s u).
Proof.
  intros. general induction H; eauto using lin.
  - simpl. decide (m < n); eauto using lin.
    constructor; eauto. omega.
  - simpl. constructor. apply IHtailrec.
    apply lin_ren_preserve with (n:= n); eauto.
    intros. simpl. omega.
Qed.

Lemma linearize_correct1 n x s u xi xi1 xi2
  : tailrec n s
    → (TC s xi → x < n → terminal x xi → TC (linearize n s u) xi)
       ∧ (TC s xi → boundT n xi → partial xi → TC (linearize n s u) xi)
       ∧ (TC s xi1 → total xi1 → boundT n xi1 → TC u xi2 → TC (linearize n s u) (concat xi1 xi2)).
Proof.
  intros. general induction H; intros.
  - repeat split; simpl; intros.
    + inv H; inv H1.
    + inv H; eauto using TC. inv H1.
    + inv H.
      × rewrite concat_partial_absorb_right; eauto using TC, partial.
      × rewrite <- concat_T_iden_left. eauto.
  - repeat split; simpl; intros.
    + decide (m < n); eauto.
      assert (x ≠ m); try omega.
      inv H; eauto using TC; inv H1; try omega; inv H7.
    + decide (m < n); eauto. apply trace_partial_Seq_left; eauto.
    + decide (m < n); eauto. inv H; inv H0; inv H4.
      × inv H1. exfalso. omega.
      × constructor; eauto.
  - destruct (IHtailrec1 x u xi xi1 xi2) as [IH1s [IH2s IH3s]].
    destruct (IHtailrec2 x u xi xi1 xi2) as [IH1t [IH2t IH3t]].
    repeat split; simpl; intros; inv H1; eauto using TC.
  - repeat split; simpl; intros.
    + inv H2; eauto using TC.
      apply bound_boundT with (xi:= xi0) in H; eauto.
      destruct (terminal_concat_decompose H4) as [[[H5 | [H5 | H5]] H10] | [H6 H8]];
        [exfalso; apply terminal_boundT_contradict with (n:= n) (xi:= xi0) (x:= x); eauto..|].
      destruct (IHtailrec2 x u xi3 xi1 xi2) as [IH1t [IH2t IH3t]].
      specialize (IH1t H9 H3 H8).
      destruct (IHtailrec1 x (linearize n t u) xi1 xi0 xi3) as [IH1s [IH2s IH3s]].
      eauto.
    + inv H2; eauto using TC.
      decide (partial xi0).
      × rewrite concat_partial_absorb_right; eauto.
        rewrite concat_partial_absorb_right in H3; eauto.
        destruct (IHtailrec1 x (linearize n t u) xi0 xi0 xi3) as [IH1s [IH2s IH3s]].
        eauto.
      × apply not_partial_total in n0.
        assert (boundT n xi0); eauto using boundT_concat_decompose_left.
        apply boundT_concat_decompose_right in H3; eauto. destruct (IHtailrec1 x (linearize n t u) xi0 xi0 xi3) as [IH1s [IH2s IH3s]]. apply IH3s; eauto.
        destruct (IHtailrec2 x u xi3 xi1 xi2) as [IH1t [IH2t IH3t]].
        apply IH2t; eauto. apply concat_partial_compose with (xi1:= xi0); eauto.
    + inv H2; eauto using TC. rewrite concat_assoc.
      destruct (concat_total_decompose H3) as [A B].
      assert (boundT n xi0); eauto using boundT_concat_decompose_left.
      apply boundT_concat_decompose_right in H4; eauto.
      destruct (IHtailrec1 x (linearize n t u) xi xi0 (concat xi3 xi2)) as [IH1t [IH2t IH3t]]. apply IH3t; eauto.
      destruct (IHtailrec2 x u xi xi3 xi2) as [IH1s [IH2s IH3s]]. eauto.
  - repeat split; simpl; intros.
    + apply Fix_unfold_subsume in H0. destruct H0 as [m H0]. general induction m; simpl in H0.
      × apply Null_trace in H0. rewrite H0. eauto using TC.
      × apply TC_TCsubst in H0.
        destruct (@tailrec_subst_trace_decompose 1 s (unfold s m .: ids) shift xi) as [[xiA [A1 [A2 A3]]] | [xiA [xiB [y [B2 [B3 [B4 [B5 [B6 B7]]]]]]]]]; eauto using simulate_shift.
        { apply tailrec_step with (n:= S n); eauto. omega. }
        { destruct (IHtailrec (S x) u.[ren(+1)] xiA xi1 xi2) as [IH1 [IH2 IH3]].
          assert (TC (linearize (S n) s u.[ren(+1)]) xiA).
          { apply IH1; eauto; try omega. rewrite A2 in H2.
            apply terminal_ren_shift_reconstruct; eauto. }
          constructor. rewrite A2. apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift. }
        { destruct (IHtailrec 0 u.[ren(+1)] xiA xi1 xi2) as [IH1 [IH2 IH3]].
          assert (y =0). { destruct y; eauto. inv B5. inv H4. }
                         rewrite H3 in B4.
          assert (TC (linearize (S n) s u.[ren(+1)]) xiA).
          { rewrite B6 in H2.
            apply IH1; eauto; try omega. }
          constructor. rewrite B6.
          assert (TC (CFPFix (linearize (S n) s u.[ren (+1)])) xiB).
          { rewrite H3 in B3. asimpl in B3.
            apply IHm with (x:= x); eauto.
            rewrite B6 in H2. apply terminal_concat_decompose_right with (n:= n) in H2; eauto.
            rewrite ren_butLast_distribute. apply boundT_ren_shift_preserve.
            apply tailrec_trace_butLast_boundT.
            apply tailrec_tailrec_trace with (s:= s); eauto. }
          apply tailrec_subst_trace_compose2 with (x:= 0) (n:= S n); eauto using simulate_shift; try omega.
          apply tailrec_trace_butLast_boundT. apply tailrec_tailrec_trace with (s:= s); eauto. }
    + apply Fix_unfold_subsume in H0. destruct H0 as [m H0]. general induction m; simpl in H0.
      × apply Null_trace in H0. rewrite H0. eauto using TC.
      × apply TC_TCsubst in H0.
        destruct (@tailrec_subst_trace_decompose 1 s (unfold s m .: ids) shift xi) as [[xiA [A1 [A2 A3]]] | [xiA [xiB [y [B2 [B3 [B4 [B5 [B6 B7]]]]]]]]]; eauto using simulate_shift.
        { apply tailrec_step with (n:= S n); eauto. omega. }
        { constructor. destruct (IHtailrec (S x) u.[ren(+1)] xiA xi1 xi2)
            as [IH1 [IH2 IH3]].
          rewrite A2. apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
          apply IH2; eauto.
          - rewrite A2 in H1. apply boundT_ren_shift_reconstruct; eauto.
          - rewrite A2 in H2. apply ren_partial_origin with (f:= shift). eauto. }
        { decide (partial xiA).
          - rewrite concat_partial_absorb_right in B6; eauto using butLast_partial_preserve, ren_partial_preserve.
            rewrite ren_butLast_distribute in B6. rewrite B6.
            destruct (IHtailrec (y) u.[ren(+1)] xiA xi1 xi2)
              as [IH1 [IH2 IH3]].
            constructor.
            apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
            apply trace_partial_prefix2; eauto.
            apply IH1; eauto. omega.
          - apply not_partial_total in n0.
            assert (y= 0).
            { destruct y; eauto. inv B5. inv H4. }
            rewrite H3 in B3. asimpl in B3.
            assert (TC (CFPFix (linearize (S n) s u.[ren (+1)])) xiB).
            { apply IHm; eauto.
              - rewrite B6 in H1. apply boundT_concat_decompose_right with (xi1:= butLast (ren_trace shift xiA)); eauto using butLast_total_preserve, ren_total_preserve.
              - rewrite B6 in H2.
                apply concat_partial_compose with (xi1:= butLast (ren_trace shift xiA)); eauto using butLast_total_preserve, ren_total_preserve. }
            destruct (IHtailrec (0) u.[ren(+1)] xiA xi1 xi2)
              as [IH1 [IH2 IH3]].
            assert (TC (linearize (S n) s u.[ren (+1)]) xiA).
            { apply IH1; eauto; try omega. rewrite H3 in B4. eauto. }
            rewrite B6. constructor. apply tailrec_subst_trace_compose2 with (x:= 0) (n:= 1); eauto using simulate_shift. rewrite H3 in B4. eauto. }
    + apply Fix_unfold_subsume in H0. destruct H0 as [m H0]. general induction m; simpl in H0.
      × apply Null_trace in H0. rewrite H0. eauto using TC.
      × apply TC_TCsubst in H0.
        destruct (@tailrec_subst_trace_decompose 1 s (unfold s m .: ids) shift xi1) as [[xiA [A1 [A2 A3]]] | [xiA [xiB [y [B2 [B3 [B4 [B5 [B6 B7]]]]]]]]]; eauto using simulate_shift.
        { apply tailrec_step with (n:= S n); eauto. omega. }
        { destruct (IHtailrec (0) u.[ren(+1)] xiA xiA (ren_trace (+1) xi2)) as [IH1 [IH2 IH3]].
          constructor. rewrite A2. setoid_rewrite ren_trace_id_inc_shift at 4.
          rewrite <- ren_concat_distribute.
          apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
          - apply IH3; eauto.
            + rewrite A2 in H1. apply ren_total_origin with (f:= shift); eauto.
            + rewrite A2 in H2. apply boundT_ren_shift_reconstruct; eauto.
            + apply ren_trace_ren. eauto.
          - apply boundT_concat_compose; eauto. apply boundT_ren_lift. }
        { assert (y = 0).
          { destruct y; eauto. inv B5. inv H5. }
          subst. asimpl in B3.
          assert (TC (CFPFix (linearize (S n) s u.[ren (+1)])) (concat xiB xi2)).
          { apply concat_total_decompose in H1. destruct H1. apply IHm; eauto using boundT_concat_decompose_right. }
          destruct (IHtailrec (0) u.[ren(+1)] xiA xiA (ren_trace (+1) xi2)) as [IH1 [IH2 IH3]].
          assert (TC (linearize (S n) s u.[ren (+1)]) xiA).
          { apply IH1; eauto. omega. }
          rewrite concat_assoc. constructor.
          apply tailrec_subst_trace_compose2 with (x:= 0) (n:= 1); eauto using simulate_shift. }
Qed.

Lemma linearize_correct2 n s u xi
  : TC (linearize n s u) xi
    → tailrec n s
    → tailrec n u
    → (TC s xi ∧ partial xi ∧ boundT n xi)
       ∨ (TC s xi ∧ ∃ x, x < n ∧ terminal x xi)
       ∨ (∃ xi1 xi2, xi = concat xi1 xi2 ∧ TC s xi1 ∧ total xi1 ∧ boundT n xi1 ∧ TC u xi2).
Proof.
  intros. general induction H0; simpl in H.
  - right. right. ∃ T, xi. repeat split; eauto using TC, total, boundT.
  - decide (m < n).
    + inv H.
      × left. repeat split; eauto using TC, partial, boundT.
      × right. left. split; eauto. ∃ m. split; eauto using terminal.
      × right. left. split; eauto. ∃ m. split; eauto using terminal.
    + assert (n ≤ m); try omega. inv H.
      × left. repeat split; eauto using TC, partial, boundT.
      × decide (partial xi1).
        { left. rewrite concat_partial_absorb_right; eauto. split; repeat split; eauto.
          inv H4; eauto using boundT. }
        { right. right. ∃ xi1, xi2. repeat split; eauto using not_partial_total.
          inv H4; eauto using boundT. }
  - inv H.
    + left. repeat split; eauto using TC, partial, boundT.
    + destruct (IHtailrec1 u xi H4 H1) as [[A1 [A2 A3]] | [[B1 [x [B2 B3]] ] | [xiA [xiB [C1a [C2a [C3a [C4a C5a]]]]]]]]; eauto.
      × left. split; eauto using TC.
      × right. left. split; eauto using TC.
      × right. right. ∃ xiA, xiB. split; eauto using TC.
    + destruct (IHtailrec2 u xi H4 H1) as [[A1 [A2 A3]] | [[B1 [x [B2 B3]] ] | [xiA [xiB [C1a [C2a [C3a [C4a C5a]]]]]]]]; eauto.
      × left. split; eauto using TC.
      × right. left. split; eauto using TC.
      × right. right. ∃ xiA, xiB. split; eauto using TC.
  - simpl in H0. destruct (IHtailrec1 (linearize n t u) xi H0) as [ [A1 [A2 A3]] | [[B1 [x [B2 B3]] ] | [xi1 [xi2 [C1 [C2 [C3 [C4 C5]]]]]]]].
    + apply linearize_tailrec; eauto.
    + left. split; eauto using trace_partial_Seq_left.
    + assert (boundT n xi).
      { apply bound_boundT with (s:= s); eauto. }
      exfalso. apply terminal_boundT_contradict with (n:= n) (xi:= xi) (x:= x); eauto.
    + destruct (IHtailrec2 u xi2 C5 H1) as [ [A1 [A2 A3]] | [[B1 [x [B2 B3]] ] | [xiA [xiB [C1a [C2a [C3a [C4a C5a]]]]]]]]; eauto.
       × left. rewrite C1. repeat split; eauto using TC, concat_partial_preserve_right, boundT_concat_compose.
       × right. left. rewrite C1. split; eauto using TC.
         ∃ x. split; eauto. apply terminal_concat_compose with (n:= n); eauto.
       × right. right. ∃ (concat xi1 xiA), xiB.
         rewrite C1. rewrite C1a. repeat split; eauto using concat_assoc, TC, concat_total_compose, boundT_concat_compose.
  - apply Fix_unfold_subsume in H. destruct H as [m H]. general induction m; simpl in H.
    + apply Null_trace in H. left. rewrite H. repeat split; eauto using TC, partial, boundT.
    + apply TC_TCsubst in H.
      assert (tailrec (S n) (linearize (S n) s u.[ren (+1)])); eauto using linearize_tailrec, tailrec_lift.
      assert (tailrec 1 (linearize (S n) s u.[ren (+1)])).
      { apply tailrec_step with (n:= S n); eauto. omega. }
      apply tailrec_subst_trace_decompose with (sigma:= unfold (linearize (S n) s u.[ren (+1)]) m .: ids) (f:= shift) (xi:= xi) in H3; eauto using simulate_shift.
      destruct H3 as [[xi' [A1 [A2 A3]]]| [xi1 [xi2 [x [B2 [B3 [B4 [B5 [B6 B7]]]]]]]]].
      × destruct (IHtailrec (u.[ren(+1)]) xi') as [[A1a [A2a A3a]] | [[B1a [x [B2a B3a]] ] | [xi1 [xi2 [C1a [C2a [C3a [C4a C5a]]]]]]]]; eauto using tailrec_lift.
        { left. split.
          - constructor. rewrite A2. apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
          - rewrite A2. split; eauto using ren_partial_preserve, boundT_ren_shift_preserve. }
        { right. left. split.
          - constructor. rewrite A2. apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
          - destruct x.
            + exfalso. apply terminal_boundT_contradict with (n:= 1) (xi:= xi') (x:= 0); eauto.
            + ∃ x. split; try omega.
              rewrite A2. apply terminal_ren_shift_preserve; eauto. }
        { right. right. ∃ (ren_trace shift xi1), (ren_trace shift xi2).
          split.
          - rewrite A2. rewrite C1a. rewrite ren_concat_distribute. eauto.
          - split.
            + constructor. apply tailrec_subst_trace_compose1 with (n:= 1); eauto using simulate_shift.
              apply boundT_step with (n:= S n); eauto. omega.
            + repeat split; eauto using ren_total_preserve, boundT_ren_shift_preserve.
              rewrite (@ id_shift u). apply ren_trace_ren. eauto. }
      × destruct (IHtailrec (u.[ren(+1)]) xi1) as [[A1a [A2a A3a]] | [[B1a [y [B2a B3a]] ] | [xiA [xiB [C1a [C2a [C3a [C4a C5a]]]]]]]]; eauto using tailrec_lift.
        { exfalso. apply terminal_boundT_contradict with (n:= S n) (xi:= xi1) (x:= x); eauto. omega. }
        { assert (x = y); eauto using terminal_unique.
          assert (x = 0).
          { destruct x; eauto. exfalso. omega. }
          decide (partial xi1).
          - assert (xi = ren_trace shift (butLast xi1)).
            { rewrite B6. rewrite concat_partial_absorb_right; eauto using ren_butLast_distribute, butLast_partial_preserve, ren_partial_preserve. }
            left. split.
            + rewrite H5. constructor.
              apply tailrec_subst_trace_compose1 with (n:= 1); eauto using trace_partial_prefix2, simulate_shift.
            + rewrite H5. split; eauto using ren_partial_preserve, butLast_partial_preserve.
              apply tailrec_tailrec_trace with (n:= S n) in B1a; eauto using boundT_ren_shift_preserve, tailrec_trace_butLast_boundT.
          - apply not_partial_total in n0.
            assert (boundT (S n) (butLast xi1)).
            { apply tailrec_tailrec_trace with (n:= S n) in B1a; eauto using tailrec_trace_butLast_boundT. }
            destruct (IHm n s H0 IHtailrec u xi2) as [[A1b [A2b A3b]] | [[B1b [z [B2b B3b]] ] | [xiA [xiB [C1b [C2b [C3b [C4b C5b]]]]]]]]; eauto.
            + rewrite H4 in B3. asimpl in B3. eauto.
            + left. split.
              × constructor. rewrite B6. apply tailrec_subst_trace_compose2 with (x:= 0) (n:= 1); eauto using simulate_shift.
                rewrite <- H3 in B3a. rewrite H4 in B3a. eauto.
              × rewrite B6. split; eauto using concat_partial_preserve_right.
                apply boundT_concat_compose; eauto. rewrite ren_butLast_distribute.
                apply boundT_ren_shift_preserve. eauto.
            + right. left. split.
              × constructor. rewrite B6. apply tailrec_subst_trace_compose2 with (x:= 0) (n:= 1); eauto using simulate_shift.
                rewrite <- H3 in B3a. rewrite H4 in B3a. eauto.
              × ∃ z. split; eauto. rewrite B6. apply terminal_concat_compose with (n:= n); eauto.
                { rewrite ren_butLast_distribute. apply boundT_ren_shift_preserve. eauto. }
                { eauto using butLast_total_preserve, ren_total_preserve. }
            + right. right. ∃ (concat (butLast (ren_trace shift xi1)) xiA), xiB.
              rewrite B6, C1b. split; eauto using concat_assoc. split.
              × constructor. apply tailrec_subst_trace_compose2 with (x:= 0) (n:= 1); eauto using simulate_shift. rewrite <- H3 in B3a. rewrite H4 in B3a. eauto.
              × split.
                { apply concat_total_compose; eauto using butLast_total_preserve, ren_total_preserve. }
                { split; eauto. apply boundT_concat_compose; eauto.
                  rewrite ren_butLast_distribute. eauto using boundT_ren_shift_preserve. } }
        { assert (terminal x xiB).
          { apply terminal_concat_decompose_right with (n:= S n) (xiA := xiA); eauto.
            - rewrite <- C1a. eauto.
            - omega. }
          exfalso. apply terminal_boundT_contradict with (n:= 1) (xi:= xiB) (x:= x); eauto.
          apply bound_boundT with (s:= u.[ren(+1)]); eauto.
          apply bound_ren. intros. left. simpl. omega. }
Qed.

Lemma linearize_correct s u
  : tailrec 0 s
    → lin 0 u
    → CFPSeq s u =T linearize 0 s u.
Proof.
  intros. split; intros.
  - inv H1; eauto using TC.
     destruct linearize_correct1 with (n:= 0) (u:= u) (xi2:= xi2) (x:= 0) (s:= s) (xi1:= xi1) (xi:= xi1) as [A1 [A2 A3]]; eauto.
     decide (partial xi1).
     + rewrite concat_partial_absorb_right; eauto.
       apply A2; eauto. apply boundT_zero.
     + apply not_partial_total in n. apply A3; eauto.
       apply boundT_zero.
  - apply linearize_correct2 in H1; eauto using lin_tailrec.
    destruct H1 as [[A1 [A2 A3]] | [[B1 [x [B2 B3]]] | [xi1 [xi2 [C1 [C2 [C3 [C4 C5]]]]]]]].
    + apply trace_partial_Seq_left; eauto.
    + inv B2.
    + rewrite C1. constructor; eauto.
Qed.

Theorem linearize_correct_final s u
  : tailrec 0 s
    → lin 0 u
    → CFPSeq s u =T linearize 0 s u
       ∧ lin 0 (linearize 0 s u).
Proof.
  intros. split; eauto using linearize_correct, linearize_lin.
Qed.