Require Export LNProperties.

Ltac auto_star ::= auto with hopi.

Lemma open_genNu {V:Set}: ∀ (P:proc V) k x n, open k x (genNu n P) = genNu n (open (k+n) x P).
Proof.
  intros; gen k; induction n; simpl; auto; intros.
  - fequals. omega.
  - rewrite IHn. do 3 fequals. omega.
Qed.

Lemma close_genNu {V:Set}: ∀ (P:proc V) k x n, close k x (genNu n P) = genNu n (close (k+n) x P).
Proof.
  intros; gen k; induction n; simpl; auto; intros.
  - fequals. omega.
  - rewrite IHn. do 3 fequals. omega.
Qed.

Lemma fn_genNu {V:Set}: ∀ (P:proc V) n, fn (genNu n P) = fn P.
Proof.
  induction n; simpl; auto.
Qed.

Lemma is_proc_genNu {V:Set} : ∀ (P:proc V) n, (∀ x, x \in bn P → x < n)
    → is_proc (genNu n P).
Proof.
  intros; gen P; induction n; intros; simpl.
  - assert (bn P = \{}). autofs. forwards*: H x; auto. omega.
    apply is_proc_bn_rev; auto.
  - apply (proc_nu \{}). intros. unfold open. rewrite open_genNu.
    apply× IHn. intros. rewrite bn_open in H1. autofs.
    forwards*: H x0. destruct (classic (x0 =n)); intuition.
Qed.

Lemma mapN_genNu {V:Set}: ∀ n f (P:proc V),
    mapN f (genNu n P) = genNu n (mapN (liftN f n) P).
Proof.
  induction n; intros; simpl; auto.
  - rewrite× liftN_0.
  - rewrite IHn. rewrite× liftN_liftN.
Qed.

Hint Rewrite @fn_close @fn_genNu @fn_mapN @fn_mapV:fn.

Ltac autofn := intros_all;
 repeat (try(match goal with
| [ H: _ \in fn(open _ _ _) |- _ ] ⇒ apply fn_open_sub in H
| [ H: _ \in fn(subst _ _) |- _ ] ⇒ apply fn_subst in H
| H1 : fn (?A) \c _, H2 : _ \in fn(?A) |- _ ⇒ apply H1 in H2
end); substs; simpl in *; auto with fs; autorewrite with fn fs in *; intuition auto; destruct_hyps).

Hint Rewrite @bn_open @bn_mapN @bn_mapV:bn.

Ltac autobn := intros_all;
 repeat (try( match goal with
| [ H: _ \in bn(close _ _ _) |- _ ] ⇒ apply bn_close_sub in H
| [ H: _ \in bn(subst _ _) |- _ ] ⇒ apply bn_subst in H
| [ H: _ \in map_fset _ _ |- _ ] ⇒ apply map_fset_spec in H
| H1 : bn(?A) \c _, H2 : _ \in bn(?A) |- _ ⇒ apply H1 in H2
end); substs; simpl in *; auto with fs; autorewrite with bn fs in *; intuition auto; destruct_hyps).

Ltac notinFalse :=
repeat (match goal with
| [ H: _ \notin _ |- False ] ⇒ solve [apply H; autofs]
end).

Tactic Notation "autofnF" := autofn; try solve [false; notinFalse].

Tactic Notation "autobnF" := autobn; try solve [false; notinFalse].


Lemma lts_conc_wf : ∀ P l (C:conc), lts P l C → conc_wf C.
Proof.
  intros. gen_eq: (ag_conc C) as A. gen C.
  induction H; introv HC; try solve [inverts HC].
  - inverts HC. intros_all; omega.
  - destructA A; inverts HC. intros_all. forwards*: IHlts.
  - destructA A; inverts HC. intros_all. forwards*: IHlts.
  - destructA A; inverts HC.
    pick_fresh x. forwards*: H0 x. reflexivity. simpl in H1.
    rewrite bn_open in H1.
    case_if; intros_all.
    destruct (classic (k = n)); try (subst; auto).
    forwards*: H1 k. omega. autofs.
    forwards*: H1 k. autobnF. ∃ k; intuition. simpl_down.
Qed.

