Require Export Bisimulation.

Inductive struct_congr {V : Set} : binary (proc V) :=
| sc_par_assoc : ∀ P Q R, struct_congr (P // (Q // R)) ((P // Q) // R)
| sc_par_assoc_rev : ∀ P Q R, struct_congr ((P // Q) // R) (P // (Q // R))
| sc_par_comm : ∀ P Q, struct_congr (P // Q) (Q // P)
| sc_par_nil : ∀ P, struct_congr (P // PO) P
| sc_par_nil_conv : ∀ P, struct_congr P (P // PO)
| sc_scope: ∀ P Q, struct_congr (nu (P // (shiftN 1 Q))) ((nu P) // Q)
| sc_scope_rev: ∀ P Q, struct_congr ((nu P) // Q) (nu (P // (shiftN 1 Q)))
| sc_nu_nil : struct_congr (nu PO) PO
| sc_nu_nil_rev : struct_congr PO (nu PO)
| sc_nu_nu : ∀ P, struct_congr (nu nu P) (nu nu (mapN (permut 1) P))
| sc_nu_nu_rev : ∀ P, struct_congr (nu nu (mapN (permut 1) P)) (nu nu P)
| sc_nil : struct_congr PO PO
| sc_var : ∀ x, struct_congr (pr_var x) (pr_var x)
| sc_par : ∀ P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                              → struct_congr (P // P') (Q // Q')
| sc_inp : ∀ a P Q, @struct_congr (incV V) P Q → struct_congr (a? P) (a? Q)
| sc_out : ∀ a P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                                 → struct_congr (a!(P) P') (a!(Q) Q')
| sc_nu : ∀ L P Q, (∀ x, x \notin L → struct_congr (open 0 x P)(open 0 x Q))
                                              → struct_congr (nu P) (nu Q)
| sc_trans : ∀ P Q R, struct_congr P Q → struct_congr Q R → struct_congr P R
.

Hint Constructors struct_congr:sc.

Lemma sc_open {V : Set}: ∀ (P Q:proc V) k x,
    struct_congr P Q → struct_congr (open k x P)(open k x Q).
Proof with eauto with sc.
  introv H. gen k. induction H; simpl; intros...
  - rewrite <- mapN_open; auto using (shiftN_injective 1) with sc.
  - rewrite <- mapN_open; auto using (shiftN_injective 1) with sc.
  - replace (S (S k)) with (permut 1 (S (S k))) at 2 by (simpl_permut; try omega).
    rewrite <- (mapN_open P (S (S k)) x (permut 1)); eauto using (permut_injective 1) with sc.
  - replace (S (S k)) with (permut 1 (S (S k))) at 1 by (simpl_permut; try omega).
    rewrite <- (mapN_open P (S (S k)) x (permut 1)); eauto using (permut_injective 1) with sc.
  - apply (sc_nu L). intros. rewrite open_open... rewrite (open_open Q)...
Qed.

Lemma sc_nu' {V:Set}: ∀ (P Q:proc V), struct_congr P Q → struct_congr (nu P)(nu Q).
Proof.
  intros. apply (sc_nu (\{}:vars)). intros. apply sc_open; auto.
Qed.

Hint Resolve sc_nu':sc.

Lemma sc_refl {V : Set} : ∀ P, @struct_congr V P P.
Proof.
  induction P; auto with sc.
Qed.

Lemma sc_symmetric {V : Set} : ∀ (P Q:proc V),
  struct_congr P Q → struct_congr Q P.
Proof.
  intros P Q H. induction H; eauto with sc.
Qed.

Lemma sc_genNu {V:Set}: ∀ k (P Q:proc V), struct_congr P Q → struct_congr (genNu k P) (genNu k Q).
Proof.
  induction k; simpl; auto with sc.
Qed.

Hint Resolve sc_refl sc_symmetric sc_genNu:sc.

Lemma sc_close {V : Set}: ∀ (P Q:proc V) k x,
    struct_congr P Q → struct_congr (close k x P)(close k x Q).
Proof with eauto with sc.
  introv H. gen k. induction H; simpl; intros...
  - rewrite mapN_close. auto with sc.
  - rewrite mapN_close. auto with sc.
  - replace (S (S k)) with (permut 1 (S (S k))) at 2 by (simpl_permut; try omega).
    rewrite mapN_close. auto with sc.
  - replace (S (S k)) with (permut 1 (S (S k))) at 1 by (simpl_permut; try omega).
    rewrite mapN_close. eauto with sc.
  - apply (sc_nu (L \u \{x})). intros. rewrite <- close_open_neq...
    rewrite <- (close_open_neq Q)...
Qed.

Lemma sc_open_rev {V : Set}: ∀ k x (P Q:proc V), x \notin fn P \u fn Q →
   struct_congr (open k x P)(open k x Q) → struct_congr P Q.
Proof.
  intros. forwards*: @sc_close k x H0.
  do 2 (rewrite close_open in H1); try solve [autofnF].
Qed.

Lemma is_proc_sc {V:Set}: ∀ (P Q:proc V), struct_congr P Q → is_proc P → is_proc Q.
Proof with eauto with hopi sc.
  induction 1; intros Hp; inverts Hp...
  - inverts H2...
  - inverts H1...
  - pick_fresh_V V x. forwards: H0 x...
    inverts H... apply proc_par... apply (proc_nu L)... intros.
    eapply is_proc_rename... apply is_proc_bn in H4.
    assert ((bn Q) = \{}).
      apply fset_extens; autobnF.
      assert (S x0 \in map_fset (fun x ⇒ S x) (bn Q) \- \{0}).
      rewrite in_remove. split.
      rewrite map_fset_spec; auto. ∃ x0; intuition.
      rewrite notin_singleton; omega.
      rewrite H4 in H1; autobnF.
    apply is_proc_bn_rev...
  - inverts H1. apply (proc_nu L). intros.
    simpl. apply proc_par... rewrite is_proc_open...
  - apply (proc_nu (\{}:vars)). intros. simpl...
  - apply (proc_nu L). intros.
    forwards: H0 x... inverts H1. simpl. apply (proc_nu (L0 \u L)).
    intros. forwards: H3 x0... apply is_proc_bn in H2.
    repeat (rewrite bn_open in H2). apply is_proc_bn_rev.
    repeat (rewrite bn_open). autofs. autobnF.
    assert (x2 \in (bn P \- \{ 1}) \- \{0}).
      autofs; simpl_permut.
    rewrite H2 in H4. autofs.
  - apply (proc_nu L). intros.
    forwards: H0 x... inverts H1. simpl. apply (proc_nu (L0 \u L)).
    intros. forwards: H3 x0... apply is_proc_bn in H2.
    repeat (rewrite bn_open in H2). apply is_proc_bn_rev.
    repeat (rewrite bn_open). autofs. rewrite bn_mapN in H2.
    assert (x1 \in (map_fset (permut 1)(bn P) \- \{ 1}) \- \{0}).
      autofs. ∃ x1. simpl_permut; intuition.
    rewrite H2 in H8. autofs.
  - apply (proc_nu (L\u L0)). intros. eapply H0; eauto.
Qed.

Lemma sc_mapV: ∀ (V W:Set) P Q (f:V → W), @struct_congr V P Q
   → @struct_congr W (mapV f P) (mapV f Q).
Proof.
  intros. gen W.
  induction H;
  simpl; auto with sc; try (intros; rewrite mapV_mapN; auto with sc).
  - intros. apply (sc_nu L); eauto. intros. do 2 rewrite <- mapV_open.
    auto.
  - eauto with sc.
Qed.

Lemma sc_mapN: ∀ (V:Set) (P:proc V) Q f, injective f → struct_congr P Q
   → struct_congr (mapN f P) (mapN f Q).
Proof.
  intros. gen f. induction H0; simpl; auto with sc.
  - intros.
    replace (mapN (liftN f 1) (mapN (fun x ⇒ S x) Q)) with (mapN S (mapN f Q));
      auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. intros. simpl_liftN.
    auto with arith.
  - intros.
    replace (mapN (liftN f 1) (mapN (fun x ⇒ S x) Q)) with (mapN S (mapN f Q));
      auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. intros. simpl_liftN.
    auto with arith.
  - intros.
    replace (mapN (liftN (liftN f 1) 1) (mapN (permut 1) P)) with
                    (mapN (permut 1) (mapN (liftN (liftN f 1) 1) P)); auto with sc.
    repeat (rewrite mapN_mapN). fequals.
      extens; intros. simpl_liftN; simpl_permut.
  - intros.
    replace (mapN (liftN (liftN f 1) 1) (mapN (permut 1) P)) with
                    (mapN (permut 1) (mapN (liftN (liftN f 1) 1) P)); auto with sc.
    repeat (rewrite mapN_mapN). fequals.
      extens; intros. simpl_liftN; simpl_permut.
  - destruct a; simpl; auto with sc.
  - destruct a; simpl; auto with sc.
  - intros. apply sc_nu'. intros. pick_fresh_V V x. forwards*: H0 x (liftN f 1).
    apply× liftN_preserves_injectivity.
    do 2 (rewrite mapN_open in H2); auto using liftN_preserves_injectivity.
    eapply sc_open_rev; eauto. autofnF.
  - eauto with sc.
Qed.

Lemma sc_liftV: ∀ (V W:Set) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   (∀ x, @struct_congr (incV W) (liftV f x) (liftV g x)).
Proof.
  intros.
  destruct x; simpl; auto with sc.
  apply sc_mapV. auto with sc.
Qed.

Lemma sc_bind': ∀ (V W:Set) (P : proc V) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g P).
Proof.
  intros. gen W.
  induction P; intros; simpl; auto with sc.
  - apply sc_inp. apply IHP. intros. apply× sc_liftV.
  - apply sc_nu'. apply IHP. intros. apply× sc_mapN. apply (shiftN_injective 1).
Qed.

Hint Resolve sc_bind' sc_liftV sc_mapN sc_mapV:sc.

Lemma sc_bind: ∀ (V W:Set) (P Q : proc V) (f:V → proc W) (g:V → proc W), @struct_congr V P Q →
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g Q).
Proof.
  intros. gen W. induction H; simpl; try solve [auto with sc]; intros.
  - apply sc_trans with (bind f P // (bind f Q // bind g R)); auto with sc.
    apply sc_trans with (bind f P // (bind g Q // bind g R)); eauto with sc.
  - apply sc_trans with (bind f P // bind f Q // bind g R); auto with sc.
    apply sc_trans with (bind f P // bind g Q // bind g R); eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - replace (bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0) (f x))
        (mapN (fun x ⇒ S x) Q)) with (shiftN 1 (bind f Q)).
    apply sc_trans with (((nu bind (fun x : V ⇒ shiftN 1 (f x)) P) // bind f Q));
      auto using (shiftN_injective 1) with sc.
    rewrite bind_mapN. auto.
  - replace (bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0) (g x))
        (mapN (fun x ⇒ S x) Q)) with (shiftN 1 (bind g Q))
        by (rewrite bind_mapN;auto).
    apply sc_trans with (((nu bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0)(g x)) P) // bind g Q));
      auto using (shiftN_injective 1) with sc.
  - apply sc_trans with (nu nu bind (fun x : V ⇒ shiftN 1 (shiftN 1 (g x))) P).
    × repeat (apply sc_nu'). auto using (shiftN_injective 1) with sc.
    × asserts_rewrite ((fun x ⇒ mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (g x)))
        = (fun x ⇒ mapN (permut 1) (mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (g x))))).
        extens. intros. repeat (rewrite mapN_mapN).
      asserts_rewrite× ((fun x ⇒ S (S x))= fun x ⇒ permut 1 (S (S x))); auto.
        extens. simpl_permut.
      rewrite <-bind_mapN; auto with sc.
  - apply sc_trans with (nu nu bind (fun x : V ⇒ shiftN 1 (shiftN 1 (f x))) P).
    × asserts_rewrite ((fun x ⇒ mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (f x)))
         = (fun x ⇒ mapN (permut 1) (mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (f x))))).
        extens. intros. repeat (rewrite mapN_mapN).
      asserts_rewrite× ((fun x ⇒ S (S x))= fun x ⇒ permut 1 (S (S x))).
        extens. simpl_permut.
      rewrite <-bind_mapN; auto with sc.
    × repeat (apply sc_nu'). auto using (shiftN_injective 1) with sc.
  - apply sc_nu'. pick_fresh_fset_V V (
        (fn (bind (fun y ⇒ mapN (fun x1 ⇒ S x1) (f y)) P))
       \u (fn(bind (fun y ⇒ mapN (fun x1 ⇒ S x1) (g y)) Q))) x.
    forwards*: H0 x (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (f x0))
          (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (g x0)).
      intros. apply× sc_mapN. apply (shiftN_injective 1).
    assert (∀ (f: V → proc W), (fun y ⇒ open 0 x (mapN (fun x1 ⇒ S x1) (f y)))
      = fun y ⇒ (mapN (fun x1 ⇒ S x1) (f y))).
      intros. extens; intros. rewrite× @open_id. autobnF.
    rewrite <- (H3 f), <- (H3 g) in H2.
    do 2 (rewrite bind_open' in H2). eapply sc_open_rev; eauto. autofnF.
  - eauto with sc.
Qed.

Hint Resolve sc_bind:sc.

Lemma sc_nuK_permutK {V:Set}: ∀ k (P:proc V),
  struct_congr (genNu (S k) P) (genNu (S k) (mapN (permut k) P)).
Proof.
  induction k.
  - intros. simpl. erewrite mapN_id. auto with sc. simpl_permut.
  - intros. apply sc_trans with (genNu (S k)(mapN (permut k) (nu P))).
    Opaque mapN. simpl. rewrite nu_genNu.
    replace (nu genNu k (nu P)) with (genNu (S k) (nu P)) by reflexivity.
    apply IHk.
    replace (genNu (S (S k)) (mapN (permut (S k)) P)) with
      (genNu (S k)(nu (mapN (permut (S k)) P))) by (simpl; rewrite <- nu_genNu; auto).
    simpl. repeat (rewrite nu_genNu). apply sc_genNu.
    Transparent mapN. simpl.
    apply sc_trans with (nu nu mapN (permut 1)(mapN (liftN (permut k) 1) P)).
    auto with sc.
    replace (mapN (permut 1) (mapN (liftN (permut k) 1) P)) with (mapN (permut (S k)) P).
    auto with sc.
    rewrite mapN_mapN. fequals. extens; simpl_liftN; simpl_permut.
Qed.

Lemma sc_scope_genNu {V:Set}: ∀ k (P Q:proc V),
   struct_congr (genNu k (P // (shiftN k Q))) ((genNu k P) // Q).
Proof.
  induction k; intros.
  - simpl. rewrite mapN_id'; auto with sc.
  - simpl. repeat (rewrite nu_genNu).
    apply sc_trans with (genNu k ((nu P) // (mapN (fun x⇒k+x) Q))); auto.
    apply sc_genNu.
    replace (mapN (fun x ⇒ S (k + x)) Q)
         with (shiftN 1 (mapN (fun x ⇒ k+x) Q)). auto with sc.
    simpl. rewrite mapN_mapN. auto.
Qed.

Hint Resolve sc_scope_genNu:sc.

Lemma sc_scope_genNu' {V:Set}: ∀ n (P Q:proc V), (∀ k, k \in bn Q → k < n) →
  struct_congr (genNu n (nu P // Q)) (genNu n ((nu mapN (permut n) P) // Q)).
Proof.
  intros. apply sc_trans with (genNu n (nu (mapN (permut n)(P // Q)))).
  assert (∀ (P:proc V), genNu n (nu P) = genNu (S n) P).
    intros; induction n; simpl; auto. rewrite <- nu_genNu. auto.
  repeat (rewrite H0). apply sc_nuK_permutK.
  simpl. replace (mapN (permut n) Q) with (shiftN 1 Q); auto with sc.
  apply mapN_eq_on_bn. intros. forwards*: H k. simpl_permut; try omega.
Qed.

Lemma clusterfuck: ∀ Pr' k' P,
  bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0) (subst_func Pr' x))
       (mapN (liftN (fun x ⇒ k' + x) 1)(mapN (fun x ⇒ S x) P)) =
  ((shiftN 1)(subst ((shiftN k') (P)) Pr')).
Proof.
  intros. rewrite bind_mapN.
  simpl. repeat (rewrite mapN_mapN). repeat fequals.
    extens. intros; simpl_liftN.
Qed.

Lemma sc_new_A_shift: ∀ A (Q:proc0), sim_test struct_congr
  (new (parl A (mapN (fun x ⇒ S x) Q))) (parl (new A) Q).
Proof.
  intros; destruct_agent_sim A; intros; auto with sc.
  × simpl. rewrite (mapV_mapN _ _ (@VS _)). rewrite clusterfuck.
    auto with sc.
  × simpl. case_if. simpl. rewrite mapN_mapN. replace (fun x ⇒ n + S x) with
     (fun x ⇒ S (n + x)); auto with sc.
    extens; intros; omega.
    simpl.
    rewrite (mapN_mapN _ (fun x ⇒ S x) (fun x ⇒ n+x)).
    replace (fun x ⇒ n + S x) with (fun x ⇒ (S n) + x) by (extens; intros; omega).
    rewrite permut_shiftN; auto.
    replace ((shiftN (S n)) Q) with (shiftN 1 (shiftN n Q) )
    by (rewrite mapN_mapN; simpl; auto). auto with sc.
Qed.

Lemma sc_new_shift_A {V:Set}: ∀ A (P:proc V) f, is_agent A → sim_test struct_congr
 (new (parr (mapV f P) A)) (parr (mapV f (nu P)) A).
Proof.
  intros; destruct_agent_sim A; simpl in *; intros; auto with sc.
  × replace p with (shiftN 1 p) at 1 by apply× @is_proc_mapN. auto with sc.
  × replace p with (shiftN 1 p) at 1 by apply× @is_proc_mapN. rewrite clusterfuck.
    auto with sc.
  × case_if. false. forwards: H n. autobnF. omega. rewrite down_id.
    rewrite mapN_mapN. replace (mapN (permut n) p0) with (shiftN 1 p0).
    replace (mapN (fun x ⇒ permut n (n + x))(mapV f P))
      with (mapN (liftN (fun x ⇒ n + x) 1)(mapV f P)). eauto with sc.
    apply mapN_eq_on_bn. intros. simpl_liftN; simpl_permut.
    apply mapN_eq_on_bn. intros. forwards: H k. autobnF. simpl_permut.
    intros. forwards: H k. autofs. omega.
Qed.

Lemma sc_appl_new_conc: ∀ p p0 p1 n, is_proc p1 →
   (∀ k, k \in bn p \u bn p0 → k ≤ n) →
   struct_congr (nu genNu n (p0 // subst ((shiftN n) p1) p))
              (appl (conc_new (conc_def n p p0)) (abs_def p1)).
Proof.
  intros. simpl.
  case_if.
  - simpl. repeat (rewrite is_proc_mapN); auto with sc.
  - simpl. repeat (rewrite (is_proc_mapN p1)); auto. rewrite nu_genNu.
    rewrite down_id.
    apply sc_scope_genNu'. intros. forwards: @is_proc_bn H.
    destruct (classic (k = n)).
    subst. false. autobnF. rewrite H2 in H3; autobnF.
    autobnF. rewrite H2 in H4; autobnF. forwards: H0 k; autobnF. omega.
    intros. forwards: H0 k; autofs.
Qed.

Lemma sc_appr_new_abs: ∀ p p0 p1 n, is_agent (conc_def n p p0) →
  struct_congr (nu genNu n (subst ((shiftN n) p1) p // p0))
      (appr (abs_new (abs_def p1)) (conc_def n p p0)).
Proof.
  intros. simpl. rewrite nu_genNu. apply sc_trans with (genNu n
     ((nu mapN (permut n) ((subst ((shiftN n) p1) p))) //
         p0)). apply sc_scope_genNu'. simpl in H.
  intros; forwards: H k; autofs.
  replace (mapN (permut n) (subst ((shiftN n) p1) p)) with (bind
            (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0) (subst_func p x))
            (mapN (liftN (fun x ⇒ n + x) 1) p1)); auto with sc.
  rewrite bind_mapN. fequals.
  + extens; intros [|]; auto. simpl. apply mapN_eq_on_bn.
    intros. simpl in H. forwards: H k; autofs. simpl_permut.
  + rewrite mapN_mapN. apply mapN_eq_on_bn. intros.
    simpl_liftN; simpl_permut.
Qed.

Lemma sc_nuK_compL_permutK {V:Set}: ∀ k l (P:proc V),
  struct_congr (genNu (S k) P) (genNu (S k) (mapN (comp l (permut k)) P)).
Proof.
  induction l; intros.
  - simpl. erewrite mapN_id; auto with sc.
  - apply sc_trans with (genNu (S k) (mapN (permut k)(mapN (comp l (permut k)) P))).
    apply sc_trans with (genNu (S k) (mapN (comp l (permut k)) P)); auto.
    apply sc_nuK_permutK.
    rewrite mapN_mapN. simpl. auto with sc.
Qed.

Lemma sc_nuK_permut1 {V:Set}: ∀ (P:proc V) k,
    struct_congr (genNu (S (S k)) P)(genNu (S (S k))(mapN (liftN (permut 1) k) P)).
Proof.
  intros. apply sc_trans with (genNu (S (S k))(mapN (permut (S k)) P)).
  apply sc_nuK_permutK.
  apply sc_trans with (genNu (S (S k))(mapN (comp k (permut k))(mapN (permut (S k)) P))).
  apply sc_nu'. fold (@genNu V). apply sc_nuK_compL_permutK.
  replace (mapN (comp k (permut k)) (mapN (permut (S k)) P))
            with (mapN (liftN (permut 1) k) P); auto with sc.
  rewrite mapN_mapN; fequals; extens; intros.
  destruct k.
  - simpl. rewrite× liftN_0.
  - unfold liftN. case_if.
    + rewrite compK_permutK_leb; auto; simpl_permut; try omega.
      replace (S k+(x1+1)) with (x1 + 1*(S (S k))) by omega.
      rewrite Nat.mod_add; auto. rewrite Nat.mod_small; try omega.
    + destruct (classic (x1 = S k)). subst.
      rewrite compK_permutK_gt; simpl_permut; omega.
      destruct (classic (x1=(S (S k)))). subst.
      rewrite compK_permutK_leb; try omega.
      rewrite Nat.mod_small; simpl_permut; try omega. simpl_permut.
      rewrite compK_permutK_gt; try (simpl_permut; omega).
Qed.


Lemma nu_nu_conc: ∀ F k Q R, is_agent (ag_abs F) →
    struct_congr (appr F (conc_new (conc_new (conc_def k Q R))))
          (appr F (conc_new (conc_new (cmapN (permut 1) (conc_def k Q R))))).
Proof.
  intros [P'] k Q R Hf. simpl.
  case_if.
  + simpl. case_if.
     ×
       assert (k \in bn (mapN (liftN (permut 1) k) Q)).
         autobnF. ∃ (S k). simpl_name. destruct k; try omega. destruct k; try omega.
       case_if. simpl.
       assert (S k \in bn (mapN (liftN (permut 1) k) Q)).
         autobnF. ∃ k. simpl_name.
       case_if. simpl.
       replace (subst (mapN (fun x ⇒ (S (S (k+x)))) P') (mapN (liftN (permut 1) k) Q)) with
                   (mapN (liftN (permut 1) k) (subst ((shiftN (S (S k))) P') Q)).
       replace (mapN (liftN (permut 1) k) (subst ((shiftN (S (S k))) P') Q) //
                  mapN (liftN (permut 1) k) R) with
          (mapN (liftN (permut 1) k) (subst ((shiftN (S (S k))) P') Q // R))
       by reflexivity.
       apply sc_nuK_permut1.
       replace (fun x ⇒ S (S (k + x))) with (fun x ⇒ S (S k)+x)
                                                by (extens; intros; omega).
       rewrite subst_mapN. fequals.
       rewrite mapN_mapN. apply mapN_eq_on_bn; intros.
       unfold liftN; repeat case_if; simpl_permut. omega.
    ×
      assert (k \notin bn (mapN (liftN (permut 1) k) Q)).
         autobnF. simpl_name. assert (x = S k) by omega. substs. intuition.
      case_if. simpl.
      assert (k \in bn (mapN (down k) (mapN (liftN (permut 1) k) Q))).
         autobnF. ∃ (S k). simpl_name. autobnF. ∃ k. repeat case_if; try omega.
         intuition.
      case_if; simpl.
      asserts_rewrite (mapN (permut k) (mapN (liftN (permut 1) k) R) = mapN (permut (S k)) R).
        rewrite mapN_mapN. fequals. extens; simpl_name.
      asserts_rewrite (mapN (down k) (mapN (liftN (permut 1) k) Q) = mapN (down (S k)) Q).
        rewrite mapN_mapN. apply mapN_eq_on_bn; intros. simpl_name.
        assert (k0 = S k) by omega. subst. intuition.
      auto with sc.
  + simpl. case_if.
    ×
      assert (k \in bn (mapN (liftN (permut 1) k) Q)).
        autobnF. ∃ x. intuition. simpl_name.
      case_if; simpl.
      assert (S k \notin bn (mapN (liftN (permut 1) k) Q)).
        autobnF. clear H H2 H4. simpl_name. assert (x= k) by omega. substs. intuition.
      case_if; simpl.
      asserts_rewrite (mapN (permut (S k))(mapN (liftN (permut 1) k) R) = mapN (permut k) R).
        rewrite mapN_mapN. apply mapN_eq_on_bn; intros. simpl_name.
      asserts_rewrite (mapN (down (S k)) (mapN (liftN (permut 1) k) Q) = mapN (down k) Q).
        rewrite mapN_mapN. apply mapN_eq_on_bn; intros. simpl_name. assert (k=k0) by omega.
        subst. intuition.
      auto with sc.
    ×
      assert (S k \notin bn Q).
        autobnF. apply C0. ∃ (S k); intuition. simpl_name.
      assert (k \notin bn (mapN (liftN (permut 1) k) Q)).
        autobnF. simpl_name. assert (x = S k) by omega. substs. intuition.
      simpl. case_if. simpl.
      assert (k \notin bn (mapN (down k) (mapN (liftN (permut 1) k) Q))).
        autobnF. assert (x0 = k ∨ x0 = S k) by simpl_name. intuition.
        substs. intuition. substs. autofs.
      case_if. simpl.
      clear H0 C0 C1 C2 H1.
      asserts_rewrite (mapN (liftN (permut 1) k) Q = Q).
        replace Q with (mapN (fun x ⇒ x) Q) at 2 by (rewrite× @mapN_id).
        apply mapN_eq_on_bn; intros. simpl_name. assert (k0=k) by omega. false.
        assert (k0=S k) by omega. false.
      asserts_rewrite (mapN (liftN (permut k) 1)(mapN (permut k)(mapN (liftN (permut 1) k) R)) =
         mapN (permut 1) (mapN (liftN (permut k) 1)(mapN (permut k) R))).
        repeat (rewrite mapN_mapN). apply mapN_eq_on_bn; intros.
        destruct (classic (k0 < k)).
         simpl_name. destruct (classic (k0 = k)). subst.
         replace (permut k k) with 0 by simpl_permut.
         replace (liftN (permut k) 1 0) with 0 by simpl_liftN.
         replace (liftN (permut 1) k k) with (S k) by simpl_name. simpl_name.
         replace (permut k k0) with k0 by simpl_permut.
         destruct (classic (k0 = S k)). subst.
         replace (liftN (permut k) 1 (S k)) with 1 by simpl_name.
         replace (liftN (permut 1) k (S k)) with k by (simpl_name; destruct k; omega). simpl_name.
         replace (liftN (permut k) 1 k0) with k0 by simpl_name.
         replace (liftN (permut 1) k k0) with k0 by simpl_name. simpl_name.
      auto with sc.
Qed.

Lemma sc_nu_nu_permut : ∀ A,
  sim_test struct_congr (new (new A)) (new (new (amapN (permut 1) A))).
Proof.
  intros; destruct_agent_sim A; auto with sc.
  × simpl.
    replace (bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0)
      (mapN (fun x0 ⇒ S x0) (subst_func p0 x)))(mapN (liftN (liftN (fun x ⇒ n + x) 1) 1)
               (mapN (permut 1) p))) with
      (mapN (permut 1)(bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0)
               (mapN (fun x0 ⇒ S x0) (subst_func p0 x)))(mapN (liftN (liftN (fun x ⇒ n + x) 1) 1)
               p))); auto with sc.
    erewrite bind_mapN. fequals.
      extens. intros [ | ]; simpl; auto.
      repeat (rewrite mapN_mapN). apply mapN_eq_on_bn; intros. simpl_permut.
      repeat (rewrite mapN_mapN). apply mapN_eq_on_bn; intros.
      repeat (rewrite liftN_liftN). simpl. simpl_liftN; simpl_permut.
  × apply× nu_nu_conc.
Qed.

Lemma sc_appr_appl: ∀ F C,
   struct_congr (appr F C) (appl C F) ∧ struct_congr (appl C F) (appr F C).
Proof.
  intros; destruct C as [ n Q R]. destruct F as [ S ]; simpl.
  auto with sc.
Qed.

Hint Resolve sc_appr_appl:sc.

Lemma sc_newF_C: ∀ F C, is_agent (ag_conc C) →
    struct_congr (appr (abs_new F) C) (nu appr F C).
Proof.
  intros; destruct C as [n Q R]; destruct F as [P]. apply sc_symmetric.
   apply× sc_appr_new_abs.
Qed.

Lemma sc_F_newC : ∀ F Q R n, is_agent (ag_abs F) →
    (∀ k : nat, k \in bn Q \u bn R → k ≤ n) →
    struct_congr (appr F (conc_new (conc_def n Q R))) (nu appr F (conc_def n Q R)).
Proof.
  intros.
  apply sc_trans with (appl (conc_new (conc_def n Q R)) F); auto.
  apply sc_appr_appl. apply sc_symmetric.
  apply sc_trans with (nu appl (conc_def n Q R) F). apply sc_nu'. apply sc_appr_appl.
  destruct F as [ P ]. apply× sc_appl_new_conc.
Qed.

Lemma struct_congr_sim' {V : Set} : ∀ P Q f, @struct_congr V P Q → is_proc P → is_proc Q →
  ∀ P' l A, lts P' l A → P' = (mapV f P) →
  ∃ A', lts (mapV f Q) l A' ∧ sim_test struct_congr A A'.
Proof.
  intros P Q f Hstruct HprocP HprocQ.
  induction Hstruct; intros P'' l A Hlts Hp'; subst.
  -
    inverts Hlts.
    +
      ∃ (parl (parl A0 (mapV f Q)) (mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    + inversion H3; subst.
     ×
      ∃ (parl (parr (mapV f P) A) (mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (parr ((mapV f P)// (mapV f Q)) A). split;simpl.
      eapply lts_parr'; subst; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (ag_proc(appl (conc_parr (mapV f P) C) F)).
      split. eapply lts_taul'; eauto with hopi. eapply lts_parr'. apply H1. simpl; auto with hopi.
      apply st_proc.
      destruct C. simpl.
      apply sc_trans with (genNu n ((p0 // asubst (fshiftN n F) p) // (shiftN n)(mapV f P))); eauto with sc.
     ×
      ∃ (ag_proc(appr (abs_parr (mapV f P) F) C)).
      split. eapply lts_taur'; eauto with hopi. eapply lts_parr'; eauto.
      apply st_proc. destruct C as [ n Q' R']; simpl. destruct F as [ S ]; simpl.
      apply sc_trans with (genNu n (shiftN n (mapV f P) // (subst ((shiftN n) S) Q' // R'))); eauto with sc.
      apply sc_genNu. rewrite <- (mapV_mapN _ _(@VS _)). rewrite subst_shift. auto with sc.
    +
      inversion H4; subst.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        ∃ (ag_proc(appl C F' // mapV f R)).
        split. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        ∃ (ag_proc(appl (conc_parl C (mapV f Q)) F')).
        split. eapply lts_taul'; eauto with hopi. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. auto with sc.
    +
      inversion H4; subst.
      ×
        destruct A as [| | C']; inversion H5; subst.
        ∃ (ag_proc(appr F C' // mapV f R)).
        split. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        eauto with sc.
      ×
        destruct A as [| | C']; inversion H5; subst.
        ∃ (ag_proc(appr (abs_parl F (mapV f Q)) C')).
        split. eapply lts_taur'; eauto with hopi. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        repeat (rewrite <- (mapV_mapN _ _ (@VS _))). rewrite subst_shift. auto with sc.
  -
    inversion Hlts; subst.
    + inversion H3; subst.
     ×
      ∃ (parl A (mapV f Q // mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (parr (mapV f P) (parl A (mapV f R))). split;simpl.
      eapply lts_parr'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (ag_proc (appl C (abs_parl F (mapV f R)))).
      split. eapply lts_taul'; eauto with hopi. eapply lts_parl'; eauto with hopi.
      apply st_proc.
      destruct C. simpl. destruct F as [ P' ]; simpl.
      rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
     ×
      ∃ (ag_proc(appr F (conc_parl C (mapV f R)))).
      split. eapply lts_taur'; eauto with hopi. eapply lts_parl'; eauto.
      apply st_proc. destruct C as [ n Q' R']; simpl. destruct F as [ P' ]; simpl. eauto with sc.
    +
      eexists. split. eapply lts_parr'; eauto. eapply lts_parr'; eauto. fold (@mapV V).
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      inversion H1; subst.
      ×
        destruct A as [| | C']; inversion H5; subst.
        eexists. split. eapply lts_taul'; eauto with hopi. eapply lts_parr'; eauto with hopi.
        fold (@mapV V). simpl; eauto.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        repeat (rewrite <- (mapV_mapN _ _ (@VS _))). rewrite subst_shift. auto with sc.
      ×
        destruct A as [| | C']; inversion H5; subst.
        eexists. split. eapply lts_parr'; eauto with hopi. fold (@mapV V).
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl. eauto with sc.
   +
      inversion H1; subst.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        eexists. split. eapply lts_taur'; eauto with hopi. eapply lts_parr'; eauto with hopi. simpl; eauto.
        fold (@mapV V). destruct C as [ n Q' R']. destruct F' as [ S ]; simpl. apply st_proc.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. auto with sc.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        eexists. split. eapply lts_parr'; eauto with hopi. fold (@mapV V).
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
  -
    inversion Hlts; subst.
    +
      ∃ (parr (mapV f Q) A0). split; subst; simpl; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      ∃ (parl A0 (mapV f P)). split; subst; simpl; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      ∃ (ag_proc (appr F C)).
      split. eapply lts_taur'; eauto with hopi. apply st_proc. apply sc_appr_appl.
    +
      ∃ (ag_proc (appl C F)).
      split. eapply lts_taul'; eauto with hopi. apply st_proc. apply sc_appr_appl.
  -
    inversion Hlts; subst.
    + ∃ A0; subst; split; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    + inversion H3.
    + inversion H4.
    + inversion H4.
  -
    eexists. split. eapply lts_parl'; eauto. destruct_agent_sim A; simpl; eauto with sc.
  -
    inversion Hlts; subst. inverts HprocP.
    pick_fresh_V V x. forwards*: H0 x.
    simpl in H. inversion H; subst.
    +
      forwards: lts_open H5; eauto with hopi. forwards: H1 x; eauto.
        inverts H2. rewrite <- mapV_open. auto with hopi.
        autofnF.
      destruct H2 as [A' [Ha' [Hx HltsA' ]]].
      ∃ (parl (new A') (mapV f Q)). split; subst; simpl; eauto with hopi.
      eapply lts_parl'; eauto. apply (lts_new L). intros.
      specialize (HltsA' x0). rewrite subst_lab_id in HltsA'; auto.
      rewrite parl_open in H6.
      forwards:open_agent_injective (parl A' (mapV f (mapN (fun x ⇒ S x) Q))) A0; eauto.
      rewrite fn_parl. autofnF. subst. rewrite mapV_mapN. apply sc_new_A_shift.
    +
      inverts HprocQ. rewrite is_proc_mapN in H5; auto.
      rewrite open_id in H5.
      ∃ (parr (mapV f (nu P)) A).
      split. simpl. eapply lts_parr'; eauto.
      rewrite <- (open_agent_id 0 x A) in H6; auto with hopi.
      rewrite parr_open in H6. forwards: open_agent_injective H6; auto.
        intros_all. rewrite fn_parr in H2. autofnF. forwards: @lts_fn H5. autofnF.
      subst. apply sc_new_shift_A. auto with hopi.
      forwards: @is_proc_bn H7. autobnF. rewrite H2 in H3. autofs.
    +
      inverts HprocQ. rewrite is_proc_mapN in H7; auto. rewrite open_id in H7.
      forwards: lts_open H6; eauto with hopi. forwards: H1 x; eauto.
        inverts H2. rewrite <- mapV_open. auto with hopi.
        autofnF.
      destruct H2 as [A' [Ha' [Hx HltsA' ]]].
      destruct A' as [ | [] | C' ]; inverts Ha'.
      ∃ (ag_proc (appl (conc_new C') F)). split.
      simpl. eapply lts_taul'; eauto with hopi.
      apply (lts_new' L) with C'; eauto. intros_all.
      specialize (HltsA' x0). rewrite subst_lab_id in HltsA'. auto.
        simpl. forwards: notin_fn_notin_fnlab H7; eauto. intros_all; autofnF.
      destruct C'. destruct F. inverts H3.
      rewrite <- (open_id p1 0 x) in H4. forwards: (app_open p p0 p1 n 0) x.
      destruct H2. inverts H2. simpl in H4. rewrite H10 in H4. clear H3 H10.
      replace (ag_proc (open 0 x (genNu n (p0 // subst ((shiftN n) p1) p)))) with
        (open_agent 0 x (ag_proc (genNu n (p0 //subst ((shiftN n) p1) p)))) in H4 by auto.
      forwards: open_agent_injective H4; auto.
        simpl. intros_all. autofnF. forwards: @lts_fn H7. simpl in H12. apply H12 in H2. autofnF.
      rewrite <- H2. apply st_proc. apply sc_appl_new_conc; auto with hopi.
        simpl. intros. forwards: lts_is_proc H6; auto with hopi. forwards: H1 x; auto.
        inverts H9; auto with hopi. rewrite <- mapV_open. auto with hopi.
        simpl in H9. destruct (classic (k = n)); try omega.
        repeat(rewrite bn_open in H9). rewrite <- union_remove in H9.
        forwards: H9 k. rewrite in_remove. rewrite notin_singleton. intuition. omega.
      assert (is_proc p1) by auto with hopi. apply is_proc_bn in H2. rewrite H2; auto.
      apply is_proc_bn in H8. autobnF. rewrite H8 in H2; autofs.
    +
      inverts HprocQ. rewrite is_proc_mapN in H7; auto. rewrite open_id in H7.
      forwards: lts_open H6; eauto with hopi. forwards: H1 x; eauto.
        inverts H2. rewrite <- mapV_open. auto with hopi.
        autofnF.
      destruct H2 as [A' [Ha' [Hx HltsA' ]]].
      destruct A' as [ | F' | [] ]; inverts Ha'.
      ∃ (ag_proc (appr (abs_new F') C)). split.
      simpl. eapply lts_taur'; eauto with hopi.
      apply (lts_new' L) with F'; eauto. intros_all.
      specialize (HltsA' x0). rewrite subst_lab_id in HltsA'. auto.
        simpl. forwards: notin_fn_notin_fnlab H7; eauto. intros_all; autofnF.
      destruct C. destruct F'. inverts H3.
      assert (is_agent (conc_def n p p0)) by auto with hopi. simpl in H2.
      rewrite <- (open_id p n x) in H4; try (intros_all; forwards: H2 n; autofs; omega).
      rewrite <- (open_id p0 n x) in H4; try (intros_all; forwards: H2 n; autofs; omega).
      forwards: (app_open p p0 p1 n 0) x.
      destruct H3. inverts H9. simpl in H4. rewrite H11 in H4. clear H3 H11.
      replace (ag_proc (open 0 x (genNu n (subst ((shiftN n) p1) p //p0)))) with
        (open_agent 0 x (ag_proc (genNu n (subst ((shiftN n) p1) p//p0)))) in H4 by auto.
      forwards: open_agent_injective H4; auto.
        simpl. forwards: @lts_fn H7. autofnF.
        forwards: subset_union_weak_l (fn p) (fn p0). apply H12 in H9. apply H3 in H9.
        autofnF.
        forwards: subset_union_weak_r (fn p) (fn p0). apply H9 in H12.
        apply H3 in H12. autofnF.
      rewrite <- H3. apply st_proc. apply sc_appr_new_abs; auto with hopi.
      apply is_proc_bn in H8. autobnF. rewrite H8 in H2; autobnF.
  -
    inverts HprocQ. inverts HprocP.
    inverts Hlts.
    +
      inverts H6. pick_fresh_V V x. forwards*: H1 x.
      ∃ (new (parl A (mapV f Q))). split.
      eapply (lts_new L); eauto. fold (@mapV V). intros.
      simpl. rewrite <- parl_open.
      eapply lts_parl'; eauto. forwards× HltsA': @lts_rename H x0.
        forwards*: H0 x. inverts H6. rewrite <- mapV_open. auto with hopi.
        autofnF.
      rewrite subst_lab_id in HltsA'; auto with hopi. apply HltsA'.
      rewrite is_proc_mapN; auto.
      apply sim_test_sym. intros_all; auto with sc.
      replace (mapV f Q) with (shiftN 1 (mapV f Q)) at 1 by (rewrite is_proc_mapN; auto with hopi).
      apply sc_new_A_shift.
    +
      ∃ (new (parr (mapV f P) A0)). split. eapply (lts_new L); eauto.
      fold (@mapV V). intros. simpl. rewrite <- parr_open.
      eapply lts_parr'; eauto. rewrite× @is_proc_mapN.
      rewrite open_id. rewrite open_agent_id; auto with hopi.
      forwards: @is_proc_bn H3. autobnF. rewrite H4 in H5; autofs.
      apply sim_test_sym. intros_all; auto with sc.
      apply sc_new_shift_A; auto with hopi.
    +
      inverts H4. destruct A; inverts H1.
      ∃ (new (ag_proc (appl c F))).
      split. eapply (lts_new (L0 \u \{ a })); auto with hopi. fold (@mapV V). intros.
      simpl. forwards*: H6 x. destruct c.
      eapply lts_taul'; eauto with hopi.
      rewrite× @is_proc_mapN. rewrite open_id; eauto.
      forwards: @is_proc_bn H3. autobnF. rewrite H5 in H8; autofs.
      destruct F. rewrite <- (open_id p1 0 x) at 1.
      simpl. forwards: (app_open p p0 p1 n 0) x; intuition.
      forwards: @is_proc_bn p1; auto with hopi. rewrite H5. auto.
      apply sim_test_sym. intros_all; auto with sc.
      apply st_proc. destruct c; destruct F; apply sc_appl_new_conc; auto with hopi.
      pick_fresh_V V x. forwards: H6 x; auto.
      assert (is_agent (conc_def n (open n x p) (open n x p0))).
        forwards: H0 x; auto with hopi. inverts H1.
        forwards: @lts_is_proc H; auto. rewrite <- mapV_open; auto with hopi.
      simpl in H1. intros. repeat(rewrite bn_open in H1). rewrite <- union_remove in H1.
      destruct (classic (k=n)); try omega. forwards*: H1 k. autobnF. omega.
    +
      inverts H4. destruct A; inverts H1.
      ∃ (new (ag_proc (appr a0 C))). split.
      eapply (lts_new (L0 \u \{ a })); auto with hopi. fold (@mapV V). intros.
      simpl. forwards*: H6 x. destruct a0.
      eapply lts_taur'; eauto with hopi.
      rewrite× @is_proc_mapN. rewrite open_id; eauto.
      forwards: @is_proc_bn H3. autobnF. rewrite H5 in H8; autofs.
      destruct C. assert (is_agent (conc_def n p0 p1)); auto with hopi.
      rewrite <- (open_id p1 n x) at 1; try (intros_all; forwards: H5 n; autofs; omega).
      rewrite <- (open_id p0 n x) at 1; try (intros_all; forwards: H5 n; autofs; omega).
      simpl. forwards: (app_open p0 p1 p n 0) x; intuition.
      apply sim_test_sym. intros_all; auto with sc.
      apply st_proc. destruct C; destruct a0; apply sc_appr_new_abs; auto with hopi.
  - simpl in Hlts; inversion Hlts. pick_fresh_V V x. forwards*: H0 x.
    simpl in H3; inverts H3.
  - inversion Hlts.
  -
    inverts Hlts. inverts HprocP. pick_fresh_V V x. forwards*: H0 x.
    simpl in ×. inverts H. forwards*: H1 x. inverts H.
    forwards*: decomp_agent_gen A 1 x.
      pick_fresh y.
      assert (is_agent (open_agent 0 y A)).
      forwards*: H5 y.
      forwards: lts_is_proc H; auto with hopi. forwards*: H4 y.
      rewrite <- mapV_open. rewrite <- mapV_open. auto with hopi.
      apply is_agent_bn in H. rewrite bn_agent_open in H. intros_all.
      assert (1 \in bn_agent A \- \{0}). autofs. omega.
      rewrite H in H6; autofs.
    destruct H as [A' [Haa' HxA']]. subst.
    pick_fresh_V V y. forwards*: H4 y. forwards*: H5 y.
    assert (H6:= H2).
    assert (is_proc (open 0 y (open 1 x (mapV f P)))).
      repeat (rewrite <- mapV_open). auto with hopi.
    rewrite <- (is_proc_mapN (open 0 y (open 1 x (mapV f P))) (permut 1)) in H6; auto with hopi.
    rewrite <- (is_agent_amapN (open_agent 0 y (open_agent 1 x A')) (permut 1)) in H6;
      auto with hopi.
    do 2 (rewrite mapN_open in H6; auto using permut_injective).
    do 2 (rewrite <- amapN_open in H6; auto using permut_injective).
    rewrite× @open_open in H6; try (simpl_permut; omega).
    rewrite× @open_agent_open_agent in H6; try (simpl_permut; omega).
    ∃ (new (new (amapN (permut 1) A'))).
    split.
    + apply (lts_new (L\uL1)); eauto. intros. simpl.
      apply (lts_new' (L \u L1 \u \{y})) with (open_agent 1 x0 (amapN (permut 1) A')); eauto.
      intros. rewrite mapV_mapN.
      forwards× HltsA': lts_rename H6 x1.
        do 2 (rewrite <- mapN_open; auto using permut_injective).
        rewrite is_proc_mapN; rewrite open_open; auto.
        autofnF.
        intros_all. apply fn_agent_open_sub in H12.
        rewrite fn_agent_amapN in H12. autofs.
      replace (permut 1 1) with 0 in HltsA' by simpl_permut.
      rewrite open_open in HltsA'; try solve [simpl_permut].
      rewrite open_agent_open_agent in HltsA'; try solve [simpl_permut].
      forwards× HltsA'': lts_rename HltsA' x0.
         replace 0 with (permut 1 1) at 3 by simpl_permut.
         do 2 (rewrite <- mapN_open; auto using permut_injective).
         rewrite is_proc_mapN; rewrite× @open_open; apply is_proc_rename with x;
         rewrite× @open_open in H7.
         autofnF.
         intros_all; apply fn_agent_open_sub in H12.
          rewrite fn_agent_amapN in H12. autofs.
      replace (permut 1 0) with 1 in HltsA'' by simpl_permut.
      rewrite (subst_lab_id _ x x1) in HltsA''; try solve [autofs].
      rewrite subst_lab_id in HltsA''; try solve [autofs]. rewrite× @open_open.
      rewrite× open_agent_open_agent.
      apply new_open_agent.
    + rewrite new_open_agent in H3.
      forwards*: open_agent_injective H3.
      rewrite× fn_agent_new.
      subst; apply sc_nu_nu_permut.
  -
    inverts Hlts. inverts HprocP. inverts HprocQ. pick_fresh_V V x.
    forwards*: H0 x. forwards*: H1 x. forwards*: H2 x.
    simpl in ×. inverts H. inverts H3. forwards*: decomp_agent_gen A 1 x.
      pick_fresh y.
      assert (is_agent (open_agent 0 y A)).
      forwards*: H8 y.
      forwards: lts_is_proc H; auto with hopi. forwards*: H5 y.
      do 2 (rewrite <- mapV_open). auto with hopi.
      apply is_agent_bn in H. rewrite bn_agent_open in H. intros_all.
      assert (1 \in bn_agent A \- \{0}). autofs. omega.
      rewrite H in H7; autofs.
    destruct H as [A' [Haa' HxA']]. subst. inverts H4.
    pick_fresh_V V y. forwards*: H3 y. forwards*: H5 y.
    forwards*: H8 y.
    replace 1 with ((permut 1) 0) in H7 at 1 by simpl_permut.
    replace 0 with ((permut 1) 1) in H7 at 1 by simpl_permut.
    rewrite mapV_mapN in H7.
    do 2 (rewrite <- mapN_open in H7; auto using permut_injective).
    rewrite× @open_open in H7.
    rewrite× @open_agent_open_agent in H7.
    assert (is_proc (open 0 x (open 1 y (mapV f P)))).
      repeat (rewrite <- mapV_open). apply is_proc_mapV.
      apply is_proc_rename with y. rewrite× @open_open.
      apply is_proc_rename with x. rewrite× @open_open.
    rewrite× @is_proc_mapN in H7.
    rewrite <- (is_agent_amapN (open_agent 1 x (open_agent 0 y A')) (permut 1)) in H7;
      auto with hopi.
    do 2 (rewrite <- amapN_open in H7; auto using permut_injective).
    ∃ (new (new (amapN (permut 1) A'))).
    split.
    + apply (lts_new (L\uL1)); eauto. intros. simpl.
      apply (lts_new' (L \u L1 \u \{y})) with (open_agent 1 x0 (amapN (permut 1) A')); eauto.
      intros.
      replace (permut 1 1) with 0 in H7 by simpl_permut.
      replace (permut 1 0) with 1 in H7 by simpl_permut.
      forwards× HltsA': lts_rename H7 x1.
        autofnF.
        intros_all. apply fn_agent_open_sub in H14.
        rewrite fn_agent_amapN in H14. autofs.
      rewrite× @open_open in HltsA'.
      rewrite× open_agent_open_agent in HltsA'.
      forwards× HltsA'': lts_rename HltsA' x0.
        rewrite× @open_open.
        apply is_proc_rename with x. auto.
        autofnF.
        intros_all. apply (fn_agent_open_sub _ 0 x1) in H14.
        rewrite fn_agent_amapN in H14. autofs.
      rewrite (subst_lab_id _ x x1) in HltsA''; try solve [autofs].
      rewrite subst_lab_id in HltsA''; try solve [autofs]. rewrite× @open_open.
      rewrite× open_agent_open_agent.
      apply new_open_agent.
    + rewrite new_open_agent in H6.
      forwards*: open_agent_injective H6.
      rewrite× fn_agent_new.
      subst; apply sc_nu_nu_permut.
  - simpl in Hlts; inversion Hlts.
  - simpl in Hlts; inversion Hlts.
  -
    inverts HprocP. inverts HprocQ. inversion Hlts; subst.
    +
      forwards: IHHstruct1 A0 H7; auto. destruct H as [ A' [ Hq HAA' ]].
      ∃ (parl A' (mapV f Q')).
      split. eapply lts_parl'; eauto.
      destruct A0; destruct A'; inversion HAA'; subst.
      × apply st_proc. auto with sc.
      × apply st_abs. intros. forwards: H6 C; auto. destruct C as [ k R S ]; simpl.
        destruct a; destruct a0; simpl. repeat (rewrite <- (mapV_mapN _ _ (@VS _))).
        repeat (rewrite subst_shift).
        apply sc_trans with (genNu k (subst ((shiftN k) p) R // S) // (mapV f P')).
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S) // shiftN k (mapV f P'))); eauto with sc.
        apply sc_trans with (genNu k (subst ((shiftN k) p0) R // S) // (mapV f Q')); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p0) R // S) // shiftN k (mapV f Q'))); eauto with sc.
      × apply st_conc. intros; forwards: H6 F; auto. destruct F as [ R ]; simpl.
        destruct c; destruct c0; simpl; simpl in H2.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0) // shiftN n (mapV f P'))); auto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2) // shiftN n0 (mapV f Q'))); auto with sc.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0)) // mapV f P'); auto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2)) // mapV f Q'); auto with sc.
    +
      forwards: IHHstruct2 A0 H7; auto. destruct H as [ A' [ Hq HAA' ]].
      ∃ (parr (mapV f Q) A').
      split. eapply lts_parr'; eauto.
      destruct A0; destruct A'; inversion HAA'; subst.
      × apply st_proc. auto with sc.
      × apply st_abs. intros. forwards: H6 C; auto. destruct C as [ k R S ]; simpl.
        destruct a; destruct a0; simpl. simpl in H2. repeat (rewrite <- (mapV_mapN _ _ (@VS _))).
        repeat (rewrite subst_shift). simpl in H5.
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S) // (shiftN k) (mapV f P))); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p0) R // S) // (shiftN k) (mapV f Q))); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S)) // (mapV f P)); eauto with sc.
      × apply st_conc. intros. forwards: H6 F; auto. destruct F as [ R ]; simpl.
        destruct c; destruct c0; simpl. simpl in H0.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0) // (shiftN n) (mapV f P))); eauto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2) // (shiftN n0) (mapV f Q))); eauto with sc.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0)) // (mapV f P)); eauto with sc.
    +
      forwards: IHHstruct1 H5; auto. destruct H as [ A' [ Hq HAA' ]].
      forwards: IHHstruct2 H8; auto. destruct H as [ A'' [ Hq' HAA'' ]].
      assert (Hbla:=Hq'). apply lts_inp_abs in Hq'. destruct Hq' as [ F' ]; subst.
      assert (Hbla':=Hq). apply lts_out_conc in Hq. destruct Hq as [ C' ]; subst.
      ∃ (ag_proc (appl C' F')).
      split. eapply lts_taul'; eauto.
      apply st_proc. inversion HAA'; subst. Opaque is_agent. forwards: H7 F; auto with hopi.
      inversion HAA''; subst. forwards: H10 C'; auto with hopi.
         eapply lts_conc_wf; eauto.
      apply sc_trans with (appr F C). apply sc_appr_appl.
      apply sc_trans with (appr F' C'); eauto with sc. apply sc_appr_appl.
    +
      forwards: IHHstruct1 f H5; auto. destruct H as [ A' [ Hq HAA' ]].
      forwards: IHHstruct2 H8; auto. destruct H as [ A'' [ Hq' HAA'' ]].
      assert (Hbla:=Hq'). apply lts_out_conc in Hq'. destruct Hq' as [ C' ]; subst.
      assert (Hbla':=Hq). apply lts_inp_abs in Hq. destruct Hq as [ F' ]; subst.
      ∃ (ag_proc (appr F' C')).
      split. eapply lts_taur'; eauto.
      apply st_proc. inversion HAA'; subst. forwards: H7 C; auto with hopi.
        eapply lts_conc_wf; eauto.
      inversion HAA''; subst. forwards: H10 F'; auto with hopi. eauto with sc.
  -
    inversion Hlts; subst. ∃ (ag_abs (abs_def (mapV (incV_map f) Q))).
    simpl; split; auto with hopi.
    apply st_abs; intros [k R S] H H'; simpl. apply sc_genNu. apply sc_par;
      auto using (shiftN_injective k) with sc.
  -
    inversion Hlts; subst. ∃ (ag_conc (conc_def 0 (mapV f Q) (mapV f Q'))).
    simpl; split; auto with hopi.
    apply st_conc. intros [ R] H. simpl. apply sc_par; auto with sc. apply sc_bind; auto with sc.
    intros [ |]; simpl; auto with sc.
  -
    simpl in Hlts. inverts Hlts; subst.
    inverts HprocP. inverts HprocQ. pick_fresh_V V x.
    forwards*: H0 x f (mapV f (open 0 x P)).
      rewrite× @mapV_open.
    destruct H1 as [ A' [HltsA' HAA'] ]. rewrite mapV_open in HltsA'.
    forwards*: lts_open HltsA'.
      forwards*: H4 x. rewrite <- mapV_open; auto with hopi.
      autofnF.
    destruct H1 as [A'' [Ha'a'' [HxA'' HltsA'']]].
    ∃ (new A''). split.
    + simpl. apply (lts_new' L) with A''; auto.
      intros. forwards: HltsA'' x0.
      rewrite× subst_lab_id in H6.
    + destruct A'' as [ P2 | [P2] | [n2 P2 P2'] ]; destruct A' as [P3 | [P3] | [n3 P3 P3']];
        simpl in *; inverts Ha'a'';
      destruct A0 as [ P1 | [P1] | [n1 P1 P1'] ]; inverts HAA'; simpl.
      × apply st_proc. apply sc_nu'. eapply sc_open_rev; eauto.
        intros_all. autofnF.
      × apply st_abs. intros. rename H5 into HwfC.
        apply sc_trans with (nu (appr (abs_def P1) C)). remember (abs_def P1) as F.
        asserts_rewrite (abs_def (nu P1) = abs_new F). subst. auto.
        apply× sc_newF_C.
        apply sc_trans with (nu (appr (abs_def P2) C)). apply sc_nu'. intros.
        forwards*: decomp_agent (ag_conc C) 1 x.
        destruct H5 as [A' [Hca' Hxa']].
        destruct A' as [ | []|[]]; inverts Hca'.
        pick_fresh_fset_V V (fn P1 \u fn P2 \u fn p \u fn p0) z.
        forwards: H7 (conc_def n (open (S n) z p) (open (S n) z p0)).
          Transparent is_agent. simpl. intros. apply H1.
          autobnF.
          intros_all. forwards*: HwfC k. autobnF.
        assert (∀ P1, (appr (abs_def (open 0 x P1))
              (conc_def n (open (S n) z p) (open (S n) z p0))=
        open 0 x (appr (abs_def P1)(conc_def n (open (S n) z p) (open (S n) z p0))))).
          intros. forwards*: (appr_open (open (S n) z p)(open (S n) z p0) P0 n 0) x.
          asserts_rewrite (open n x (open (S n) z p0) = open (S n) z p0) in H6.
            apply open_id. intros_all. forwards*: H1 n. autobnF. omega.
          asserts_rewrite (open n x (open (S n) z p) = open (S n) z p) in H6.
            apply open_id. intros_all. forwards*: H1 n. autobnF. omega.
          simpl. rewrite× H6.
        rewrite (H6 P1), (H6 P2) in H5.
        apply sc_open_rev in H5; try solve [intros_all; autofnF].
        clear H6.
        assert (∀ P1 z, 1 \notin bn P1 →
            genNu n (subst ((shiftN n) P1) (open (S n) z p) // open (S n) z p0) =
            open 1 z (appr (abs_def P1)(conc_def n p p0))).
          intros. forwards*: (appr_open p p0 P0 n 1) z0.
          asserts_rewrite (open 1 z0 P0 = P0) in H8. apply× @open_id.
          rewrite× H8.
        assert (bn P1 \c \{ 0}).
          forwards*: lts_is_proc (H2 x). rewrite <- mapV_open; auto with hopi.
          apply is_proc_bn in H8. rewrite bn_open in H8. intros_all.
          destruct (classic (x0 = 0)); autobnF.
          assert (x0 \in bn P1 \- \{ 0}). autobnF. rewrite H8 in H17; autobnF.
        assert (bn P2 \c \{ 0}).
          forwards*: lts_is_proc HltsA'. rewrite <- mapV_open; auto with hopi.
          apply is_proc_bn in H9. rewrite bn_open in H9. intros_all.
          destruct (classic (x0 = 0)); autobnF.
          assert (x0 \in bn P2 \- \{ 0}). autobnF. rewrite H9 in H18; autobnF.
        simpl in H5. rewrite (H6 P1), (H6 P2) in H5; try solve [autobnF].
        apply sc_open_rev in H5; try solve [autofnF].
        simpl. rewrite (H6 P1 x); try solve [autobnF].
        rewrite (H6 P2 x); try solve [autobnF]. apply× @sc_open.
        apply sc_symmetric. remember (abs_def P2) as F'.
        asserts_rewrite (abs_def (nu P2) = abs_new F'). subst. auto.
        apply× sc_newF_C.
      × apply st_conc. intros.
        assert (∀ k, k \in (bn P2 \u bn P2') → k ≤ n2).
          forwards*: lts_is_proc HltsA'. rewrite <- mapV_open; auto with hopi.
          intros. destruct× (classic (k = n2)). omega.
          forwards*: H5 k. autobnF; rewrite notin_singleton; autobnF. omega.
        assert (∀ k, k \in (bn P1 \u bn P1') → k ≤ n1).
          forwards*: lts_is_proc (H2 x). rewrite <- mapV_open; auto with hopi.
          intros. destruct× (classic (k = n1)). omega.
          forwards*: H6 k. autobnF; rewrite notin_singleton; autobnF. omega.
        apply sc_trans with (nu (appr F (conc_def n1 P1 P1'))). apply× sc_F_newC.
        apply sc_trans with (nu (appr F (conc_def n2 P2 P2'))). apply sc_nu'.
        forwards*: decomp_agent (ag_abs F) 1 x.
        destruct H8 as [A' [Hca' Hxa']].
        destruct A' as [ | []|[]]; inverts Hca'.
        pick_fresh_fset_V Empty_set (fn p) z.
        forwards*: H7 (abs_def (open 1 z p)).
          eapply is_proc_rename; eauto.
        assert (∀ P1 P1' n, (appr (abs_def (open 1 z p))
               (conc_def n (open n x P1) (open n x P1'))=
                open 0 x (appr (abs_def (open 1 z p))(conc_def n P1 P1')))).
          intros. forwards*: (appr_open P0 P1'0 (open 1 z p) n 0) x.
          asserts_rewrite (open 0 x (open 1 z p) = open 1 z p) in H9.
            apply open_id. autobnF. forwards*: @is_proc_bn H1.
            rewrite bn_open in H15. assert (0 \in bn p \- \{1 }). autobnF.
            rewrite H15 in H35. autobnF.
          simpl. rewrite× H9.
        fold (appr (abs_def (open 1 z p))((conc_def n1 (open n1 x P1) (open n1 x P1')))) in H8.
        rewrite (H9 P1 P1') in H8.
        fold (appr (abs_def (open 1 z p))((conc_def n2 (open n2 x P2) (open n2 x P2')))) in H8.
        rewrite (H9 P2 P2') in H8.
        apply sc_open_rev in H8; try solve [autofnF].
        clear H9.
        assert (∀ P1 P1' z n, (S n) \notin bn P1 \u bn P1' →
                genNu n (subst ((shiftN n)(open 1 z p)) P1 // P1') =
                open 1 z (appr (abs_def p)(conc_def n P1 P1'))).
          intros. forwards*: (appr_open P0 P1'0 p n 1) z0.
          asserts_rewrite (open (S n) z0 P0 = P0) in H10.
            apply open_id. autobnF.
          asserts_rewrite (open (S n) z0 P1'0 = P1'0) in H10.
            apply open_id. autobnF.
          rewrite× H10.
        simpl in H8. assert (S n2 \notin bn P2 \u bn P2').
          intros_all. forwards*:H5 (S n2). omega.
        assert (S n1 \notin bn P1 \u bn P1').
          intros_all. forwards*:H6 (S n1). omega.
        rewrite (H9 P1 P1'), (H9 P2 P2') in H8; auto.
        apply sc_open_rev in H8; try solve [autofnF].
        simpl. rewrite× (H9 P1 P1' x). rewrite× (H9 P2 P2' x). apply× @sc_open.
      apply sc_symmetric. apply× sc_F_newC.
  -
    edestruct IHHstruct1 as [A1 [HltsA1 HAA1]]; eauto. eapply is_proc_sc; eauto.
    edestruct IHHstruct2 as [A2 [HltsA2 HAA2]]; eauto. eapply is_proc_sc; eauto.
    ∃ A2. split; auto.
    eapply sim_test_trans; eauto.
    intros P' Q' R' Hpq Hqr; eapply sc_trans; eauto.
Qed.

Inductive sc0 : binary proc0 :=
| sc0_def : ∀ P Q, is_proc P → is_proc Q → struct_congr P Q → sc0 P Q.

Hint Constructors sc0:sc.

Lemma struct_congr_sim: simulation sc0.
Proof.
  apply late_implies_sim.
  split. intros_all. inverts H. intuition.
  intros P Q Hstruct.
  replace Q with (mapV (fun x ⇒ x) Q) by (apply mapV_id).
  replace P with (mapV (fun x ⇒ x) P) by (apply mapV_id).
  intros; inverts Hstruct. forwards: @struct_congr_sim'; eauto.
  destruct H3 as [A']. ∃ A'; intuition. Opaque is_agent.
  destruct A; destruct A'; inverts H5; simpl in *;
    auto with bisim sc hopi.
Qed.

Lemma struct_congr_bisim: bisimulation sc0.
Proof.
  apply sim_sym_imply_bisim.
  apply struct_congr_sim.
  intros_all. inverts H. auto with sc.
Qed.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | [ H1: struct_congr P ?Q,
      H2: is_proc ?Q |- _ ] ⇒ forwards: @is_proc_sc H1; auto with sc
  | [ H1: struct_congr ?Q P,
      H2: is_proc ?Q |- _ ] ⇒ forwards: @is_proc_sc H1; auto with sc
  end:sc.

Lemma sc0_trans : trans sc0.
Proof.
  intros_all. inverts H0. inverts H. apply sc0_def; eauto with hopi sc.
Qed.

Lemma sc0_sym : sym sc0.
Proof.
  intros_all. inverts H. apply sc0_def; eauto with hopi sc.
Qed.

Lemma sc0_refl : ∀ P, is_proc P → sc0 P P.
Proof.
  intros_all. auto with sc.
Qed.

Lemma oe_sc0 : ∀ Rel, Rincl sc0 Rel → Rincl sc0 (open_extension Rel).
Proof.
  intros_all. apply× oe_proc0.
Qed.

Hint Resolve sc0_trans sc0_sym:sc.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | H1: sc0 P ?Q |- _ ⇒ inverts H1
  | H1: sc0 ?Q P |- _ ⇒ inverts H1
  end:sc.