Require Export Syntax.

Inductive label : Set :=
| out : name → label
| inp : name → label
| tau : label
.

Definition fn_lab (l:label) :=
  match l with
  | tau ⇒ \{}
  | out a ⇒ \{a}
  | inp a ⇒ \{a}
  end.

Definition down_lab (l:label) :=
  match l with
  | tau ⇒ tau
  | out a ⇒ out (a-1)
  | inp a ⇒ inp (a-1)
  end.

Inductive abs : Set :=
| abs_def : proc1 → abs
.

Definition asubst (F : abs) (P : proc0) : proc0 :=
  match F with
  | abs_def Q ⇒ subst Q P
  end.

Inductive conc : Set :=
| conc_def : nat → proc0 → proc0 → conc
.

Inductive agent :=
| ag_proc : proc0 → agent
| ag_abs : abs → agent
| ag_conc : conc → agent
.

Coercion ag_abs : abs >-> agent.
Coercion ag_conc : conc >-> agent.

Tactic Notation "destructA" constr(A) := destruct A as [|[]|[]].

Definition fn_agent A := match A with
| ag_proc P ⇒ fn P
| ag_abs F ⇒ match F with | abs_def P ⇒ fn P end
| ag_conc C ⇒ match C with | conc_def n P Q ⇒
    map (fun k ⇒ k-n) (filter (fun k ⇒ leb n k) (fn P \u fn Q)) end
 end.

Definition conc_wf C := match C with
| conc_def n P Q ⇒ ∀ k, k < n → k \in fn P
end.

Definition fmapN f F :=
  match F with | abs_def P ⇒ abs_def (mapN f P) end.

Definition cmapN f C :=
  match C with | conc_def n P Q ⇒ conc_def n (mapN (liftN f n) P)(mapN (liftN f n) Q) end.

Definition amapN f A := match A with
| ag_proc P ⇒ ag_proc (mapN f P)
| ag_abs F ⇒ fmapN f F
| ag_conc C ⇒ cmapN f C
end.

Definition conc_parl C P : conc :=
  match C with
  | conc_def k P' Q ⇒ conc_def k P' (Q // (shiftN k P))
  end.

Definition conc_parr P C : conc :=
  match C with
  | conc_def k P' Q ⇒ conc_def k P' ((shiftN k P) // Q)
  end.

Definition abs_parl F P : abs :=
  match F with
  | abs_def Q ⇒ abs_def (Q // (shiftV P))
  end.

Definition abs_parr P F : abs :=
  match F with
  | abs_def Q ⇒ abs_def ((shiftV P) // Q)
  end.

Definition parl A P : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_parl F P)
  | ag_proc P' ⇒ ag_proc (P' // P)
  | ag_conc C ⇒ ag_conc (conc_parl C P)
  end.

Definition parr P A : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_parr P F)
  | ag_proc P' ⇒ ag_proc (P // P')
  | ag_conc C ⇒ ag_conc (conc_parr P C)
  end.

Definition down k x := If (x ≤ k) then x else x-1.

Tactic Notation "simpl_down" := unfold down in *; intros_all; default_simp; intuition.

Tactic Notation "simpl_name" := unfold liftN, down, permut in *; default_simp; intuition.

Definition conc_new (C:conc) : conc :=
  match C with
  | conc_def k P Q ⇒ If k \in fn P then conc_def (S k) P Q
                                     else conc_def k (mapN (down k) P) (nu (mapN (permut k) Q))
  end.

Definition abs_new (F:abs) : abs :=
  match F with
  | abs_def P ⇒ abs_def (nu P)
  end.

Definition new (A: agent) : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_new F)
  | ag_proc P ⇒ ag_proc (nu P)
  | ag_conc C ⇒ ag_conc (conc_new C)
  end.

Fixpoint genNu {V:Set} k (P:proc V) :=
  match k with
  | 0 ⇒ P
  | S k' ⇒ nu (genNu k' P)
  end.

Lemma nu_genNu {V:Set}: ∀ (P:proc V) n, nu (genNu n P) = genNu n (nu P).
Proof.
  induction n; simpl; auto.
  intros; rewrite× <- IHn.