Lemma mapN_eq_on_bn {V:Set} : ∀ (P:proc V) f g,
  (∀ k, k \in bn P → f k = g k) → mapN f P = mapN g P.
Proof.
  induction P; intros; try solve [simpl; auto].
  - simpl. destruct n; try (rewrite H); try (erewrite IHP); eauto;
       simpl; try (intros; apply H); autobnF.
  - simpl. destruct n; try (rewrite H); try (erewrite IHP1);
     try (erewrite IHP2); eauto; simpl; try (intros; apply H); autobnF.
  - simpl; try (erewrite IHP1); try (erewrite IHP2); eauto;
      simpl; try (intros; apply H); autobnF.
  - simpl. erewrite IHP; eauto. intros. unfold liftN.
    case_if; auto. rewrite H; auto. simpl. rewrite down_fset_spec'.
    replace (S (k -1)) with k by omega. auto.
Qed.

Lemma down_id {V:Set}: ∀ (P:proc V) n, (∀ k, k \in bn P → k ≤ n)
      → mapN (down n) P = P.
Proof.
  intros. replace P with (mapN (fun x ⇒ x) P) at 2 by (rewrite× @mapN_id).
  apply mapN_eq_on_bn; intros. forwards*: H k. simpl_down.
Qed.

Lemma open_agent_injective: ∀ A A' k x, open_agent k x A = open_agent k x A' →
    x \notin fn_agent A → x \notin fn_agent A' → A = A'.
Proof.
  introv Haa' Hxa Hxa'; destructA A; destructA A'; inverts Haa';
    simpl in Hxa; simpl in Hxa'; try fequals; try fequals; eauto using open_injective.
Qed.

Lemma open_agent_id : ∀ k x A, is_agent A → open_agent k x A = A.
Proof.
  intros. destructA A; simpl.
  - rewrite× @open_id. simpl in ×. forwards: @is_proc_bn H. rewrite H0; autobnF.
  - rewrite× @open_id. simpl in ×. forwards: @is_proc_bn H. rewrite H0; autobnF.
  - simpl in ×. repeat rewrite× @open_id; intros_all; forwards: H (k+n); autofs;
    omega.
Qed.

Lemma open_agent_open_agent : ∀ A (k1 k2 : nat) (x0 y0 : var), k1 ≠ k2
    → open_agent k1 x0 (open_agent k2 y0 A) = open_agent k2 y0 (open_agent k1 x0 A).
Proof.
  intros. destructA A; simpl; rewrite× @open_open; try omega.
    rewrite (open_open _ (k1+n)); try omega. auto.
Qed.

Lemma fn_agent_open : ∀ A (k : nat) (x : var),
       (k \in bn_agent A → fn_agent (open_agent k x A) = fn_agent A \u \{ x})
     ∧ (k \notin bn_agent A → fn_agent (open_agent k x A) = fn_agent A).
Proof.
  intros; destructA A; simpl;
    try solve [forwards*: @fn_open; intuition eauto].
  split; intros.
    rewrite map_fset_spec in H. destruct H as [ y []].
    rewrite filter_fset_spec in H0. apply fset_extens.
    autofs; autofnF. intros_all. destruct H0. subst.
    replace (y-n+n) with y by omega. forwards*: @fn_open p y x.
    forwards*: @fn_open p0 y x0.
    autofs; try solve [left; match goal with
      | [H : ?A = _ |- ?x \in ?A ] ⇒ rewrite H; autofnF end];
      try solve [match goal with
        | [H : ?x0 \in fn ?P |- _ ] ⇒ apply fn_open_rev with P y x in H; autofs end].
    subst. right. rewrite H1; autofs.
    assert ((k+n) \notin bn p).
      intros_all. apply H. rewrite map_fset_spec. ∃ (k+n); intuition.
      rewrite filter_fset_spec; intuition. autofs.
    assert ((k+n) \notin bn p0).
      intros_all. apply H. rewrite map_fset_spec. ∃ (k+n); intuition.
      rewrite filter_fset_spec; intuition. autofs.
    forwards*: @fn_open p0 (k+n) x. forwards*: @fn_open p (k+n) x.
    intuition. rewrite H3, H6. auto.
Qed.

Lemma fn_agent_open_sub : ∀ A (k : nat) (x : var),
       fn_agent (open_agent k x A) \c fn_agent A \u \{ x}.
Proof.
  intros. forwards*:fn_agent_open A k x.
  destruct (classic (k \in bn_agent A)); intuition; rewrite H; autofs.
Qed.

Lemma fn_agent_amapN : ∀ A (f : nat → nat), fn_agent (amapN f A) = fn_agent A.
Proof.
  intros; destructA A; simpl; rewrite× @fn_mapN.
    rewrite× @fn_mapN.
Qed.

Lemma fn_agent_new : ∀ A, fn_agent (new A) = fn_agent A.
Proof.
  intros; destructA A; simpl; autofnF.
    case_if; autofnF.
Qed.

Lemma app_open: ∀ P Q R n k x,
   (ag_proc (appl (conc_def n (open (k + n) x P) (open (k + n) x Q)) (abs_def (open k x R))) =
   open_agent k x (ag_proc (appl (conc_def n P Q) (abs_def R)))) ∧
   (ag_proc (appr (abs_def (open k x R)) (conc_def n (open (k + n) x P) (open (k + n) x Q))) =
    open_agent k x (ag_proc (appr (abs_def R) (conc_def n P Q)))).
Proof.
  intros. simpl.
  split;
    rewrite mapN_open; auto using shiftN_injective;
    replace (n+k) with (k+n) by omega; rewrite <- open_subst;
    rewrite open_genNu; simpl; auto.
Qed.

Lemma appr_open: ∀ P Q R n k x,
   appr (abs_def (open k x R)) (conc_def n (open (k + n) x P) (open (k + n) x Q)) =
    open k x (appr (abs_def R) (conc_def n P Q)).
Proof.
  intros. forwards*: (app_open P Q R n k) x.
  destruct H. inverts H0. auto.
Qed.

Lemma parl_open : ∀ k x A P, parl (open_agent k x A)(open k x P)
  = open_agent k x (parl A P).
Proof.
  intros. destructA A; simpl; auto.
  - rewrite× @mapV_open.
  - rewrite mapN_open; auto using shiftN_injective.
    replace (k+n) with (n+k) by omega; auto.
Qed.

Lemma parr_open : ∀ k x A P, parr (open k x P)(open_agent k x A)
  = open_agent k x (parr P A).
Proof.
  intros. destructA A; simpl; auto.
  - rewrite× @mapV_open.
  - rewrite mapN_open; auto using shiftN_injective.
    replace (k+n) with (n+k) by omega; auto.
Qed.

Lemma new_open_agent : ∀ A x k,
 new (open_agent (S k) x A) = open_agent k x (new A).
Proof.
   intros; destructA A; simpl; auto.
    repeat case_if; auto.
   - replace (S (k+n)) with (k + S n) by omega; auto.
   - false. autobnF.
   - false. autobnF. omega.
   - simpl in ×.
     asserts_rewrite (mapN (down n) (open (S (k+ n)) x p) =
                      open (k+n) x (mapN (down n) p)).
      rewrite mapN_open_gen. fequals. simpl_down.
      intros. simpl_down. destruct k; try omega.
      subst. replace (S (0 + n) - 1) with n in H by omega. intuition.
     asserts_rewrite× (mapN (permut n) (open (S (k + n)) x p0) =
          open (S (k + n)) x (mapN (permut n) p0)).
      rewrite mapN_open; auto using permut_injective.
      repeat fequals. simpl_permut.
Qed.

Lemma is_agent_amapN : ∀ A f, is_agent A → amapN f A = A.
Proof.
  intros; destructA A; simpl; try solve [repeat fequals; auto using is_proc_mapN].
  simpl in H. replace p with (mapN (fun x ⇒ x) p) at 2 by (rewrite× @mapN_id).
  replace p0 with (mapN (fun x ⇒ x) p0) at 2 by (rewrite× @mapN_id).
  fequals. fequals; apply mapN_eq_on_bn; intros; forwards: H k; autofs; simpl_liftN.
Qed.

Lemma amapN_open : ∀ (k : nat) (x : var) A (f : nat → nat), injective f
    → open_agent (f k) x (amapN f A) = amapN f (open_agent k x A).