Qed.

Definition fshiftN k F := match F with
  | abs_def P ⇒ abs_def (shiftN k P)
  end.

Definition appr F C : proc0 :=
  match C with
  | conc_def k P Q ⇒ genNu k (asubst (fshiftN k F) P // Q)
  end.

Definition appl C F : proc0 :=
  match C with
  | conc_def k P Q ⇒ genNu k (Q // asubst (fshiftN k F) P)
  end.

Inductive lts: proc0 → label → agent → Prop :=
| lts_out : ∀ a P Q, lts (a !(P) Q) (out a) (ag_conc (conc_def 0 P Q))
| lts_inp : ∀ a P, lts (a ? P) (inp a) (ag_abs (abs_def P))
| lts_parl : ∀ P Q l A, lts P l A → lts (P // Q) l (parl A Q)
| lts_parr : ∀ P Q l A, lts P l A → lts (Q // P) l (parr Q A)
| lts_new : ∀ P l A, 0 \notin fn_lab l → lts P l A →
    lts (nu P)(down_lab l)(new A)
| lts_taul : ∀ P Q a F C, lts P (out a) (ag_conc C) →
    lts Q (inp a) (ag_abs F) → lts (P // Q) tau (ag_proc (appl C F))
| lts_taur : ∀ P Q a F C, lts Q (inp a) (ag_abs F) →
    lts P (out a) (ag_conc C) → lts (Q // P) tau (ag_proc (appr F C))
.

Hint Constructors lts:hopi.

Lemma lts_parl' : ∀ P Q l A A', lts P l A → parl A Q = A' → lts (P // Q) l A'.
Proof.
  intros; subst; eapply lts_parl; eassumption.
Qed.

Lemma lts_parr' : ∀ P Q l A A', lts P l A → parr Q A = A' → lts (Q // P) l A'.
Proof.
  intros; subst; eapply lts_parr; eassumption.
Qed.

Lemma lts_taul' : ∀ P A' Q a F C,
    lts P (out a) (ag_conc C) → lts Q (inp a) (ag_abs F) →
    ag_proc (appl C F) = A' → lts (P // Q) tau A'.
Proof.
  intros. subst. eapply lts_taul; eassumption.
Qed.

Lemma lts_taur' : ∀ P A' Q a F C,
    lts P (out a) (ag_conc C) → lts Q (inp a) (ag_abs F) →
    ag_proc (appr F C) = A' → lts (Q // P) tau A'.
Proof.
  intros; subst; eapply lts_taur; eassumption.
Qed.

Lemma lts_new' : ∀ P l l' A A', 0 \notin fn_lab l → lts P l A →
    new A = A' → l' = down_lab l → lts (nu P) l' A'.
Proof.
  intros; subst; eapply lts_new; eassumption.
Qed.

Hint Resolve lts_parl' lts_parr' lts_taul' lts_taur':hopi.

Lemma lts_tau_proc: ∀ P A, lts P tau A → ∃ P', A = ag_proc P'.
Proof.
  introv Hlts. remember tau as l.
  induction Hlts; try (inverts Heql; eauto); try (destruct l; inverts H1);
    try (destruct IHHlts; try reflexivity; subst; eexists; simpl; reflexivity).
Qed.

Lemma lts_inp_abs : ∀ P a A, lts P (inp a) A → ∃ F, A = ag_abs F.
Proof.
  introv Hlts. remember (inp a) as l. gen a.
  induction Hlts; introv Heql; try (inverts Heql; eauto); try (destruct l; inverts H1);
    try (edestruct IHHlts; try reflexivity; subst; eexists; simpl; auto).
Qed.

Lemma lts_out_conc : ∀ P a A, lts P (out a) A → ∃ C, A = ag_conc C.
Proof.
  intros P a A Hlts. remember (out a) as l. gen a.
  induction Hlts; introv Heql; try (inverts Heql; eauto); try (destruct l; inverts H1);
    try (edestruct IHHlts; try reflexivity; subst; eexists; simpl; auto).
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.

Lemma genNu_fold {V:Set} : ∀ (P:proc V) k, genNu k (nu P) = genNu (S k) P.
Proof.
   intros; induction k; simpl; auto. rewrite <- nu_genNu. auto.
Qed.

Lemma fn_genNu {V:Set}: ∀ (P:proc V) n, fn (genNu n P) [=] map (fun k ⇒ k-n) (filter (fun k ⇒ leb n k) (fn P)).
Proof.
  induction n; simpl.
  - asserts_rewrite ((fun k ⇒ k-0) = fun k ⇒ k). extens; intros; omega.
    rewrite map_id. rewrite filter_id. fsetdec.
  - split; intros. simplfs; ∃ (S(a+ n)); split; try omega. apply IHn in H. simplfs. assert (x = S(a + n)) by omega.
    subst. intuition.
    simplfs. apply IHn. destruct x; intuition. simplfs. ∃ (S(a+n)). intuition. simplfs. intuition.
    assert (x = a+n) by omega. rewrite H2 in H0; auto.
Qed.

Hint Rewrite @fn_genNu:fs.

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. forwards:IHlts. reflexivity.
    case_if; intros_all.
    destruct (classic (k = n)); try (subst; auto).
    forwards*: H1 k. omega.
    forwards*: H1 k. rewrite fn_mapN. apply map_spec. ∃ k; intuition. simpl_down.
Qed.

Lemma mapN_concwf : ∀ f C, conc_wf C ↔ conc_wf (cmapN f C).
Proof.
  split; intros; destruct C as [n P Q]; intros_all.
  - forwards*: H. simplfs. ∃ k; intuition. simpl_liftN.
  - forwards*: H. simplfs. simpl_liftN.
Qed.

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

Lemma mapN_eq_on_fn_rev {V:Set} : ∀ (P:proc V) f g, mapN g P = mapN f P
        → ∀ n, n \in fn P → g n = f n.
Proof.
  induction P; simpl; intros; try fsetdec.
  - simplfs. destruct H0. rewrite singleton_iff in H0. subst. inverts H. auto.
    forwards*: IHP f g. inverts H. auto.
  - simplfs. destruct H0. rewrite singleton_iff in H0. subst. inverts H; auto.
    destruct H0; [forwards*: IHP1 f g | forwards*: IHP2 f g]; inverts H; auto.
  - simplfs. destruct H0; [forwards*: IHP1 f g | forwards*: IHP2 f g]; inverts H; auto.
  - forwards*: IHP (liftN f 1)(liftN g 1)(S n). inverts H; auto. simplfs.
    simpl_liftN. rewrite <- minus_n_O in H. auto.
Qed.

Lemma amapN_amapN : ∀ f g A, amapN f (amapN g A) = amapN (fun x ⇒ f (g x)) A.
Proof.
  intros; destructA A; simpl; rewrite mapN_mapN; auto.
    rewrite mapN_mapN; repeat fequals; extens; intros; simpl_liftN;
    replace (n + g (x1 - n) - n) with (g(x1-n)) by omega; auto.
Qed.

Lemma amapN_id : ∀ A, amapN (fun x ⇒ x) A = A.
Proof.
  intros; destructA A; simpl; try (rewrite mapN_id'; auto).
   asserts_rewrite (liftN (fun x : nat ⇒ x) n = fun x⇒ x). extens; simpl_liftN.
   repeat (rewrite mapN_id'); auto.
Qed.

Lemma amapN_eq_on_fn : ∀ A f g,
  (∀ k, k \in fn_agent A → f k = g k) → amapN f A = amapN g A.
Proof.
  intros; destructA A; simpl in ×.
  - fequals; apply mapN_eq_on_fn; auto.
  - do 2 fequals; apply mapN_eq_on_fn; auto.
  - do 2 fequals; apply mapN_eq_on_fn; intros; simpl_liftN; rewrite H; auto; simplfs; ∃ k; intuition;
     simplfs; intuition.
Qed.

Lemma fn_agent_amapN : ∀ A (f : nat → nat), fn_agent (amapN f A) [=] map f (fn_agent A).
Proof.
  intros; destructA A; simpl; try solve [rewrite× @fn_mapN; fsetdec].
  split; intros.
  - simplfs. destruct H0; simplfs;
    (simpl_liftN; try solve [omega]; ∃ (x0 -n); split; try omega; apply map_spec; ∃ x0; split; auto; simplfs; intuition).
  - simplfs. subst.
    ∃ (f (x0-n) + n). split; try omega. apply filter_iff; simplfs; auto with hopi. split; try omega.
    destruct H1; [ left | right ]; ∃ x0; split; simpl_liftN.
Qed.

Lemma amapN_subset : ∀ f A A', fn_agent A \c fn_agent A' → fn_agent (amapN f A) \c fn_agent (amapN f A').
Proof.
  intros. do 2 rewrite fn_agent_amapN. apply× map_subset.
Qed.

Lemma fn_agent_new : ∀ A, fn_agent (new A) [=] downfs (fn_agent A \- \{0}).
Proof.
  intros; destructA A; simpl; try fsetdec.
  case_if.
  - split; intros.
    × simplfs. ∃ x. destruct H0; split; try omega; simplfs; intuition.
    × simplfs. ∃ x. destruct H0; split; try omega; simplfs; intuition.
  - split; intros.
    × simplfs. ∃ (S x). split; try omega. destruct H0. simplfs. intuition.
        left. simpl_down. subst. assert (x0=n) by omega. subst. fsetdec.
        subst. replace (S (x0 -1)) with x0 by omega. auto.
        simpl in H0. simplfs. intuition. simpl_permut.
    × simplfs. ∃ (x-1). split; try omega. simplfs. destruct H0; intuition.
        left. ∃ x; simpl_down; intuition.
        right. simpl. simplfs. ∃ x; simpl_permut. intuition.
Qed.

Lemma fn_appr_appl : ∀ F C, fn (appr F C) [=] fn (appl C F).
Proof.
  intros. destruct F as []; destruct C as [].
    split; simpl; do 2 rewrite fn_genNu; simpl; apply map_subset; apply filter_subset; fsetdec.
Qed.

Lemma fn_C_par {V:Set}: ∀ (n:nat) E (Q:proc V), map (fun k : nat ⇒ k - n)
    (filter (fun k : nat ⇒ n <=? k) (E \u fn ((shiftN n) Q)))
    [=] map (fun k : nat ⇒ k - n)
      (filter (fun k : nat ⇒ n <=? k) E) \u fn Q.
Proof.
  intros_all. simplfs; intuition.
  - destruct_hyps. simplfs. intuition. left. ∃ x. intuition. simplfs.
    destruct_hyps. assert (x0=a) by omega. substs. intuition.
  - destruct_hyps. simplfs. ∃ x. intuition. simplfs.
  - ∃ (n+a). intuition. simplfs. intuition. right. ∃ a; intuition.
Qed.

Lemma fn_appr_subset : ∀ F C, fn (appr F C) \c fn_agent C \u fn_agent F.
Proof.
  intros. destruct F as []; destruct C as [].
    simpl; simplfs; intuition.
    apply subset_trans with (map (fun k : nat ⇒ k - n)
      (filter (fun k : nat ⇒ n <=? k) (((fn p0 \u fn p1) \u fn((shiftN n) p))))).
    apply map_subset. apply filter_subset. simpl. eapply subset_trans. apply union_s_m. apply fn_subst.
    apply Subset_refl. fsetdec. rewrite fn_C_par. fsetdec.
Qed.

Lemma fn_parl: ∀ A P, fn_agent (parl A P) [=] fn_agent A \u fn P.
Proof.
  intros. destructA A; simpl. fsetdec. simplfs. fsetdec.
  asserts_rewrite ((filter (fun k : nat ⇒ n <=? k)(fn p \u fn p0 \u fn ((shiftN n) P))) [=] filter (fun k : nat ⇒ n <=? k)
      ((fn p \u fn p0) \u fn ((shiftN n) P))). apply IndexSetProperties.Dec.F.filter_equal; auto with fs. fsetdec.
  rewrite fn_C_par. fsetdec.
Qed.

Lemma fn_parr: ∀ A P, fn_agent (parr P A) [=] fn_agent A \u fn P.
Proof.
  intros. destructA A; simpl. fsetdec. simplfs. fsetdec.
  asserts_rewrite ((filter (fun k : nat ⇒ n <=? k)(fn p \u fn ((shiftN n) P) \u fn p0)) [=] filter (fun k : nat ⇒ n <=? k)
      ((fn p \u fn p0) \u fn ((shiftN n) P))). apply IndexSetProperties.Dec.F.filter_equal; auto with fs. fsetdec.
  rewrite fn_C_par. fsetdec.
Qed.

Lemma lts_fn : ∀ P l A, lts P l A → fn_agent A \c fn P.
Proof.
  intros. induction H; simpl in *; try fsetdec.
  - asserts_rewrite ((fun k ⇒ k-0) = fun k ⇒ k). extens; intros; omega.
    rewrite map_id. rewrite filter_id. fsetdec.
  - rewrite fn_parl; fsetdec.
  - rewrite fn_parr; fsetdec.
  - rewrite fn_agent_new. intros_all. simplfs.
  - eapply subset_trans. rewrite <- fn_appr_appl. apply fn_appr_subset. fsetdec.
  - eapply subset_trans. apply fn_appr_subset. fsetdec.
Qed.

Definition lmapN f l :=
  match l with
  | out n ⇒ out (f n)
  | inp n ⇒ inp (f n)
  | _ ⇒ l
  end.

Lemma amapN_new : ∀ f A, amapN f (new A) = new (amapN (liftN f 1) A).
Proof.
  intros; destructA A; simpl; auto.
  repeat (case_if; simpl).
  + repeat (rewrite mapN_mapN). repeat (rewrite liftN_liftN). auto.
  + false. repeat (rewrite liftN_liftN in *). simpl_liftN. apply C0. simplfs.
    ∃ n. intuition; case_if; omega.
  + false. repeat (rewrite liftN_liftN in *). simpl_liftN. apply C. simplfs.
    intuition; case_if; omega.
  + repeat (rewrite mapN_mapN). repeat (rewrite liftN_liftN in *). do 2 fequals. apply mapN_eq_on_fn. intros.
    simpl_name. assert (k=n) by omega. substs. fsetdec. replace (k-1-n) with (k-S n) by omega. omega.
    repeat fequals. extens. intros; simpl_name. replace (x1 - (n + 1)) with (x1 - S n) by omega. omega.
Qed.

Lemma shiftN_mapN {V:Set} : ∀ (P:proc V) f n, (shiftN n)(mapN f P) = mapN (liftN f n) (shiftN n P).
Proof.
   intros. repeat (rewrite mapN_mapN).
   apply mapN_eq_on_fn.
   intros. simpl_liftN. replace (n+k-n) with k by omega. auto.
Qed.

Lemma mapN_appl : ∀ f F C, appl (cmapN f C) (fmapN f F) = mapN f (appl C F).
Proof.
   intros. destruct F; subst. destruct C; simpl.
   rewrite mapN_genNu. simpl.
   replace (subst ((shiftN n) (mapN f p)) (mapN (liftN f n) p0))
            with (mapN (liftN f n) (subst ((shiftN n) p) p0)); auto.
   simpl. rewrite subst_mapN. rewrite shiftN_mapN. auto.
Qed.

Lemma mapN_appr : ∀ f F C, appr (fmapN f F) (cmapN f C) = mapN f (appr F C).
Proof.
  intros. destruct F; subst. destruct C; simpl.
  rewrite mapN_genNu. simpl.
  replace (subst ((shiftN n) (mapN f p)) (mapN (liftN f n) p0))
            with (mapN (liftN f n) (subst ((shiftN n) p) p0)); auto.
  simpl. rewrite subst_mapN. rewrite shiftN_mapN. auto.
Qed.

Lemma amapN_parl: ∀ f A P, parl (amapN f A) (mapN f P) = amapN f (parl A P).
Proof.
 intros; destructA A; auto; simpl.
 - rewrite× @mapV_mapN.
 - rewrite× @shiftN_mapN.
Qed.

Lemma amapN_parr: ∀ f A P, parr (mapN f P) (amapN f A) = amapN f (parr P A).
Proof.
 intros; destructA A; auto; simpl.
 - rewrite× @mapV_mapN.
 - rewrite× @shiftN_mapN.
Qed.

Lemma mapN_lts : ∀ P l A f, lts P l A → lts (mapN f P) (lmapN f l) (amapN f A).
Proof.
  introv Hlts. gen f.
  induction Hlts; intros f; simpl; eauto with hopi.
  - rewrite liftN_0. auto with hopi.
  - eapply lts_parl'; eauto. destructA A; simpl; auto.
    rewrite× @mapV_mapN. do 2 rewrite mapN_mapN. repeat fequals. extens. simpl_liftN.
    replace (n+x1-n) with x1 by omega. omega.
  - eapply lts_parr'; eauto. destructA A; simpl; auto.
    rewrite× @mapV_mapN. do 2 rewrite mapN_mapN. repeat fequals. extens. simpl_liftN.
    replace (n+x1-n) with x1 by omega. omega.
  - rewrite amapN_new. forwards: IHHlts (liftN f 1).
    eapply lts_new'; auto; destruct l; simpl_liftN; destruct n; try omega; rewrite singleton_iff in *; omega.
  - eapply lts_taul'; eauto. rewrite× mapN_appl.
  - eapply lts_taur'; eauto. rewrite× mapN_appr.
Qed.

Lemma mapN_lts_rev : ∀ P l A f, lts (mapN f P) l A →
    injective f → (∃ A' l', A = amapN f A' ∧ lts P l' A' ∧ l = lmapN f l').
Proof.
  introv Hlts. remember (mapN f P) as P'. gen P f.
  induction Hlts; introv Hp' Hf; destruct P0; inverts Hp'.
  - ∃ (ag_conc (conc_def 0 P0_1 P0_2)) (out n).
    intuition; eauto. simpl. rewrite liftN_0. auto.
  - ∃ (ag_abs (abs_def P0)). eauto with hopi.
  - edestruct IHHlts as [A' [ l' [HA' [ HltsP Hl'] ]]]; eauto.
    ∃ (parl A' P0_2) l'. subst. split; auto with hopi. rewrite× amapN_parl.
  - edestruct IHHlts as [A' [ l' [HA' [ HltsP Hl'] ]]]; eauto.
    ∃ (parr P0_1 A') l'. subst. split; auto with hopi. rewrite× amapN_parr.
  -
    destruct (IHHlts _ _ eq_refl (liftN_preserves_injectivity f Hf 1)) as [A' [ l'0 [HA' [ HltsP Hl']]]].
    subst. ∃ (new A'). eexists; splits; [ rewrite× amapN_new | apply (lts_new _ l'0) | ];
    destruct l'0; simpl; try fsetdec; simpl_liftN; rewrite singleton_iff in *; omega.
  - edestruct IHHlts2 as [Ain [ lin [HAin [ HltsP2 Hlin] ]]]; eauto with hopi.
    destruct Ain; inverts HAin. destruct lin; inverts Hlin.
    edestruct IHHlts1 as [Aout [ lout [HAout [ HltsP1 Hlout] ]]]; eauto.
    destruct Aout; inverts HAout. destruct lout; inverts Hlout.
    apply Hf in H0; subst.
    ∃ (ag_proc (appl c a0)) tau. split; eauto with hopi. rewrite× mapN_appl.
  - edestruct IHHlts2 as [Ain [ lin [HAin [ HltsP2 Hlin] ]]]; eauto.
    destruct Ain; inverts HAin. destruct lin; inverts Hlin.
    edestruct IHHlts1 as [Aout [ lout [HAout [ HltsP1 Hlout] ]]]; eauto.
    destruct Aout; inverts HAout. destruct lout; inverts Hlout.
    apply Hf in H0; subst.
    ∃ (ag_proc (appr a c)) tau. split; eauto with hopi. rewrite× mapN_appr.
Qed.