Proof.
  intros. destructA A; simpl;
    try solve [rewrite× @mapN_open].
  repeat (rewrite mapN_open); auto using liftN_preserves_injectivity.
  repeat (rewrite liftN_plus_n). replace (n+f k) with (f k+n) by omega.
  auto.
Qed.

Lemma bn_agent_open : ∀ A k x, bn_agent (open_agent k x A) = bn_agent A \- \{ k}.
Proof.
  intros; destructA A; simpl; auto using bn_open.
  apply fset_extens.
  + autobnF; try omega.
    ∃ x1; autobnF.
    ∃ x1; autobnF.
  + autobnF. ∃ x1. autofs. left. intuition.
    ∃ x1. autofs. right. intuition.
Qed.

Lemma is_agent_bn : ∀ A, is_agent A → bn_agent A = \{}.
Proof.
  intros. destructA A; simpl in *; auto using is_proc_bn.
  autofs; forwards*: H x0; autofs; omega.
Qed.

Lemma is_agent_bn_rev : ∀ A, bn_agent A = \{} → is_agent A.
Proof.
  intros. destructA A; simpl in *; auto using is_proc_bn_rev.
  intros; destruct (classic (k<n)); auto. false.
  assert ((k-n) \in map_fset (fun k ⇒ k - n)
            (filter_fset (fun k ⇒ k ≥ n) (bn p \u bn p0))).
   rewrite map_fset_spec. ∃ k; intuition.
   rewrite filter_fset_spec. intuition.
  rewrite H in H2; autofs.
Qed.

Lemma bn_agent_new : ∀ A, bn_agent (new A) = down_fset (bn_agent A \- \{ 0}).
Proof.
  intros. destructA A; simpl; auto.
  case_if.
  + apply fset_extens; intros_all. apply down_fset_spec'. apply map_fset_spec.
    apply map_fset_spec in H. destruct_hyps. apply filter_fset_spec in H0. destruct_hyps.
    ∃ x0. split. omega. apply filter_fset_spec. intuition.
    apply down_fset_spec' in H. apply map_fset_spec.
    apply map_fset_spec in H. destruct_hyps. apply filter_fset_spec in H0. destruct_hyps.
    ∃ x0. split. omega. apply filter_fset_spec. intuition.
  + apply fset_extens; intros_all. apply down_fset_spec'. apply map_fset_spec.
    apply map_fset_spec in H. destruct_hyps. apply filter_fset_spec in H0. destruct_hyps.
    ∃ (S x0). split. omega. apply filter_fset_spec. intuition. rewrite bn_mapN in H1.
    autofs. simpl_down. subst. assert (x=n) by omega. subst. intuition.
    replace (S (x-1)) with x by omega. autofs.
    simpl in H. rewrite down_fset_spec' in H. autobnF. simpl_permut. subst. intuition.
    apply down_fset_spec' in H. apply map_fset_spec in H. destruct_hyps.
    apply filter_fset_spec in H0. destruct H0.
    apply map_fset_spec. ∃ (x0-1). split. omega.
    apply filter_fset_spec. intuition. autofs.
    left. autobnF. ∃ x0. split×. simpl_down.
    right. autobnF. apply down_fset_spec'. replace (S (x0-1)) with x0 by omega.
    autofs. ∃ x0. split×. simpl_permut.
Qed.

Lemma decomp_agent_gen: ∀ A k x, k \notin bn_agent A →
    ∃ A', A = open_agent k x A' ∧ x \notin fn_agent A'.
Proof.
  intros. destructA A; simpl in ×.
  - forwards: @decomp_proc_gen p k x; auto. destruct H0 as [R].
    ∃ (ag_proc R). simpl. unfold decomp in *; intuition. fequals.
  - forwards: @decomp_proc_gen p k x; auto. destruct H0 as [R]. unfold decomp in ×.
    ∃ (ag_abs (abs_def R)). simpl. intuition. fequals.
  - forwards: @decomp_proc_gen p (k+n) x; auto.
      intros_all. apply H. rewrite map_fset_spec. ∃ (k+n).
      intuition. rewrite filter_fset_spec. intuition. autofs.
    destruct H0 as [R]. forwards: @decomp_proc_gen p0 (k+n) x.
      intros_all. apply H. rewrite map_fset_spec. ∃ (k+n).
      intuition. rewrite filter_fset_spec. intuition. autofs.
    destruct H1 as [R0].
    ∃ (ag_conc (conc_def n R R0)). simpl. intuition.
    subst×.
Qed.

Lemma decomp_agent: ∀ A k x,
    is_agent A → ∃ A', A = open_agent k x A' ∧ x \notin fn_agent A'.
Proof.
  intros. forwards*: decomp_agent_gen A k x. forwards*: is_agent_bn H.
  intros_all. rewrite H0 in H1. autofs.
Qed.

Lemma is_proc_app : ∀ (F:abs) (C:conc), is_agent F → is_agent C →
   is_proc (appl C F) ∧ is_proc (appr F C).
Proof.
  intros [P] [n Q R]. intros. simpl in ×.
  split; apply is_proc_genNu; intros;
    autobnF; try solve [apply H0; autobnF];
    try solve [apply is_proc_bn in H; rewrite H in H2; autofs].
Qed.

Lemma notin_fn_notin_fnlab : ∀ P l A x,
        lts P l A → x \notin fn P → x \notin fn_lab l.
Proof.
  induction 1; simpl; auto.
  pick_fresh y. intros. forwards*: H0 y. autofnF.
Qed.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | H: bn P = \{} |- _ ⇒ apply is_proc_bn_rev
  | |- is_proc (open _ _ (close _ _ _)) ⇒ apply is_proc_open_close; intuition
  | |- is_proc (mapN _ _) ⇒ rewrite is_proc_mapN; intuition
  | |- is_proc (mapV _ _) ⇒ apply is_proc_mapV; intuition
  | |- is_proc (bind _ _) ⇒ apply is_proc_bind; intuition
  end : hopi.

Hint Extern 1 (∀ (x:incV Empty_set), is_proc (_)) ⇒
    intros [|]; simpl; intuition:hopi.

Hint Extern 1 (is_proc (appr _ _)) ⇒ apply is_proc_app; intuition:hopi.
Hint Extern 1 (is_proc (appl _ _)) ⇒ apply is_proc_app; intuition:hopi.

Lemma lts_is_proc: ∀ P l A, is_proc P → lts P l A → is_agent A.
Proof.
  introv Hp Hlts; induction Hlts; simpl; inverts× Hp.
  - intros. apply is_proc_bn in H1. apply is_proc_bn in H3.
    rewrite H1 in H. rewrite H3 in H. autofs.
  - destructA A; simpl in *; auto with hopi.
    intros. specialize (IHHlts H1). apply IHHlts.
    autobnF. apply is_proc_bn in H2; rewrite H2 in H0; autofs.
  - destructA A; simpl in *; auto with hopi.
    intros. specialize (IHHlts H2). apply IHHlts.
    autobnF. apply is_proc_bn in H1; rewrite H1 in H0; autofs.
  - destructA A; simpl;
      try solve [apply (proc_nu (L \u fn_lab l \u L0));
                 auto; intros; forwards*: H0 x].
    pick_fresh y. forwards*: H2 y.
    case_if; intros.
    destruct (classic (k=n)); try omega.
    forwards: H0 H1 k; try solve [autobnF].
    asserts_rewrite (mapN (down n) p = p) in H3.
      rewrite× @down_id.
      intros. destruct (classic (k0 = n)); try omega.
      forwards: H0 H1 k0; autobnF; omega.
    destruct (classic (k=n)); try omega.
    false. subst. autobnF. rewrite down_fset_spec' in H6. autobnF. simpl_permut. subst.
    forwards*: H0 H1 (S n). autobnF.
    forwards*: H0 H1 k. autobnF.
    right. autobnF. rewrite down_fset_spec' in H7. autobnF. simpl_permut.
    assert (x=k) by omega. subst×. subst×. forwards*: H0 H1 (S k); autobnF.
Qed.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | H: lts _ _ (ag_proc P) |- _ ⇒ forwards*: @lts_is_proc H; intuition
  | H: lts _ _ (ag_abs (abs_def P)) |- _ ⇒ forwards*: @lts_is_proc H; intuition
  end : hopi.

Hint Extern 1 (is_agent ?A) ⇒
  match goal with
  | H: lts _ _ A |- _ ⇒ forwards: @lts_is_proc H; auto
  end : hopi.

Lemma fn_appr_appl : ∀ F C, fn (appr F C) \c fn_agent C \u fn_agent F
    ∧ fn (appl C F) \c fn_agent F \u fn_agent C.
Proof.
  intros. destruct F as []; destruct C as [].
    split; autofnF; intuition.
Qed.

Lemma fn_parl: ∀ A P, fn_agent (parl A P) = fn_agent A \u fn P.
Proof.
  intros. destructA A; simpl; try solve [autofnF; autofs].
Qed.

Lemma fn_parr: ∀ A P, fn_agent (parr P A) = fn_agent A \u fn P.
Proof.
  intros. destructA A; simpl; try solve [autofnF; autofs].
Qed.

Lemma lts_fn : ∀ P l A, lts P l A → fn_agent A \c fn P.
Proof.
  intros. induction H; simpl in *; try solve [autofs].
  - rewrite fn_parl; autofs.
  - rewrite fn_parr; autofs.
  - rewrite fn_agent_new. pick_fresh x. forwards*: H0 x.
    forwards: fn_agent_open_rev A 0 x. intros_all. assert (H4:= H3).
    apply H2 in H3. apply H1 in H3. autofnF.
  - forwards: fn_appr_appl F C. intros_all. apply H1 in H2.
    destruct F as []; destruct C as []; autofs. left.
    forwards: IHlts1 x. autofs. auto. forwards: IHlts1 x. autofs. auto.
  - forwards: fn_appr_appl F C. intros_all. apply H1 in H2.
    destruct F as []; destruct C as []; autofs.
    forwards: IHlts2 x. autofs. auto. forwards: IHlts2 x. autofs. auto.
Qed.

Definition subst_lab l (x y:var) :=
  match l with
  | out n ⇒ out (If (n=x) then y else n)
  | inp n ⇒ inp (If (n=x) then y else n)
  | _ ⇒ l
  end.

Lemma subst_lab_id : ∀ l x y, x \notin fn_lab l → subst_lab l x y = l.
Proof.
  intros; destruct l; simpl;
    try case_if; auto; try (false; autofnF).
Qed.

Lemma subst_lab_inv : ∀ l x y, y \notin fn_lab l → subst_lab (subst_lab l x y) y x = l.
Proof.
  intros; destruct l; simpl; repeat case_if; subst; auto;
    try (false; autofnF).
Qed.

Lemma subst_lab_rename : ∀ l x y z, y \notin fn_lab l →
    subst_lab (subst_lab l x y) y z = subst_lab l x z.
Proof.
  intros; destruct l; simpl; repeat case_if; subst; auto;
    try (false; autofnF).
Qed.

Lemma fn_subst_lab : ∀ l x y, fn_lab (subst_lab l x y) \c fn_lab l \u \{ y }.
Proof.
  intros; destruct l; simpl; repeat case_if; subst; autofs.
Qed.

Lemma lts_rename : ∀ P A l k x, is_proc (open k x P) → lts (open k x P) l (open_agent k x A) →
    x \notin fn P → x \notin fn_agent A →
    ∀ y, lts (open k y P) (subst_lab l x y) (open_agent k y A).
Proof.
  introv Hip Hlts. assert (is_agent (open_agent k x A)) by auto with hopi.
  remember (open k x P) as P'. remember (open_agent k x A) as A'. gen k x P A.
  induction Hlts; intros k x P' Hp A' Ha Hx HxA; destruct P'; inverts Hp; inverts Hip; simpl in Hx; intros.
  - destructA A'; inverts Ha. simpl. replace (k+0) with k in × by omega.
    destruct n; simpl in HxA; forwards*: @open_injective H4;
    forwards*: @open_injective H6; subst; clear H4 H6; repeat case_if; auto with hopi.
    inverts H1. autofs.
    inverts H1. auto with hopi.
  - destructA A'; inverts Ha. simpl.
    destruct n; simpl in HxA; forwards*: @open_injective H3;
    subst; clear H3; repeat case_if; auto with hopi.
    inverts H1. autofs.
    inverts H1. auto with hopi.
  - forwards*: decomp_agent A k x. destruct_hyps. subst.
    rewrite parl_open in Ha. forwards*: @open_agent_injective Ha. rewrite fn_parl. autofs.
    simpl. forwards*: IHHlts k x P'1 y. eapply lts_parl'; eauto.
    rewrite parl_open. rewrite× H0.
  - forwards*: decomp_agent A k x. destruct_hyps. subst.
    rewrite parr_open in Ha. forwards*: @open_agent_injective Ha. rewrite fn_parr. autofs.
    simpl. forwards*: IHHlts k x P'2 y. eapply lts_parr'; eauto.
    rewrite parr_open. rewrite× H0.
  - simpl. forwards*: decomp_agent_gen A (S k) x. apply is_agent_bn in H. rewrite bn_agent_new in H.
    apply down_fset_empty_rev in H. intros_all. apply H in H2. autofs. omega.
    destruct_hyps. rename x0 into A''.
    rewrite H2 in Ha. rewrite new_open_agent in Ha. forwards*: open_agent_injective Ha. rewrite fn_agent_new. auto.
    apply (lts_new' (L \u L0 \u fn_lab l \u fn P' \u \{x})) with (open_agent (S k) y A'').
    intros. rewrite× @open_open. rewrite× open_agent_open_agent. apply (H1 x0); auto.
    forwards*: H0 x0.
    rewrite× <- @open_open. rewrite× <- open_agent_open_agent. rewrite H2. auto.
    autofnF. intros_all. apply fn_agent_open_sub in H8. autofs.
    rewrite new_open_agent. rewrite× H5.
  - simpl. forwards*: decomp_agent C k x. destruct_hyps.
    destructA x0; inverts H0.
    forwards*: IHHlts1 k x P'1 (conc_def n p p0) y.
    assert (is_agent (conc_def n (open (k + n) x p) (open (k + n) x p0))) by auto with hopi.
    simpl in H0. intros. apply× H0.
    forwards*: decomp_agent F k x. destruct_hyps.
    destructA x0; inverts H4.
    forwards*: IHHlts2 k x P'2 (abs_def p1) y.
    eapply lts_taul'; eauto. forwards: (app_open p p0 p1 n k) x. destruct H6.
    simpl in Ha. rewrite H6 in Ha. clear H6 H7.
    replace (ag_proc (open k x (genNu n (p0 // subst ((shiftN n) p1) p))))
      with (open_agent k x (ag_proc (genNu n (p0 // subst ((shiftN n) p1) p)))) in Ha by reflexivity.
    forwards*: open_agent_injective Ha. autofnF.
    rewrite <- H6. forwards: (app_open p p0 p1 n k) y. destruct H7. simpl. rewrite× <- H7.
  - simpl. forwards*: decomp_agent C k x. destruct_hyps.
    destructA x0; inverts H0.
    forwards*: IHHlts2 k x P'2 (conc_def n p p0) y.
    assert (is_agent (conc_def n (open (k + n) x p) (open (k + n) x p0))) by auto with hopi.
    simpl in H0. intros. apply× H0.
    forwards*: decomp_agent F k x. destruct_hyps.
    destructA x0; inverts H4.
    forwards*: IHHlts1 k x P'1 (abs_def p1) y.
    eapply lts_taur'; eauto. forwards: (app_open p p0 p1 n k) x. destruct H6.
    simpl in Ha. rewrite H7 in Ha. clear H6 H7.
    replace (ag_proc (open k x (genNu n (subst ((shiftN n) p1) p // p0))))
      with (open_agent k x (ag_proc (genNu n (subst ((shiftN n) p1) p // p0)))) in Ha by reflexivity.
    forwards*: open_agent_injective Ha. autofnF.
    rewrite <- H6. forwards: (app_open p p0 p1 n k) y. destruct H7. simpl. rewrite× <- H8.
Qed.

Lemma lts_open : ∀ P P' A l k x, P = open k x P' → is_proc P → lts P l A → x \notin fn P'
      → ∃ A', A = open_agent k x A' ∧ (x \notin fn_agent A')
       ∧ (∀ y, lts (open k y P') (subst_lab l x y) (open_agent k y A')).
Proof.
  intros. forwards*: decomp_agent A k x. destruct_hyps. ∃ x0. intuition. subst.
  apply× lts_rename.
Qed.