Library HOC25Axiomatization

Require Import Relations.
Require Import Program.Wf.

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC18ONORbis.
Require Import HOC21Coinductive.
Require Import HOC22Decidability.
Require Import HOC23PrimeDecomposition.


Lemma wf_characterize_set : ∀ p : wfprocess,
  {T | p = wfp_Send (fst T) (snd T)} +
  {T | p = wfp_Abs (fst T) (fst (snd T)) (snd (snd T))} +
  {X | p = wfp_Gvar X} +
  {T | p = wfp_Par (fst T) (snd T)} +
  {p = wfp_Nil}.
Proof with (try rewrite_wfp_equal; automate).
  introv. destruct p; rename proc into p; rename wf_cond into Hwf.
  destruct p.
    repeat left.
    lets Hwf´ : wf_send Hwf.
    ∃ (c, (mkWfP p Hwf´))...

    do 3 left; right.
    lets Hyp : (Abs_from_Receive_spec c l p Hwf (@nil process)).
    ∃ (c, ((fst (Abs_from_Receive c l p Hwf (@nil process))), (snd (Abs_from_Receive c l p Hwf (@nil process)))))...

    false. inverts Hwf.

    do 2 left; right. ∃ v...

    left; right.
    lets Hwf1 : wf_par1 Hwf; lets Hwf2 : wf_par2 Hwf.
    ∃ ((mkWfP p1 Hwf1), (mkWfP p2 Hwf2))...

    right...
Qed.

Ltac destruct_wf_set q :=
  let T := fresh "T" in
  let p := fresh "p" in
  let a := fresh "a" in
  let X := fresh "X" in
  let p1 := fresh "p1" in
  let p2 := fresh "p2" in
  let Hyp := fresh "Hyp" in
  destruct (wf_characterize_set q) as
  [[[[[T Hyp] | [T Hyp]] | [X Hyp]] | [T Hyp]] | Hyp];
  [destruct T as [a p] |
   destruct T as [a [X p]] |
                           |
   destruct T as [p1 p2] | ]; simpls.

Lemma peano_induction_type :
  ∀ (P : nat → Type),
    (∀ n, (∀ m, m < n → P m) → P n) →
    (∀ n, P n).
Proof.
  introv H. cuts× K: (∀ n m, m < n → P m).
  nat_comp_to_peano.
  induction n; introv Le. false. inversion Le. apply H.
  intros. apply IHn. nat_math.
Qed.

Lemma measure_induction_set :
  ∀ (A:Type) (mu : A → nat) (P : A → Set),
    (∀ x, (∀ y, mu y < mu x → P y) → P x) →
    (∀ x, P x).
Proof.
  introv IH. intros x. gen_eq n: (mu x). gen x.
  induction n using peano_induction_type. introv Eq. subst×.
Qed.

Lemma wfp_ind_set : ∀ (P : wfprocess → Set),
  (∀ (a : chan) (p : wfprocess), P p → P (wfp_Send a p)) →
  (∀ (a : chan) (X : var) (p : wfprocess), P p → P (wfp_Abs a X p)) →
  (∀ X : var, P (wfp_Gvar X)) →
  (∀ p q : wfprocess, P p → P q → P (wfp_Par p q)) →
  P wfp_Nil →
    ∀ p : wfprocess, P p.
Proof with solve_wfp_size.
  introv HSend HAbs HGvar HPar HNil.
  induction p using (measure_induction_set _ wfp_size).
  destruct_wf_set p; substs¬.
    apply HSend; apply H...
    apply HAbs; apply H...
    apply HPar; apply H...
Qed.

Require Import HOC04DefLTS.
Require Import HOC24PreCompleteness.


Inductive norm_step : wfprocess → wfprocess → Prop :=
 | NCoreNil : ∀ a X n, n > 0 →
              norm_step
                (wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))))
                (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))
 | NCore : ∀ a X p n, n > 0 → wfp_sizeP p > 0 →
             norm_step
               (wfp_Abs a X (wfp_Par p
               (wfp_prod (wfp_repeat n (wfp_Abs a X p)))))
               (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))
 | NSend : ∀ p q a,
             norm_step p q →
               norm_step (wfp_Send a p) (wfp_Send a q)
 | NReceive : ∀ p q a X,
                norm_step p q →
                  norm_step (wfp_Abs a X p) (wfp_Abs a X q)
 | NParLeft : ∀ p q r,
                norm_step p q →
                  norm_step (wfp_Par p r) (wfp_Par q r)
 | NParRight : ∀ p q r,
                 norm_step p q →
                   norm_step (wfp_Par r p) (wfp_Par r q).

Definition norm_full := (clos_trans wfprocess norm_step).

Infix "--->" := norm_step (at level 60).
Infix "--->*" := norm_full (at level 60).

Definition ext_cgr_step := up_to wfcgr norm_full.
Definition ext_cgr_full := (clos_trans wfprocess ext_cgr_step).

Infix "-≡->" := ext_cgr_step (at level 60).
Infix "-≡->*" := ext_cgr_full (at level 60).


Instance trans_norm_full : Transitive norm_full.
Proof with automate.
  introv Ht1. inductions Ht1...
    introv Ht1.
      eapply t_trans.
      constructor. eassumption. eassumption.
Qed.

Lemma norm_full_send : ∀ p q a, p --->* q → wfp_Send a p --->* wfp_Send a q.
Proof.
  introv Ht. inductions Ht. repeat constructor×.
  etransitivity; eassumption.
Qed.

Lemma norm_full_abs : ∀ p q a X, p --->* q → wfp_Abs a X p --->* wfp_Abs a X q.
Proof.
  introv Ht. inductions Ht. repeat constructor×.
  etransitivity; eassumption.
Qed.

Lemma norm_full_par_l : ∀ p q r, p --->* q → wfp_sizeP r > 0 → wfp_Par p (remove_par_nils r) --->* wfp_Par q (remove_par_nils r).
Proof.
  introv Ht.
  inductions Ht. repeat constructor×.
  introv Hyp. etransitivity; jauto.
Qed.

Lemma norm_full_par_r : ∀ p q r, p --->* q → wfp_sizeP r > 0 → wfp_Par (remove_par_nils r) p --->* wfp_Par (remove_par_nils r) q.
Proof.
  introv Ht.
  inductions Ht. introv Hr. constructor. applys¬ NParRight.
  etransitivity; jauto.
Qed.

Lemma norm_step_sizeP : ∀ p q, p ---> q → wfp_sizeP p ≠ 0 ∧ wfp_sizeP q ≠ 0.
Proof with automate.
  introv Ht. inductions Ht; splits...
  + inductions n; simpls...
  + inductions n; simpls...
Qed.

Lemma norm_full_sizeP : ∀ p q, p --->* q → wfp_sizeP p ≠ 0 ∧ wfp_sizeP q ≠ 0.
Proof with automate.
  introv Ht. inductions Ht...
  applys¬ norm_step_sizeP.
Qed.

Lemma norm_step_sizeP_eq : ∀ p q, p ---> q → wfp_sizeP p = wfp_sizeP q.
Proof with automate.
  introv Ht. inductions Ht...

  gen a X. induction n using (lt_wf_ind).
  destruct n. nat_math.
  clear H. destruct n. introv. simpls...
  introv; repeat rewrite wfp_prod_repeat_SS.
  repeat (try rewrite wfp_sizeP_abs; try rewrite wfp_sizeP_par)...

  gen a X. induction n using (lt_wf_ind).
  destruct n. nat_math.
  clear H. remember (remove_par_nils p) as q. clear Heqq.
  destruct n; introv. simpls...
  introv; repeat rewrite wfp_prod_repeat_SS.
  repeat (try rewrite wfp_sizeP_abs; try rewrite wfp_sizeP_par)...
Qed.

Lemma norm_full_sizeP_eq : ∀ p q, p --->* q → wfp_sizeP p = wfp_sizeP q.
Proof with automate.
  introv Hc; inductions Hc...
  applys¬ norm_step_sizeP_eq.
Qed.

Instance trans_ext_cgr_full : Transitive ext_cgr_full.
Proof with automate.
  introv Ht1 Ht2.
    eapply t_trans; eassumption.
Qed.


Inductive R_io_nf : binary wfprocess :=
 | io_nf_base_nil : ∀ n a X, n > 0 → R_io_nf (wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil)))) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))
 | io_nf_base : ∀ n p a X, n > 0 → R_io_nf (wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat n (wfp_Abs a X p))))) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))
 | io_nf_sym_base : ∀ n p a X, n > 0 → R_io_nf (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) (wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat n (wfp_Abs a X p)))))
 | io_nf_sym_base_nil : ∀ n a X, n > 0 → R_io_nf (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) (wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))))
 | io_nf_cgr : ∀ p q, p ≡* q → R_io_nf p q.

Hint Resolve io_nf_base_nil io_nf_base io_nf_cgr io_nf_sym_base io_nf_sym_base_nil.

Lemma io_nf_no_out : ∀ n p a X a´ p´ p´´, n > 0 → {{(wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) -- LabOut a´ p´ ->> p´´}} → False.
Proof with automate.
  inductions n; introv Hyp; [nat_math | clear Hyp].
  simpl wfp_repeat. rewrite wfp_prod_cons.
  destruct n; introv Ht.
    simpls; inverts Ht... inverts H3. inverts H3.
    inverts Ht... inverts H3.
    simpls. eapply IHn. nat_math. eassumption.
Qed.

Lemma io_nf_no_rem : ∀ n p a X Y p´, n > 0 → {{(wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) -- LabRem Y ->> p´}} → False.
Proof with automate.
  inductions n; introv Hyp; [nat_math | clear Hyp].
  simpl wfp_repeat. rewrite wfp_prod_cons.
  destruct n; introv Ht.
    simpls; inverts Ht... inverts H3. inverts H3.
    inverts Ht... inverts H3.
    simpls. eapply IHn. nat_math. eassumption.
Qed.

Lemma R_io_nf_IObis : IO_bisimulation_full R_io_nf.
Proof with automate.
  splits; introv Hr; try introv Ht.
    inverts× Hr. symmetry in H; auto.

    inverts× Hr.
    {
      lets Hyp : wfp_trans_in_chan_eq Ht. subst a0.
      lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp.
        simpl wfp_repeat. simpl wfp_inst_Abs.
        destruct n; [nat_math | ].
        simpl wfp_repeat. repeat rewrite wfp_prod_cons.
        eexists. splits; introv. apply act1_in. constructor.
        remember (wfp_prod (wfp_Abs a X wfp_Nil :: wfp_repeat n (wfp_Abs a X wfp_Nil))) as q.
        simpl wfp_inst_Abs. rewrite_wfp_subst.
        assert (wfp_subst (wfp_Gvar X0) X q = q).
          subst q. clear. gen a X X0. inductions n; introv.
          simpl. rewrite¬ wfp_eq_subst_abs1.
          simpl wfp_repeat; rewrite wfp_prod_cons. rewrite_wfp_subst. fequals.
          rewrite¬ wfp_eq_subst_abs1.
        rewrite× H0. constructor.
        etransitivity. apply wfcgr_nil_l. apply wfcgr_par_com.

        destruct H0 as (Y & HneqY & HfY & Heq); subst fp. simpl wfp_inst_Abs.
        destruct n; [nat_math | ].
        simpl wfp_repeat. repeat rewrite wfp_prod_cons.
        eexists. splits; introv. apply act1_in. constructor.
        remember (wfp_prod (wfp_Abs a X wfp_Nil :: wfp_repeat n (wfp_Abs a X wfp_Nil))) as q.
        simpl wfp_inst_Abs. rewrite <- wfp_subst_decomposition_g. rewrite_wfp_subst.
        assert (wfp_subst (wfp_Gvar X0) X q = q).
          subst q. clear. gen a X X0. inductions n; introv.
          simpl. rewrite¬ wfp_eq_subst_abs1.
          simpl wfp_repeat; rewrite wfp_prod_cons. rewrite_wfp_subst. fequals.
          rewrite¬ wfp_eq_subst_abs1.
        rewrite× H0. constructor.
        etransitivity. apply wfcgr_nil_l. apply wfcgr_par_com.
        clear Ht H HneqY X0. subst q. gen a X Y.
        destruct n; introv Hf; simpls¬.
     }

      lets Hyp : wfp_trans_in_chan_eq Ht. subst a0.
      lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp.
        simpl wfp_repeat. simpl wfp_inst_Abs.
        destruct n; [nat_math | ].
        simpl wfp_repeat. repeat rewrite wfp_prod_cons.
        eexists. splits; introv. apply act1_in. constructor.
        remember (wfp_prod (wfp_Abs a X p0 :: wfp_repeat n (wfp_Abs a X p0))) as q.
        simpl wfp_inst_Abs. rewrite_wfp_subst.
        assert (wfp_subst (wfp_Gvar X0) X q = q).
          subst q. clear. gen p0 a X X0. inductions n; introv.
          simpl. rewrite¬ wfp_eq_subst_abs1.
          simpl wfp_repeat; rewrite wfp_prod_cons. rewrite_wfp_subst. fequals.
          rewrite¬ wfp_eq_subst_abs1.
        rewrite× H0. repeat constructor.

        destruct H0 as (Y & HneqY & HfY & Heq); subst fp. simpl wfp_inst_Abs.
        destruct n; [nat_math | ].
        simpl wfp_repeat. repeat rewrite wfp_prod_cons.
        eexists. splits; introv. apply act1_in. constructor.
        remember (wfp_prod (wfp_Abs a X p0 :: wfp_repeat n (wfp_Abs a X p0))) as q.
        simpl wfp_inst_Abs. rewrite <- wfp_subst_decomposition_g. rewrite_wfp_subst.
        assert (wfp_subst (wfp_Gvar X0) X q = q).
          subst q. clear. gen p0 a X X0. inductions n; introv.
          simpl. rewrite¬ wfp_eq_subst_abs1.
          simpl wfp_repeat; rewrite wfp_prod_cons. rewrite_wfp_subst. fequals.
          rewrite¬ wfp_eq_subst_abs1.
        rewrite× H0. repeat constructor.
        clear Ht H HneqY X0. subst q. gen a p0 X Y.
        destruct n; introv Hf; simpls¬.

        rename p0 into p. gen p a a0 fp X H. destruct n; [nat_math | ].
        introv Ht _.
        assert (a0 = a).
          gen fp; inductions n; introv Ht.
            simpls. inverts Ht...
            destruct ap; inverts× H3; try solve [inverts¬ H2].
            destruct aq; inverts× H3; try solve [inverts¬ H2].

            simpls wfp_repeat. rewrite wfp_prod_cons in Ht. inverts Ht...
            destruct ap; inverts× H3; try solve [inverts¬ H2].
            destruct aq; inverts× H3.
        subst a0.
        eexists. splits. constructor. introv.
        rewrite wfp_prod_repeat_SS in Ht.
        remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
        inverts Ht. subst_wfp.
        remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
        destruct ap; inverts H3; rename a0 into fp.
        simpl wfp_inst_Abs. rewrite_wfp_subst.
        subst q. rewrite wfp_subst_X_prod_repeat_Abs.
        lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
          simpls¬. repeat constructor. destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          repeat constructor.

        subst_wfp. destruct aq; inverts H3; rename a0 into fp.
        destruct n.
          simpls... lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
          simpls¬. rewrite¬ wfp_eq_subst_abs1. do 2 constructor.
          apply WfCgrPar_com.
          destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          rewrite¬ wfp_eq_subst_abs1. do 2 constructor. apply WfCgrPar_com.
          rewrite wfp_prod_repeat_SS in ×.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
          simpl wfp_inst_Abs. rewrite_wfp_subst.
          rewrite¬ wfp_eq_subst_abs1. subst q. rewrite wfp_subst_X_prod_repeat_Abs. constructor.
          etransitivity. Focus 2. constructor. apply WfCgrPar_com.
          etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
          apply wfcgr_par. repeat constructor.
          etransitivity. Focus 2. constructor. apply WfCgrPar_com.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
          inverts H2. subst_wfp.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
          destruct ap; inverts H4.
          simpl. applys× wfcgr_par.
          lets Hyp : wfp_trans_in_abs_eq H3; inverts Hyp.
          simpls¬. repeat constructor. destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          repeat constructor. repeat constructor.
          subst_wfp. destruct aq; inverts H4; rename a0 into fp.
          gen p a X X0 fp. inductions n; introv Ht.
            simpls. lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp.
            simpls¬. constructor. apply WfCgrPar_com.
            destruct H as (Y & HneqY & HfY & Heq).
            subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
            constructor. apply WfCgrPar_com.

            rewrite wfp_prod_repeat_SS in ×.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
            inverts Ht. subst_wfp.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q.
            destruct ap; inverts H3.
            lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
            simpl. etransitivity. Focus 2. constructor. apply WfCgrPar_com.
            etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
            apply wfcgr_par. repeat constructor.
            constructor. apply WfCgrPar_com.
            destruct H as (Y & HneqY & HfY & Heq).
            subst a0; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
            simpl. etransitivity. Focus 2. constructor. apply WfCgrPar_com.
            etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
            apply wfcgr_par. repeat constructor.
            constructor. apply WfCgrPar_com.

            subst_wfp.
            destruct aq; inverts H3; rename a0 into fp.
            specializes IHn X0 H2. clear H2.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) as q. clear Heqq.
            simpls. etransitivity. Focus 2. constructor. apply WfCgrPar_com.
            etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
            apply wfcgr_par. repeat constructor. etransitivity. Focus 2.
            constructor. apply WfCgrPar_com. auto.

        gen a a0 fp X H. destruct n; [nat_math | ].
        introv Ht _.
        assert (a0 = a).
          gen fp; inductions n; introv Ht.
            simpls. inverts Ht...
            destruct ap; inverts× H3; try solve [inverts¬ H2].
            destruct aq; inverts× H3; try solve [inverts¬ H2].

            simpls wfp_repeat. rewrite wfp_prod_cons in Ht. inverts Ht...
            destruct ap; inverts× H3; try solve [inverts¬ H2].
            destruct aq; inverts× H3.
        subst a0.
        eexists. splits. constructor. introv.
        rewrite wfp_prod_repeat_SS in Ht.
        remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
        inverts Ht. subst_wfp.
        assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal; subst; clear H.
        remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
        destruct ap; inverts H3; rename a0 into fp.
        simpl wfp_inst_Abs. rewrite_wfp_subst.
        subst q. rewrite wfp_subst_X_prod_repeat_Abs.
        lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
          simpl wfp_inst_Abs. constructor. rewrite_wfp_subst.
          etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.
          destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          constructor. rewrite_wfp_subst.
          etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.

        subst_wfp. destruct aq; inverts H3; rename a0 into fp.
        destruct n.
          simpls... lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
          simpls¬. rewrite¬ wfp_eq_subst_abs1. do 2 constructor. rewrite_wfp_subst.
          apply WfCgrPar_nil2.
          destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          rewrite¬ wfp_eq_subst_abs1. do 2 constructor. rewrite_wfp_subst.
          apply WfCgrPar_nil2.
          assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal. subst; clear H.
          rewrite wfp_prod_repeat_SS in ×.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
          simpl wfp_inst_Abs. rewrite_wfp_subst.
          rewrite¬ wfp_eq_subst_abs1. subst q. rewrite wfp_subst_X_prod_repeat_Abs. constructor.
          apply wfcgr_par. reflexivity.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
          inverts H2. subst_wfp.
          assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal. subst; clear H.
          remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
          destruct ap; inverts H4. simpl.
          lets Hyp : wfp_trans_in_abs_eq H3; inverts Hyp.
          simpl. rewrite_wfp_subst.
          etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.
          destruct H as (Y & HneqY & HfY & Heq).
          subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
          rewrite_wfp_subst. etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.

          destruct aq; inverts H4; rename a0 into fp; subst_wfp.
          assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal. subst; clear H.
          gen a X X0 fp. inductions n; introv Ht.
            simpls. lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp.
            simpls¬. rewrite_wfp_subst. apply wfcgr_nil_r.
            destruct H as (Y & HneqY & HfY & Heq).
            subst; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
            rewrite_wfp_subst. apply wfcgr_nil_r.

            rewrite wfp_prod_repeat_SS in ×.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
            inverts Ht. subst_wfp.
            assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal. subst; clear H.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q.
            destruct ap; inverts H3.
            lets Hyp : wfp_trans_in_abs_eq H2; inverts Hyp.
            simpl. rewrite_wfp_subst. apply wfcgr_par. reflexivity.
            etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.
            destruct H as (Y & HneqY & HfY & Heq).
            subst a0; simpls wfp_inst_Abs. rewrite× <- wfp_subst_decomposition_g.
            rewrite_wfp_subst. apply wfcgr_par. reflexivity.
            etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.

            subst_wfp.
            assert (p = wfp_Abs a X wfp_Nil) by rewrite_wfp_equal. subst; clear H.
            destruct aq; inverts H3; rename a0 into fp.
            specializes IHn X0 H2. clear H2.
            remember (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) as q. clear Heqq.
            simpls. apply wfcgr_par. reflexivity. jauto.

        lets Hyp : congr_in_strong H Ht.
        destruct Hyp as (fq & Htq & Hrq). ∃ fq; splits×.

    inverts× Hr. inverts Ht. inverts Ht.
    apply io_nf_no_out in Ht; intuition. apply io_nf_no_out in Ht; intuition.

    lets Hyp : congr_out H Ht.
    destruct Hyp as (q´ & q´´ & Htq & Hrq´ & Hrq´´). ∃ q´ q´´; splits×.

    inverts× Hr. inverts Ht. inverts Ht.
    apply io_nf_no_rem in Ht; intuition. apply io_nf_no_rem in Ht; intuition.
    lets Hyp : congr_rem H Ht.
    destruct Hyp as (q´ & Htq & Hrq´). ∃ q´; splits×.
Qed.

Lemma io_norm_step : ∀ p q, p ---> q → p ≈ q.
Proof.
  introv Ht; inductions Ht.

  ∃ R_io_nf; splits×.
  lets (Hs & Hi & Ho & Hv) : R_io_nf_IObis.
  splits×. applys¬ in_full_forall.

  ∃ R_io_nf; splits×.
  lets (Hs & Hi & Ho & Hv) : R_io_nf_IObis.
  splits×. applys¬ in_full_forall.

  applys¬ IObis_congr_send.
  applys¬ IObis_congr_abs.
  applys¬ IObis_congr_par.
  applys¬ IObis_congr_par.
Qed.

Lemma io_norm_full : ∀ p q, p --->* q → p ≈ q.
Proof.
  introv Ht; inductions Ht.
    applys¬ io_norm_step.
    etransitivity; eassumption.
Qed.

Lemma io_extcgr_step : ∀ p q, p -≡-> q → p ≈ q.
Proof.
  introv Ht. inverts Ht...
  destruct H as (p´ & q´ & Hc1 & Hc2 & Hnorm).
  etransitivity. Focus 2. etransitivity.
  apply io_norm_full. eassumption.
    ∃ wfcgr; splits~; apply congr_IObisimulation.
    ∃ wfcgr; splits~; apply congr_IObisimulation.
Qed.

Lemma io_extcgr_full : ∀ p q, p -≡->* q → p ≈ q.
Proof.
  introv Ht; inductions Ht.
    applys¬ io_extcgr_step.
    etransitivity; eassumption.
Qed.


Lemma has_free_par_nil_par : ∀ p q, has_free_par_nil (wfp_Par p q) ↔
  p = wfp_Nil ∨ q = wfp_Nil ∨ has_free_par_nil p ∨ has_free_par_nil q.
Proof.
  simpls; introv; repeat rewrite_wfp_equal; intuition.
Qed.


Inductive normal_form : wfprocess → Prop :=
 | nf_Send : ∀ p, normal_form p → ∀ a, normal_form (wfp_Send a p)
 | nf_Abs : ∀ p a X, normal_form p → (∀ n, n > 0 → ∀ q, ¬ (p ≡* (wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q)))))) → normal_form (wfp_Abs a X p)
 | nf_Gvar : ∀ X, normal_form (wfp_Gvar X)
 | nf_Par : ∀ p q, wfp_sizeP p > 0 → wfp_sizeP q > 0 → normal_form p → normal_form q → normal_form (wfp_Par p q)
 | nf_Nil : normal_form wfp_Nil.

Lemma nf_swap_invariant : ∀ (p : wfprocess) (X Y : var),
   normal_form (wfp_swap X Y p) ↔ normal_form p.
Proof with automate.
induction p using (measure_induction wfp_size).
introv. splits. Focus 2.
destruct_wf p; introv Hnf...
  inverts Hnf. constructor. rewrite H...
  Focus 2. repeat cases_if*; constructor.
  Focus 2. constructor; simpls; inverts Hnf; try rewrite H...
    rewrite¬ wfp_sizeP_swap. rewrite¬ wfp_sizeP_swap.

  rename p0 into p; rename X0 into Z.
  inverts Hnf.

  assert (Heq : wfp_Abs a X0 p0 = wfp_Abs a Z p).
    rewrite wfprocess_eq; simpls; unfold Abs.
    rewrite H1 in ×. rewrite¬ H3. clear H1 H3.
    rewrite wfp_Abs_equal in Heq.
    destruct Heq as (_ & Heq). cases_if×.
    subst. constructor. rewrite¬ H...
    introv Hn Hc. specializes H4 Hn.
    apply congr_swap with (X := X) (Y := Y) in Hc...
    rewrite wfp_swap_involutive in Hc. rewrite wfp_prod_repeat_swap in Hc.
    rewrite wfp_eq_swap_abs in Hc. rewrite swap_gvar_involutive in Hc.
    applys¬ H4...

    destruct Heq as (Heqp0 & Hfx0).
    rewrite wfp_gfresh_subst_is_swap in Heqp0; auto.
    subst p0. constructor. rewrite H... rewrite H in H2...
    rename n into Hneq_X0_Z. introv Hn Hc; specializes H4 Hn.
    apply congr_swap with (X := X) (Y := Y) in Hc...
    rewrite wfp_swap_involutive in Hc. rewrite wfp_prod_repeat_swap in Hc.
    rewrite wfp_eq_swap_abs in Hc. rewrite swap_gvar_involutive in Hc.
    apply congr_swap with (X := Z) (Y := X0) in Hc...
    rewrite wfp_prod_repeat_swap in Hc. rewrite wfp_eq_swap_abs in Hc.
    rewrite swap_gvar_left in Hc. applys¬ H4...

  destruct_wf p; introv Hnf...
    constructor. eapply H...
    inverts Hnf...
    assert (p = wfp_swap X Y p0) by rewrite_wfp_equal. substs×.
    Focus 2. constructor.
    Focus 2. inverts Hnf.
      assert (p = wfp_swap X Y p1) by rewrite_wfp_equal. substs×.
      assert (q = wfp_swap X Y p2) by rewrite_wfp_equal. substs×.
      constructor; try (rewrite <- wfp_swap_nil_eq in *; auto); try eapply H...
      rewrite¬ wfp_sizeP_swap in H2. rewrite¬ wfp_sizeP_swap in H3.

  rename p0 into p; rename X0 into Z.
  inverts Hnf.

  assert (Heq : wfp_Abs a X0 p0 = wfp_Abs a ({{X, Y}}Z) (wfp_swap X Y p)).
    rewrite wfprocess_eq; simpls; unfold Abs.
    rewrite H1 in ×. rewrite¬ H3. clear H1 H3.
    rewrite wfp_Abs_equal in Heq.
    destruct Heq as (_ & Heq). cases_if×.
    subst. constructor. rewrite¬ <- H...
    introv Hn Hc; specializes H4 Hn.

    apply congr_swap with (X := X) (Y := Y) in Hc...
    rewrite wfp_prod_repeat_swap in Hc. rewrite wfp_eq_swap_abs in Hc.
    applys¬ H4...

    destruct Heq as (Heqp0 & Hfx0).
    rewrite wfp_gfresh_subst_is_swap in Heqp0; auto.
    subst p0. constructor. rewrite H in H2... rewrite¬ H in H2...
    unfold wfp_size; simpl; rewrite size_swap. rewrite size_subst...
    rename n into Hneq_X0_XYZ. introv Hn Hc; specializes H4 Hn.
    apply congr_swap with (X := X) (Y := Y) in Hc...
    rewrite wfp_prod_repeat_swap in Hc. rewrite wfp_eq_swap_abs in Hc.
    apply congr_swap with (X := {{X, Y}}Z) (Y := X0) in Hc...
    rewrite wfp_prod_repeat_swap in Hc. rewrite wfp_eq_swap_abs in Hc.
    rewrite swap_gvar_left in Hc. applys¬ H4...
Qed.

Lemma nf_cannot_reduce_basic : ∀ p, normal_form p → ∀ q, ¬ (p --->* q).
Proof with automate.
  introv Hnf Ht. gen Hnf. inductions Ht; jauto.
  introv Hnf. inductions H.
    remember (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))) as r.
    inverts Hnf. clear H2; assert (wfp_Abs a X r = wfp_Abs a X0 p).
      rewrite wfprocess_eq; simpls. unfold Abs.
      rewrite H1. rewrite H1 in H3. rewrite¬ H3. clear H1 H3.
      lets H2 : H0. symmetry in H2.
      rewrite wfp_Abs_equal in H0. destruct H0 as (_ & H0).
      cases_if×. subst X0 r. eapply H4. eassumption.
      rewrite wfp_Abs_equal in H2. destruct H2 as (_ & H2).
      cases_if×. subst. etransitivity. apply wfcgr_nil_l. apply wfcgr_par_com.
      destruct H0 as (Heqr´ & HfX).
      rewrite Heqr in H2. rewrite Heqr´ in Heqr. clear Heqr´.
      assert (wfp_subst (wfp_Gvar X0) X (wfp_subst (wfp_Gvar X) X0 p) =
         (wfp_subst (wfp_Gvar X0) X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))))) by (rewrite¬ Heqr). clear Heqr.
      rewrite <- wfp_subst_decomposition_g in H0; auto.
      rewrite wfp_subst_gvar_idem in H0.
      specializes¬ H4 H. subst p.
      eapply H4... instantiate (1 := wfp_Nil).
      rewrite¬ wfp_prod_repeat_subst. rewrite wfp_eq_subst_abs1.
      assert (wfp_Abs a X wfp_Nil = wfp_Abs a X0 (wfp_subst (wfp_Gvar X0) X wfp_Nil)).
        rewrite_wfp_subst.
        rewrite wfp_Abs_equal. splits¬. cases_if×.
        rewrite_wfp_subst. splits×. fresh_solve.
      rewrite H0. rewrite_wfp_subst. etransitivity.
      apply wfcgr_nil_l. apply wfcgr_par_com.

    remember (wfp_Par p (wfp_prod (wfp_repeat n (wfp_Abs a X p)))) as r.
    clear H0; inverts Hnf.
      clear H2; assert (wfp_Abs a X r = wfp_Abs a X0 p0).
      rewrite wfprocess_eq; simpls. unfold Abs.
      rewrite H1. rewrite H1 in H3. rewrite¬ H3. clear H1 H3.
      lets H2 : H0. symmetry in H2.
      rewrite wfp_Abs_equal in H0. destruct H0 as (_ & H0).
      cases_if×. subst X0 p0 r. eapply H4. eassumption.
      constructor. apply WfCgrRefl.
      rewrite wfp_Abs_equal in H2. destruct H2 as (_ & H2).
      cases_if×. destruct H2 as (_ & H2).
      destruct H0 as (Heqr´ & HfX).
      rewrite Heqr in H2. rewrite Heqr´ in Heqr. clear Heqr´.
      assert (wfp_subst (wfp_Gvar X0) X (wfp_subst (wfp_Gvar X) X0 p0) =
         (wfp_subst (wfp_Gvar X0) X (wfp_Par p (wfp_prod (wfp_repeat n (wfp_Abs a X p)))))) by (rewrite¬ Heqr). clear Heqr.
      rewrite <- wfp_subst_decomposition_g in H0; auto.
      rewrite wfp_subst_gvar_idem in H0.
      specializes H4 H (wfp_subst (wfp_Gvar X0) X p). subst p0.
      apply H4... apply wfcgr_par. reflexivity.
      rewrite wfp_prod_repeat_subst. rewrite wfp_eq_subst_abs1.
      assert (wfp_Abs a X p = wfp_Abs a X0 (wfp_subst (wfp_Gvar X0) X p)).
        rewrite wfp_Abs_equal. splits¬. cases_if×.
        rewrite <- wfp_subst_decomposition_g. splits.
        rewrite¬ wfp_subst_gvar_idem. simpl; fresh_solve.
      simpls; rewrite gfresh_par_iff in ×. jauto.
      rewrite H0. repeat constructor. auto.

    inverts Hnf...

    inverts Hnf...
    assert (wfp_Abs a X p = wfp_Abs a X0 p0).
      rewrite wfprocess_eq; simpls. unfold Abs.
      rewrite H1. rewrite H1 in H3. rewrite¬ H3. clear H1 H3.
      lets H3 : H0. symmetry in H3.
      rewrite wfp_Abs_equal in H3. destruct H3 as (_ & H3).
      rewrite wfp_Abs_equal in H0. destruct H0 as (_ & H0).
      repeat cases_if×. destruct H0 as (Heqp & Hfx). destruct H3 as (Heqp0 & Hfx0).
      clear n; rename n0 into Hneq.
      subst p0. apply IHnorm_step.
      clear dependent q. clear H4 Heqp Hfx IHnorm_step a Hneq.
      rewrite wfp_gfresh_subst_is_swap in H2; auto.
      rewrite nf_swap_invariant in H2...

    inverts Hnf...

    inverts Hnf...
Qed.

Hint Resolve nf_Send nf_Abs nf_Gvar nf_Par nf_Nil.

Lemma nf_abs_eq : ∀ a X p, normal_form (wfp_Abs a X p) →
  normal_form p ∧ (∀ n, n > 0 → ∀ q, ¬ (p ≡* (wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q)))))).
Proof with automate.
  introv Hn; inverts Hn.
  assert (Heq : wfp_Abs a X0 p0 = wfp_Abs a X p).
    rewrite_wfp_equal. unfolds Abs. rewrite <- H0. rewrite¬ H2.
  clear H0 H2. symmetry in Heq. rewrite wfp_Abs_equal in Heq; destruct Heq as (_ & Heq).
  cases_if×. substs×. destruct Heq as (Heq & Hfx).
  rewrite wfp_gfresh_subst_is_swap in Heq; auto. subst p.
  splits. rewrite¬ nf_swap_invariant.
  intros m Hm q Hc.
  specializes H3 Hm. apply congr_swap with (X := X0) (Y := X) in Hc.
  rewrite wfp_swap_involutive in Hc... rewrite wfp_prod_repeat_swap in Hc.
  rewrite wfp_eq_swap_abs in Hc. unfolds swap_gvar; repeat cases_if×.
Qed.

Lemma nf_no_par_nil : ∀ p, normal_form p → ¬ has_free_par_nil p.
Proof with automate.
  induction p using (measure_induction wfp_size); destruct_wf p; introv Hyp; try solve [simpls~].
  + simpl. inverts Hyp... applys¬ H...
  + apply nf_abs_eq in Hyp. rewrite has_free_par_nil_abs. applys¬ H...
  + simpls; rew_logic. inverts Hyp; subst_wfp. splits*; try applys¬ H...
    introv Heq; subst... introv Heq; subst...
Qed.

Lemma nf_remove_nil_congr : ∀ p, normal_form (remove_par_nils p) →
  ∀ q, p ≡* q → normal_form (remove_par_nils q).
Proof with automate.
  introv Hp Hcgr. inductions Hcgr; jauto.
  inductions H; simpl_remove_par_nils; jauto.

  + constructor. inverts Hp...

  + apply nf_abs_eq in Hp. destruct Hp as (Hnfp & Hp).
    constructor; jauto.
    introv Hn Hcgr. clear IHwfcgr_step Hnfp. eapply Hp. eassumption.
    instantiate (1 := q0). etransitivity; try eassumption.
    constructor. applys¬ remove_nil_wfcgr_step.

  + assert (Hsp : wfp_sizeP p = wfp_sizeP p´).
      apply wfcgr_sizeP. constructor¬.
    assert (Hsq : wfp_sizeP q = wfp_sizeP q´).
      apply wfcgr_sizeP. constructor¬.
    repeat cases_if*; try solve [false; nat_math].

    inverts Hp... constructor×.
     - apply remove_nil_wfcgr_step in H.
       apply (t_step wfprocess wfcgr_step) in H. apply wfcgr_sizeP in H...
     - apply remove_nil_wfcgr_step in H0.
       apply (t_step wfprocess wfcgr_step) in H0. apply wfcgr_sizeP in H0...

  + repeat cases_if×.
  + repeat cases_if×.
    rewrite remove_par_nils_sizeP_0 in e. rewrite¬ e.

  + repeat cases_if×...
    - rewrite remove_par_nils_sizeP_0 in ×. rewrite¬ e0.
    - inverts Hp...

  + repeat cases_if×...
    inverts Hp... inverts H4... constructor...

  + repeat cases_if×...
    inverts Hp... inverts H3... constructor...
Qed.

Lemma nf_equiv_par_nil : ∀ p, normal_form p ↔ (¬ has_free_par_nil p ∧ normal_form (remove_par_nils p)).
Proof with automate.
  induction p using (measure_induction wfp_size);
  destruct_wf p; splits; introv Hyp.

  + inverts Hyp... simpl_remove_par_nils. specializes H p0.
    simpl; splits×. apply H... constructor. apply H...

  + constructor. rewrite H... splits×.
    inverts Hyp. simpl_remove_par_nils. inverts H1...

  + specializes H p0. rewrite has_free_par_nil_abs. simpl_remove_par_nils.
    apply nf_abs_eq in Hyp. splits×. apply H...
    constructor. apply H...
    introv Hn. inverts Hyp. specializes H1 Hn.
    introv Hyp. apply (H1 q). etransitivity.
    apply remove_par_nils_wfcgr. auto.

  + inverts Hyp. rewrite has_free_par_nil_abs in H0. simpl_remove_par_nils.
    apply nf_abs_eq in H1. constructor. applys H...
    inverts H1. introv Hn Hp0. eapply H3. eassumption.
    etransitivity. symmetry. apply remove_par_nils_wfcgr. eauto.

  + simpls; simpl_remove_par_nils; jauto.
  + simpls; simpl_remove_par_nils; jauto.

  + inverts Hyp... rewrite H in H4... rewrite H in H5...
    splits×. simpls. rew_logic; splits*; subst_wfp; rewrite¬ <- wfprocess_eq.
    introv Heq; subst... introv Heq; subst...
    simpl_remove_par_nils. repeat cases_if×...
    constructor*; rewrite remove_par_nils_sizeP in n, n0...

  + inverts Hyp. simpls; rew_logic in ×... destruct H0 as (Hp1 & Hp2 & Hfp1 & Hfp2);
    rewrite <- wfprocess_eq in ×. simpl_remove_par_nils; repeat cases_if×.
    false; apply Hfp1. applys¬ has_top_has_free_nil.
    clear Hfp1. clear dependent p2. induction p1 using (measure_induction wfp_size).
    destruct_wf p1; try solve [false; automate].
    tests : (p0 = wfp_Nil); simpl_has_top_nil; jauto.
    left. applys H...
    false; apply Hfp2. applys¬ has_top_has_free_nil.
    clear Hfp2. clear dependent p1. induction p2 using (measure_induction wfp_size).
    destruct_wf p2; try solve [false; automate].
    tests : (p0 = wfp_Nil); simpl_has_top_nil; jauto.
    right. applys H...
    inverts H1... constructor... rewrite H... rewrite H...

  + simpls; simpl_remove_par_nils; jauto.
  + constructor.
Qed.

Lemma nf_congr_invariant : ∀ p (q : wfprocess),
  p ≡* q → normal_form p → ¬ has_free_par_nil q → normal_form q.
Proof with automate.
  introv Hc Hnp Hnfq.
  rewrite nf_equiv_par_nil in *; splits¬.
  apply nf_remove_nil_congr in Hc; jauto.
Qed.

Lemma remove_par_nils_red : ∀ p q, p --->* q → remove_par_nils p --->* remove_par_nils q.
Proof with automate.
  introv Ht. inductions Ht...

  Focus 2. etransitivity; eassumption.

  gen y. induction x using (measure_induction wfp_size).
  introv Ht. inverts Ht; simpl_remove_par_nils.

  + repeat rewrite remove_par_nils_wfp_prod_repeat_abs.
    repeat constructor×.

  + repeat rewrite remove_par_nils_wfp_prod_repeat_abs.
    cases_if×. apply remove_par_nils_sizeP_0 in e. rewrite e. repeat constructor×.
    cases_if×. false. destruct n; try nat_math. destruct n; simpls...
    do 2 constructor×. rewrite <- remove_par_nils_sizeP. nat_math.

  + specializes H H0... applys¬ norm_full_send.

  + specializes H H0... applys¬ norm_full_abs.

  + specializes H H0... apply norm_step_sizeP in H0.
    repeat cases_if×... applys¬ norm_full_par_l...

  + specializes H H0... apply norm_step_sizeP in H0.
    repeat cases_if×... applys¬ norm_full_par_r...
Qed.

Lemma core_norm_full_send : ∀ a p q, p --->* q →
  (∀ p´, Core p = Some (wfp_Send a p´) →
     ∃ q´, Core q = Some (wfp_Send a q´) ∧ p´ --->* q´).
Proof with automate.
  introv Hred. inductions Hred; introv Hcore.

  + inductions H; try solve [false*].
    - simpl_core. inverts Hcore... ∃ q; splits×. constructor¬.
    - lets Hyp : norm_step_sizeP H. simpl_core; repeat cases_if×.
    - lets Hyp : norm_step_sizeP H. simpl_core; repeat cases_if×.

  + rewrite Hcore in ×. lets (q´ & Hcq´ & Hcgrq´) : IHHred1 p´...
    rewrite Hcq´ in ×. lets (q´´ & Hcq´´ & Hcgrq´´) : IHHred2 q´...
    ∃ q´´; splits×. etransitivity; eassumption.
Qed.

Lemma core_norm_full_gvar : ∀ p q, p --->* q →
  (∀ X, Core p = Some (wfp_Gvar X) → False).
Proof with automate.
  introv Hred; inductions Hred; introv Hcore; jauto.

  inductions H; simpl_core; try solve [inverts Hcore].
  cases_if×. lets Hyp : norm_step_sizeP H. nat_math.
  cases_if×. repeat cases_if×. lets Hyp : norm_step_sizeP H. nat_math.
Qed.

Lemma core_norm_full_none : ∀ p q, p --->* q →
  (Core p = None → Core q = None).
Proof with automate.
  introv Hred; inductions Hred; introv Hcore; jauto.

  inductions H; simpl_core; try solve [inverts Hcore].
  lets Hyp : norm_step_sizeP H. repeat cases_if×.
  lets Hyp : norm_step_sizeP H. repeat cases_if×.
Qed.

Lemma norm_step_abs_char : ∀ a X p q, wfp_Abs a X p ---> q →
  (∃ n, n > 0 ∧ p = wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))) ∨
  (∃ n, n > 0 ∧ ∃ q, p = wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q)))) ∨
  (∃ r, q = wfp_Abs a X r ∧ p ---> r).
Proof with automate.
  introv Ht; inverts Ht...
  + left. ∃ n; splits×.
    assert (wfp_Abs a X0 (wfp_prod (wfp_repeat n (wfp_Abs a X0 wfp_Nil))) = wfp_Abs a X p).
      rewrite_wfp_equal; unfold Abs. rewrite H2. rewrite¬ H1.
    symmetry in H; clear H1 H2.
    rewrite wfp_Abs_equal in H; inverts H; clear H0.
    cases_if*; substs... inverts H1.
    rewrite wfp_prod_repeat_subst... rewrite wfp_eq_subst_abs1. fequals. fequals.
    rewrite_wfp_equal.
  + rewrite remove_par_nils_sizeP in H4.
    right; left. ∃ n; splits×.
    assert (wfp_Abs a X0 (wfp_Par p0 (wfp_prod (wfp_repeat n (wfp_Abs a X0 p0)))) = wfp_Abs a X p).
    rewrite_wfp_equal. unfold Abs. simpls. rewrite H2. rewrite¬ H0.
    symmetry in H; clear H0 H2. rename p0 into q.
    rewrite wfp_Abs_equal in H; inverts H; clear H0.
    cases_if*; substs... inverts H1. ∃ (wfp_subst (wfp_Gvar X) X0 q).
      fequals. rewrite wfp_prod_repeat_subst... fequals. fequals.
      rewrite wfp_eq_subst_abs1. simpls. rewrite gfresh_par_iff in H0; inverts H0.
      clear H1. applys¬ wfp_Abs_eq.
  + right; right.
    assert (wfp_Abs a X0 p0 = wfp_Abs a X p).
      rewrite_wfp_equal. unfold Abs. rewrite H2. rewrite¬ H1.
    clear H1 H2. lets H´ : H; symmetry in H; rewrite wfp_Abs_equal in ×.
    inverts H. clear H0. inverts H´. clear H.
    repeat cases_if; substs...
    ∃ (wfp_subst (wfp_Gvar X) X0 q0). inverts H1; inverts H0. clear H H1.
    assert (X # q0). apply io_norm_step in H3. eapply gfresh_IObis; eassumption.
    splits. applys¬ wfp_Abs_eq.
    do 2 (rewrite× wfp_gfresh_subst_is_swap). rename X0 into Y.
    clear n n0 H2 H; gen X Y.
    inductions H3; intro Z; introv; rewrite_wfp_swap;
    repeat rewrite <- remove_par_nils_swap; try solve [constructor*; rewrite¬ wfp_sizeP_swap].
    - repeat rewrite wfp_prod_repeat_swap... constructor×.
    - repeat rewrite wfp_prod_repeat_swap... constructor×.
      rewrite¬ wfp_sizeP_swap.
Qed.

Lemma nf_cannot_reduce_lr : ∀ p, normal_form p → ∀ q, ¬ (p -≡->* q).
Proof with automate.
  introv Hnf Hred. inductions Hred...
  gen x y. induction x using (measure_induction wfp_size).
  destruct_wf x; introv Hnorm.

  + introv Ht. inverts Ht...
    destruct H0 as (p´ & q´ & Hc1 & Hc2 & Ht).
    lets (p´´ & Hcp´´ & Hcgrp´´) : send_core_wfcgr a Hc1 p.
      simpl_core; auto.
    lets (q´´ & Hcq´´ & Hcgrq´´) : core_norm_full_send Ht Hcp´´.
    lets (y´´ & Hcy´´ & Hcgry´´) : send_core_wfcgr a Hc2 Hcq´´.
    eapply (H p _ _ y´´)... clear H. inverts¬ Hnorm...
    constructor. ∃ p´´ q´´; splits×.

  + introv Ht. inverts Ht...
    destruct H0 as (p´ & q´ & Hc1 & Hc2 & Ht).
    apply nf_abs_eq in Hnorm. destruct Hnorm as (Hnfp & Hncgr).
    lets (p´´ & Hcp´´ & Hcgrp´´) : abs_core_wfcgr a Hc1 p X.
      simpl_core; auto.

    apply core_remove_par_nils in Hcp´´; simpl_remove_par_nils.

    assert (Hsp´´ : wfp_size (remove_par_nils p´´) < wfp_size (wfp_Abs a X p)).
      apply wfcgr_size_remove_nil in Hc1. rewrite Hcp´´ in Hc1.
      rewrite lt_peano. eapply Arith.Lt.lt_le_trans.
      Focus 2. apply remove_par_nils_size. rewrite Hc1.
      simpl_sizes. nat_math.

    assert (Hnfp´´ : normal_form (remove_par_nils p´´)).
      eapply nf_remove_nil_congr; try eassumption.
      rewrite nf_equiv_par_nil in Hnfp; jauto.

    specializes¬ H Hnfp´´.

    apply remove_par_nils_red in Ht. rewrite Hcp´´ in ×.

    assert (Hnr : ∀ n, n > 0 → ∀ q, ¬ (remove_par_nils p´´ ≡* wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q))))).
      introv Hn Hc. eapply Hncgr. eassumption.
      etransitivity. Focus 2. eassumption.
      etransitivity. eassumption. apply remove_par_nils_wfcgr.

    remember (remove_par_nils p´´) as r. remember (remove_par_nils q´) as q.
    gen Ht Hnr H. clear. introv Ht. assert (∃ q´, wfp_Abs a X r ---> q´).
      inductions Ht... clear Ht q.
    destruct H as (q & Ht). introv Hcgr Hred.
    apply norm_step_abs_char in Ht. inverts Ht as Ht.
    - destruct Ht as (n & Hn & Heqr). specializes Hcgr Hn; subst.
      apply (Hcgr wfp_Nil). etransitivity. apply wfcgr_nil_l.
      apply wfcgr_par_com.
    - inverts Ht as Ht.
      × destruct Ht as (n & Hn & r´ & Heq). specializes Hcgr Hn; subst.
        apply (Hcgr r´). reflexivity.
      × destruct Ht as (r´ & _ & Hr).
        apply (Hred r´). constructor.
        eexists. eexists. splits×.
        reflexivity. reflexivity. constructor¬.

  + introv Ht. inverts Ht...
    destruct H0 as (p´ & q´ & Hc1 & Hc2 & Ht).
    eapply core_norm_full_gvar. eassumption.
    instantiate (1 := X).
    eapply gvar_core_wfcgr. eassumption. simpl_core; auto.

  + lets Hnf : Hnorm. inverts Hnorm...
    assert (Hc : Core (wfp_Par p1 p2) = None).
      simpl_core. repeat cases_if×...
    introv Ht. inverts Ht...
    destruct H0 as (p´ & q´ & Hc1 & Hc2 & Ht).

    assert (Hcp´ : Core p´ = None).
      eapply none_core_wfcgr. eassumption. auto.
    rename p1 into p0; rename p2 into p1.
    lets (p2 & p3 & Heq23 & Hs2 & Hs3 & Hnp2 & Hnp3) : core_none_char Hcp´...
      apply wfcgr_sizeP in Hc1...

    assert (Hnfp23 : normal_form (wfp_Par p2 p3)).
      rewrite <- Heq23. eapply nf_remove_nil_congr; try eassumption.
      rewrite nf_equiv_par_nil in Hnf...

    inverts Hnfp23... clear H6 H7.

    assert (Hcsp2 : wfp_size p2 < wfp_size (wfp_Par p0 p1)).
      apply wfcgr_size_remove_nil in Hc1. rewrite Heq23 in Hc1.
      rewrite lt_peano. eapply Arith.Lt.lt_le_trans.
      Focus 2. apply remove_par_nils_size. rewrite Hc1...

    assert (Hcsp3 : wfp_size p3 < wfp_size (wfp_Par p0 p1)).
      apply wfcgr_size_remove_nil in Hc1. rewrite Heq23 in Hc1.
      rewrite lt_peano. eapply Arith.Lt.lt_le_trans.
      Focus 2. apply remove_par_nils_size. rewrite Hc1...

    apply remove_par_nils_red in Ht.
    rewrite Heq23 in ×. cut ((∃ p, p2 --->* p) ∨ (∃ p, p3 --->* p)).
      introv Hyp; inverts Hyp as Hyp; destruct Hyp.
      eapply H. apply Hcsp2. auto. constructor. eexists. eexists.
      splits. reflexivity. reflexivity. eassumption.
      eapply H. apply Hcsp3. auto. constructor. eexists. eexists.
      splits. reflexivity. reflexivity. eassumption.

    gen Ht Hs2 Hs3. clear. remember (remove_par_nils q´) as r.
    rename p2 into p; rename p3 into q; clear. introv Ht.
      inductions Ht. Focus 2. jauto.
      inverts H... intros; left. ∃ q0. constructor¬.
      intros; right. ∃ q0. constructor¬.

  + introv Ht. inverts Ht...
    destruct H0 as (p´ & q´ & Hc1 & Hc2 & Ht).
    apply norm_full_sizeP in Ht. apply wfcgr_sizeP in Hc1. automate.

Grab Existential Variables.
  inverts Hnorm... automate.
Qed.

Lemma par_nil_sizeP_not_0 : ∀ p, p ≠ wfp_Nil → ¬has_free_par_nil p → wfp_sizeP p > 0.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hneq Hfpn; simpls; try solve [solve_wfp_sizeP];
  try solve [intuition].

  clear Hneq. rew_logic in Hfpn... rewrite <- wfprocess_eq in ×.
  destruct Hfpn as (Hp1 & Hp2 & Hfp1 & Hfp2).
  simpl_sizes. cut (wfp_sizeP p1 > 0). nat_math.
  apply H...
Qed.

Lemma nf_cannot_reduce_rl : ∀ p,
  (∀ q, ¬ (p -≡->* q)) → ¬ has_free_par_nil p → normal_form p.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hnc Hfpn; try solve [constructor].
    constructor. apply H... introv Hc.
    apply Hnc with (q := wfp_Send a q). clear Hfpn.
    clear H Hnc; inductions Hc.
    inverts H. destruct H0 as (x´ & y´ & H1 & H2 & H3).
    repeat constructor. ∃ (wfp_Send a x´) (wfp_Send a y´).
    splits; try apply¬ wfcgr_send.
    clear H1 H2 y. clear dependent x. inductions H3...
      repeat constructor¬. etransitivity; eassumption.
      etransitivity; eassumption.

    Focus 2.
    simpls; rew_logic in ×... do 2 rewrite <- wfprocess_eq in Hfpn.
    constructor; try apply H...
    applys× par_nil_sizeP_not_0. applys× par_nil_sizeP_not_0.
    introv Hc. apply Hnc with (q := wfp_Par q p2).
    clear H Hnc. destruct Hfpn as (_ & Hp21 & _ & Hp22); induction Hc.
    inverts H. destruct H0 as (x´ & y´ & H1 & H2 & H3).
    repeat constructor. ∃ (wfp_Par x´ p2) (wfp_Par y´ p2).
    splits; try apply¬ wfcgr_par; try reflexivity.
    clear H1 H2. clear dependent x. inductions H3...
      repeat constructor¬.
      etransitivity; eassumption.
      etransitivity; eassumption.
    introv Hc. apply Hnc with (q := wfp_Par p1 q).
    clear H Hnc; destruct Hfpn as (Hp11 & _ & Hp12 & _); induction Hc.
    inverts H. destruct H0 as (x´ & y´ & H1 & H2 & H3).
    repeat constructor. ∃ (wfp_Par p1 x´) (wfp_Par p1 y´).
    splits; try apply¬ wfcgr_par; try reflexivity.
    clear H1 H2 y. clear dependent x. inductions H3...
      repeat constructor¬.
      etransitivity; eassumption.
      etransitivity; eassumption.

    constructor. Focus 2. introv Hn Hc.
    tests Ht : (wfp_sizeP q = 0).
    rewrite wfp_sizeP_0_wfcgr_nil in Ht.
    assert (p0 ≡* (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil)))).
      etransitivity. eassumption. etransitivity.
      apply wfcgr_par. eassumption. Focus 2.
      etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.
      gen Ht; clear. inductions n; intro Ht.
      simpls. reflexivity. destruct n. simpl. applys¬ wfcgr_abs.
      repeat rewrite wfp_prod_repeat_SS. applys¬ wfcgr_par.
      applys¬ wfcgr_abs.
      eapply Hnc. repeat constructor.
        eexists. eexists. splits.
        apply wfcgr_abs. apply H0.
        Focus 2. constructor. constructor. auto.
        reflexivity.

    eapply Hnc. repeat constructor.
    eexists. eexists. splits.
      apply wfcgr_abs. eassumption.
      Focus 2. constructor. constructor. auto. nat_math. reflexivity.

    apply H... introv Hc.
    apply Hnc with (q := wfp_Abs a X q).
    clear H Hnc Hfpn; induction Hc.
    inverts H. destruct H0 as (x´ & y´ & H1 & H2 & H3).
    repeat constructor.
    ∃ (wfp_Abs a X x´) (wfp_Abs a X y´).
    splits; try (apply¬ wfcgr_abs; repeat constructor).
    clear H1 H2 y. clear dependent x. inductions H3...
      repeat constructor¬. etransitivity; eassumption.
      etransitivity; eassumption.

    rewrite has_free_par_nil_abs in ×. auto.
Qed.

Lemma remove_par_nils_absorb : ∀ (p : wfprocess),
  ¬ has_free_par_nil p → remove_par_nils p = p.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; try rewrite has_free_par_nil_abs;
  simpls; introv Hnfp; simpl_remove_par_nils; jauto.
  + fequals. apply H...
  + fequals. apply H...
  + rew_logic in ×... do 2 rewrite <- wfprocess_eq in Hnfp.
    repeat cases_if×...
    - apply has_top_nil_sizeP_0 in e; jauto.
      apply has_top_has_free_nil in e; jauto. false×.
    - apply has_top_nil_sizeP_0 in e; jauto.
      apply has_top_has_free_nil in e; jauto. false×.
    - rewrite H... rewrite H...
Qed.

Lemma ext_cgr_step_remove_par_nils_rr_eq :
  ∀ p q, p -≡-> q ↔ remove_par_nils p -≡-> remove_par_nils q.
Proof.
  introv; splits.

  introv Hr. inverts Hr. destruct H as (p´ & q´ & Hc1 & Hc2 & Hr).
  constructor. ∃ p´. ∃ q´; splits*; etransitivity; try eassumption.
  symmetry. apply remove_par_nils_wfcgr. apply remove_par_nils_wfcgr.

  introv Hr. inverts Hr. destruct H as (p´ & q´ & Hc1 & Hc2 & Hr).
  constructor. ∃ p´. ∃ q´; splits*; etransitivity; try eassumption.
  apply remove_par_nils_wfcgr. symmetry. apply remove_par_nils_wfcgr.
Qed.

Lemma ext_cgr_full_remove_par_nils_rr_lr :
  ∀ p q, p -≡->* q → remove_par_nils p -≡->* remove_par_nils q.
Proof.
  introv Ht. inductions Ht.
  constructor. rewrite¬ <- ext_cgr_step_remove_par_nils_rr_eq.
  etransitivity; eassumption.
Qed.

Lemma ext_cgr_step_remove_par_nils :
  ∀ p q, p -≡-> q ↔ remove_par_nils p -≡-> q.
Proof.
  introv; splits.

  introv Hr. inverts Hr. destruct H as (p´ & q´ & Hc1 & Hc2 & Hr).
  constructor. ∃ p´. ∃ q´; splits*; etransitivity; try eassumption.
  symmetry. apply remove_par_nils_wfcgr.

  introv Hr. inverts Hr. destruct H as (p´ & q´ & Hc1 & Hc2 & Hr).
  constructor. ∃ p´. ∃ q´; splits*; etransitivity; try eassumption.
  apply remove_par_nils_wfcgr.
Qed.

Instance trans_clos_trans_1n : ∀ A R, Transitive (clos_trans_1n A R).
Proof.
  introv Hxy. inductions Hxy; introv Hyp.
  eapply Relations.Relation_Operators.t1n_trans. eassumption. auto.
  eapply Relations.Relation_Operators.t1n_trans. eassumption. auto.
Qed.

Lemma transitive_closure_equal : ∀ A R x y,
  clos_trans_1n A R x y ↔ clos_trans A R x y.
Proof.
  introv; splits; introv Hyp;
  inductions Hyp; try solve [constructor~].
  + apply (t_step A R) in H. eapply t_trans; eassumption.
  + etransitivity; eassumption.
Qed.

Lemma ext_cgr_full_remove_par_nils :
  ∀ p q, p -≡->* q ↔ remove_par_nils p -≡->* q.
Proof.
  introv; splits.

  introv Ht. inductions Ht.
  constructor. rewrite¬ <- ext_cgr_step_remove_par_nils.
  etransitivity. Focus 2. eassumption.
  apply ext_cgr_full_remove_par_nils_rr_lr in IHHt1.
  rewrite remove_par_nils_absorb in IHHt1; jauto.
  apply remove_nil_no_par_nil.

  introv Ht. unfolds ext_cgr_full. rewrite <- transitive_closure_equal in Ht.
  inductions Ht. constructor. rewrite¬ ext_cgr_step_remove_par_nils.
  rewrite <- transitive_closure_equal. eapply Relations.Relation_Operators.t1n_trans.
  rewrite ext_cgr_step_remove_par_nils. eassumption. auto.
Qed.

Lemma nf_cannot_reduce : ∀ p,
  (∀ q, ¬ (p -≡->* q)) ↔ normal_form (remove_par_nils p).
Proof.
  lets Hyp_lr : nf_cannot_reduce_lr.
  lets Hyp_rl : nf_cannot_reduce_rl.
  introv; splits~; intro Hyp.
  + apply Hyp_rl. introv Ht. eapply (Hyp q).
    rewrite¬ ext_cgr_full_remove_par_nils.
    apply remove_nil_no_par_nil.
  + introv Ht. eapply Hyp_lr. eassumption.
    rewrite <- ext_cgr_full_remove_par_nils. eassumption.
Qed.


Program Fixpoint nested_abs (n : nat) (p : wfprocess) {measure (wfp_size p)} : list nat :=
match p with
  | mkWfP (Send a p) wfc ⇒
     let wfp := mkWfP p (wf_send a p wfc) in
       nested_abs n wfp
| mkWfP (Receive a x p) wfc ⇒
       n :: nested_abs (S n) (snd (Abs_from_Receive a x p wfc nil))
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         (nested_abs n wfp) ++ (nested_abs n wfq)
  | _ ⇒ nil
end.
Next Obligation.
  unfold wfp_size; simpl.
  lets Hyp : Abs_from_Receive_spec a x p0.
  specialize (Hyp wfc nil). destruct Hyp as (Hyp & _).
  simpl in Hyp; unfold Abs in Hyp; inverts Hyp. rewrite H1 at 2.
  rewrite¬ size_subst.
Defined.
Next Obligation.
  unfold wfp_size; simpl; nat_math.
Defined.
Next Obligation.
  unfold wfp_size; simpl; nat_math.
Defined.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Defined.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Defined.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Defined.

Lemma nested_abs_eq : ∀ n p, nested_abs n p =
match p with
  | mkWfP (Send a p) wfc ⇒
     let wfp := mkWfP p (wf_send a p wfc) in
       nested_abs n wfp
| mkWfP (Receive a x p) wfc ⇒
       n :: nested_abs (S n) (snd (Abs_from_Receive a x p wfc nil))
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         (nested_abs n wfp) ++ (nested_abs n wfq)
  | _ ⇒ nil
end.
Proof.
intros.
  unfold nested_abs at 1. unfold nested_abs_func. rewrite Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    destruct w; simpl.
    destruct proc; simpl; repeat rewrite H; intuition.
Qed.

Lemma nested_abs_eq_send : ∀ p a n, nested_abs n (wfp_Send a p) = nested_abs n p.
Proof.
  introv. rewrite nested_abs_eq; simpls. fequals. rewrite_wfp_equal.
Qed.

Lemma nested_abs_eq_par : ∀ p q n, nested_abs n (wfp_Par p q) = nested_abs n p ++ nested_abs n q.
Proof.
  introv. rewrite nested_abs_eq; simpls. repeat fequals; rewrite_wfp_equal.
Qed.

Lemma nested_abs_eq_gvar : ∀ X n, nested_abs n (wfp_Gvar X) = nil.
Proof.
  introv. rewrite nested_abs_eq; simpls¬.
Qed.

Lemma nested_abs_eq_nil : ∀ n, nested_abs n wfp_Nil = nil.
Proof.
  introv. rewrite nested_abs_eq; simpls¬.
Qed.

Lemma nested_abs_gsubst : ∀ p n X Y,
  nested_abs n p = nested_abs n (wfp_subst (wfp_Gvar Y) X p).
Proof.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv; rewrite_wfp_subst; auto.
    rewrite_wfp_subst. repeat rewrite nested_abs_eq_send.
    apply H; solve_wfp_size.

  Focus 2.
    cases_if×.

  Focus 2.
    rewrite_wfp_subst. repeat rewrite nested_abs_eq_par.
    fequals; apply H; solve_wfp_size.

    repeat rewrite nested_abs_eq; simpls.
    rename p0 into p.
    lets Hyp1 : (Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p) (WfAbs a X p (wf_cond p)) nil).
    lets Hyp2 : (Abs_from_Receive_spec a (f X p) ([Gvar Y // X0]([Lvar (f X p) // X]p)) (wf_subst (Abs f a X p) (WfAbs a X p (wf_cond p)) X0 (Gvar Y) (WfGvar Y)) nil).
    destruct Hyp1 as (Hyp1 & _); destruct Hyp2 as (Hyp2 & _).
    remember (fst
             (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
                (WfAbs a X p (wf_cond p)) nil)) as Z1.
    remember (snd
             (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
                (WfAbs a X p (wf_cond p)) nil)) as q1.
   remember (fst
              (Abs_from_Receive a (f X p) ([Gvar Y // X0]([Lvar (f X p) // X]p)) (wf_subst (Abs f a X p) (WfAbs a X p (wf_cond p)) X0 (Gvar Y) (WfGvar Y)) nil)) as Z2.
    remember (snd
               (Abs_from_Receive a (f X p) ([Gvar Y // X0]([Lvar (f X p) // X]p)) (wf_subst (Abs f a X p) (WfAbs a X p (wf_cond p)) X0 (Gvar Y) (WfGvar Y)) nil)) as q2.
    clear HeqZ1 HeqZ2 Heqq1 Heqq2.
    lets Hwf1 : wf_cond (wfp_Abs a Z1 q1). rewrite <- Hyp1 in Hwf1.
    lets Hwf2 : wf_cond (wfp_Abs a Z2 q2). rewrite <- Hyp2 in Hwf2.
    lets (Z & Hfz) : find_fresh (proc p :: (Gvar Y) :: (Gvar X0) :: nil);
    rewrite Forall_to_conj_3 in Hfz.
    apply wf_receive with (X := Z) in Hwf1; try fresh_solve.
    apply wf_receive with (X := Z) in Hwf2.
    rewrite substs_commute_lg in Hwf2.
    rewrite <- subst_decomposition_l in *; try apply f_is_good; try apply¬ wf_lfresh.
    destruct Hwf1 as (Hwf1 & Heq1); destruct Hwf2 as (Hwf2 & Heq2).
    rewrite Heq1 in Hyp1; rewrite Heq2 in Hyp2; clear Heq1 Heq2 Hwf1 Hwf2.
    assert (Abs f a Z ([Gvar Z // X]p) = wfp_Abs a Z (wfp_subst (wfp_Gvar Z) X p)).
      simpl; fequals. rewrite H0 in Hyp1.
    assert (Abs f a Z ([Gvar Y // X0]([Gvar Z // X]p)) = wfp_Abs a Z (wfp_subst (wfp_Gvar Y) X0 (wfp_subst (wfp_Gvar Z) X p))).
      simpl; fequals. rewrite H1 in Hyp2; clear H0 H1.
    remember (wfp_subst (wfp_Gvar Z) X p) as p´.
    rewrite <- wfprocess_eq in *; rewrite wfp_Abs_equal in ×.
    destruct Hyp1 as (_ & Hyp1); destruct Hyp2 as (_ & Hyp2).
      repeat cases_if×.
        subst. erewrite (H q1 _ (S n) X0 Y); auto.
        lets Heq´ : wfp_subst_eq_rewrite p´ q1 Z Z1 Hyp1.
        destruct Hyp1 as (Heq & Hfz´). destruct Heq´ as (Heq´ & Hfz1).
        rewrite Heq in Hyp2. rewrite <- Hyp2.
        repeat erewrite <- H; auto.
          subst; unfold wfp_size; simpls; repeat rewrite¬ size_subst; nat_math.
          subst; unfold wfp_size; simpls; repeat rewrite¬ size_subst; nat_math.
        rewrite Hyp1 in ×. lets Heq´ : wfp_subst_eq_rewrite Hyp2.
        destruct Heq´ as (Heq´ & Hfz2). rewrite Heq´.
        repeat erewrite <- H; auto.
          subst; unfold wfp_size; simpls; repeat rewrite¬ size_subst; nat_math.
          subst; unfold wfp_size; simpls; repeat rewrite¬ size_subst; nat_math.
        destruct Hyp1 as (Heq & Hfz´). rewrite Heq in Hyp2.
        lets Heq´ : wfp_subst_eq_rewrite Hyp2.
        destruct Heq´ as (Heq´ & Hfz2).
        rewrite Heq´. repeat erewrite <- H; auto.
          subst; unfold wfp_size; rewrite wfprocess_eq in Heq; simpls.
          rewrite <- size_subst with (X := Z1) (q := (Gvar Z)); auto. rewrite <- Heq.
          repeat rewrite¬ size_subst; nat_math.
          subst; unfold wfp_size; rewrite wfprocess_eq in *; simpls.
          rewrite <- Heq; repeat rewrite¬ size_subst; nat_math.
          subst; unfold wfp_size; rewrite wfprocess_eq in Heq; simpls.
          rewrite <- Heq; repeat rewrite¬ size_subst; nat_math.
          repeat rewrite gfresh_gvar in *; jauto.
          freshen_up. applys× gfresh_in_subst_p_q.
          applys× gfresh_in_subst_p_q. freshen_up.
Grab Existential Variables.
  rewrite Heqp´. unfold wfp_size; simpls.
  repeat rewrite¬ size_subst. nat_math.
Qed.

Lemma nested_abs_eq_abs : ∀ p a X n, nested_abs n (wfp_Abs a X p) = n :: nested_abs (S n) p.
Proof.
  introv. rewrite nested_abs_eq; simpls; fequals.
  lets Hyp : (Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p) (WfAbs a X p (wf_cond p)) nil).
    destruct Hyp as (Hyp & _).
    remember (fst
             (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
                (WfAbs a X p (wf_cond p)) nil)) as Y.
    remember (snd
             (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
                (WfAbs a X p (wf_cond p)) nil)) as p´.

    lets Hwf : wf_cond (wfp_Abs a Y p´). rewrite <- Hyp in Hwf.
    lets (Z & Hfz) : find_fresh (proc p :: nil).
    rewrite Forall_to_conj_1 in Hfz.
    apply wf_receive with (X := Z) in Hwf.
    destruct Hwf as (Hwf & Heq). rewrite Heq in Hyp; clear Heq.
    rewrite <- subst_decomposition_l in *; try apply f_is_good; try apply¬ wf_lfresh.
    assert (Abs f a Z ([Gvar Z // X]p) = wfp_Abs a Z (wfp_subst (wfp_Gvar Z) X p)).
      simpl; fequals.
    rewrite H in Hyp. rewrite <- wfprocess_eq in Hyp; rewrite wfp_Abs_equal in Hyp.
    clear H Hwf; destruct Hyp as (_ & Hyp). cases_if×.
      rewrite <- Hyp. rewrite¬ <- nested_abs_gsubst.
      apply wfp_subst_eq_rewrite in Hyp; destruct Hyp as (Hyp & _).
      rewrite Hyp. repeat rewrite¬ <- nested_abs_gsubst.
      fresh_solve.
Qed.

Ltac simpl_nested_abs := repeat
  (repeat rewrite nested_abs_eq_send;
   repeat rewrite nested_abs_eq_abs;
   repeat rewrite nested_abs_eq_gvar;
   repeat rewrite nested_abs_eq_par;
   repeat rewrite nested_abs_eq_nil).

Definition list_sum (l : list nat) := fold_right plus 0 l.

Lemma list_sum_nil : list_sum nil = 0.
Proof.
  unfold list_sum; auto.
Qed.

Lemma list_sum_cons : ∀ l a, list_sum (a :: l) = a + list_sum l.
Proof.
  introv; unfold list_sum; simpls¬.
Qed.

Lemma list_sum_app : ∀ l1 l2,
  list_sum (l1 ++ l2) = list_sum l1 + list_sum l2.
Proof.
  inductions l1; introv.
    rewrite app_nil_l; simpls¬.
    replace ((a :: l1) ++ l2) with (a :: (l1 ++ l2)) by auto.
    repeat rewrite list_sum_cons. rewrite IHl1; nat_math.
Qed.

Ltac simpl_list_sum := repeat
  (repeat rewrite list_sum_nil;
   repeat rewrite list_sum_cons;
   repeat rewrite list_sum_app).

Lemma nested_abs_monotonous : ∀ p n,
  list_sum (nested_abs n p) ≤ list_sum (nested_abs (S n) p).
Proof with (simpl_nested_abs; simpl_list_sum).
  induction p using wfp_ind; introv; simpl_nested_abs; simpl_list_sum;
  try solve [jauto; nat_math].
    specializes IHp (S n). nat_math.
    specializes IHp1 n; specializes IHp2 n; nat_math.
Qed.


Lemma wfcgr_measure : ∀ p q, p ≡* q → ∀ n, list_sum (nested_abs n p) = list_sum (nested_abs n q).
Proof with (simpl_nested_abs; simpl_list_sum).
  introv Ht. inductions Ht.
    inductions H; introv; simpl_nested_abs; simpl_list_sum; try solve [jauto; nat_math].
    etransitivity. apply IHHt1. apply IHHt2.
Qed.

Lemma norm_step_measure : ∀ p q n, p ---> q → list_sum (nested_abs n q) < list_sum (nested_abs n p).
Proof with (simpl_nested_abs; simpl_list_sum).
  induction p using (measure_induction wfp_size).
  introv Hns; inverts Hns...
    simpl wfp_repeat... destruct n0. nat_math.
    simpl wfp_repeat; rewrite wfp_prod_cons...
    rewrite <- plus_assoc. rew_nat.
    destruct n0.
      simpl... nat_math.
      simpl wfp_repeat; repeat rewrite wfp_prod_cons...
      lets Hyp1 : nested_abs_monotonous wfp_Nil (S n).
      lets Hyp2 : nested_abs_monotonous (wfp_prod (wfp_Abs a X wfp_Nil :: wfp_repeat n0 (wfp_Abs a X wfp_Nil))) n. nat_math.

    simpl wfp_repeat... destruct n0. nat_math.
    simpl wfp_repeat; rewrite wfp_prod_cons...
    rewrite <- plus_assoc. rew_nat.
    destruct n0.
      simpl... lets Hyp : nested_abs_monotonous p0 (S n). nat_math.
      simpl wfp_repeat; repeat rewrite wfp_prod_cons...
      lets Hyp1 : nested_abs_monotonous p0 (S n).
      lets Hyp2 : nested_abs_monotonous (wfp_prod (wfp_Abs a X p0 :: wfp_repeat n0 (wfp_Abs a X p0))) n. nat_math.

    applys× H; solve_wfp_size.
    rew_nat. applys× H; solve_wfp_size.
    rew_nat. applys× H; solve_wfp_size.
    rew_nat. applys× H; solve_wfp_size.
Qed.

Lemma norm_full_measure : ∀ p q n, (p --->* q) → list_sum (nested_abs n q) < list_sum (nested_abs n p).
Proof.
  introv Ht; inductions Ht.
    apply¬ norm_step_measure.
  nat_math.
Qed.

Lemma ext_cgr_step_measure : ∀ p q n, p -≡-> q → list_sum (nested_abs n q) < list_sum (nested_abs n p).
Proof.
  introv Ht. inductions Ht.
  destruct H as (p´ & q´ & Hc1 & Hc2 & Hn).
    apply wfcgr_measure with (n := n) in Hc1.
    apply wfcgr_measure with (n := n) in Hc2.
    apply norm_full_measure with (n := n) in Hn.
    nat_math.
Qed.

Lemma ext_cgr_full_measure : ∀ p q n, p -≡->* q → list_sum (nested_abs n q) < list_sum (nested_abs n p).
Proof.
  introv Ht. inductions Ht.
    apply¬ ext_cgr_step_measure.
    nat_math.
Qed.

Lemma ext_cgr_irreflexive : ∀ p, ¬ (p -≡->* p).
Proof.
  introv Ht; apply ext_cgr_full_measure with (n := 0) in Ht; nat_math.
Qed.

Lemma ext_cgr_asymmetric : ∀ p q, (p -≡->* q) → ¬ (q -≡->* p).
Proof.
  introv Ht1 Ht2;
  apply ext_cgr_full_measure with (n := 0) in Ht1;
  apply ext_cgr_full_measure with (n := 0) in Ht2; nat_math.
Qed.

Instance dec_nf_classic : ∀ p, Decidable (normal_form p).
Proof.
  introv; applys¬ decidable_make.
Qed.

Lemma normalization_stops :
  ∀ p,
    normal_form p ∨ normal_form (remove_par_nils p) ∨
    (∃ q, p -≡->* q ∧ normal_form q).
Proof.
  induction p using (measure_induction (fun p ⇒ (list_sum (nested_abs 0 p)))).

  tests Hnp1 : (normal_form p); [left | right]; auto.
  tests Hnp2 : (normal_form (remove_par_nils p)); [left | right]; auto.

    rewrite <- nf_cannot_reduce in Hnp2.
    rew_logic in ×. destruct Hnp2 as (q & Hq). apply not_not_elim in Hq.
    lets Ht : Hq. apply ext_cgr_full_measure with (n := 0) in Hq.
    specializes H Hq. inverts H.
    eexists; splits; eassumption. inverts H0.
    eexists; splits. Focus 2. eassumption.
    rewrite ext_cgr_full_remove_par_nils. applys¬ ext_cgr_full_remove_par_nils_rr_lr.
    destruct H as (q´ & Htq´ & Hnfq´).
    eexists; splits. Focus 2. eassumption.
    etransitivity; eassumption.
Qed.


Lemma prime_characterization : ∀ p, prime p →
  ((∃ a p´, p ≈ wfp_Send a p´) ∨
   (∃ X, p ≈ wfp_Gvar X) ∨
   (∃ a X p´, p ≈ wfp_Abs a X p´ ∧ (∀ n, n > 0 → ∀ q, ¬ (p´ ≡* (wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q)))))))).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hprime.
    branch 1. eexists. eexists. reflexivity.
    Focus 2. branch 2. eexists. reflexivity.
    Focus 3. false. applys¬ not_prime_nil.
    Focus 2. rewrite prime_parallel in Hprime; inverts Hprime; destruct H0 as (H0 & H1).
      specializes H H0...
      inverts H; [branch 1 | inverts H2; [branch 2 | branch 3]].
        destruct H2 as (a & p´ & Hyp). ∃ a p´.
        etransitivity. apply IObis_congr_par; eassumption.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.
        destruct H as (X & Hyp). ∃ X.
        etransitivity. apply IObis_congr_par; eassumption.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.
        destruct H as (a & X & p´ & Hyp1 & Hyp2). ∃ a X p´. splits×.
        etransitivity. apply IObis_congr_par; eassumption.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.

      specializes H H0...
      inverts H; [branch 1 | inverts H2; [branch 2 | branch 3]].
        destruct H2 as (a & p´ & Hyp). ∃ a p´.
        etransitivity. apply IObis_congr_par; eassumption.
        etransitivity. apply IObis_congr_par_com.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.
        destruct H as (X & Hyp). ∃ X.
        etransitivity. apply IObis_congr_par; eassumption.
        etransitivity. apply IObis_congr_par_com.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.
        destruct H as (a & X & p´ & Hyp1 & Hyp2). ∃ a X p´. splits×.
        etransitivity. apply IObis_congr_par; eassumption.
        etransitivity. apply IObis_congr_par_com.
        ∃ wfcgr; splits. apply congr_IObisimulation.
        repeat constructor.

    clear H. branch 3. rename p0 into p.
    elim (classic (∀ n : nat, n > 0 → ∀ q, ¬p ≡* wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q))))); introv Hyp.
      ∃ a X p; splits×.
      rew_logic in ×. destruct Hyp as (n & Hyp).
      rew_logic in ×. destruct Hyp as (Hn & q & Hyp).
      apply not_not_elim in Hyp. false.

      assert (Hyp1 : wfp_Abs a X p ≈ wfp_Abs a X (wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q))))).
        apply IObis_congr_abs. ∃ wfcgr; splits×. apply congr_IObisimulation. clear Hyp.

      tests Hsq : (wfp_sizeP q = 0).

      assert (Hyp1´ : wfp_Abs a X p ≈ wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil)))).
        etransitivity. eassumption.
        apply congr_IObis. apply wfcgr_abs.
        apply wfp_sizeP_0_wfcgr_nil in Hsq.
        etransitivity. apply wfcgr_par_com. etransitivity.
        apply wfcgr_par. reflexivity. eassumption.
        etransitivity. apply wfcgr_nil_r. gen Hsq. clear. introv Hsq.
        inductions n. simpl. reflexivity.
        destruct n. simpl. applys¬ wfcgr_abs.
        repeat rewrite wfp_prod_repeat_SS. applys¬ wfcgr_par. applys¬ wfcgr_abs.
      clear Hyp1.

      assert (Hyp2 : wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))) ---> wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))).
        constructor¬.
      apply io_norm_step in Hyp2.
      destruct n. nat_math. clear Hn.
      rewrite wfp_prod_repeat_SS in ×.
      destruct Hprime as (_ & Hprime).
      specializes Hprime (wfp_Abs a X wfp_Nil) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))).

      assert (Hyp3 : wfp_Abs a X p ≈ wfp_Par (wfp_Abs a X wfp_Nil)
               (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
        etransitivity; eassumption.

      specializes Hprime Hyp3. inverts Hprime; rewrite <- wfp_sizeP_0_IO_nil in ×...
      destruct n; simpls...

      assert (Hyp2 : wfp_Abs a X (wfp_Par q (wfp_prod (wfp_repeat n (wfp_Abs a X q)))) ---> wfp_prod (wfp_repeat (S n) (wfp_Abs a X q))).
        constructor¬. nat_math.
      apply io_norm_step in Hyp2.
      destruct n. nat_math. clear Hn.
      rewrite wfp_prod_repeat_SS in ×.
      destruct Hprime as (_ & Hprime).
      specializes Hprime (wfp_Abs a X q) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q))).

      assert (Hyp3 : wfp_Abs a X p ≈ wfp_Par (wfp_Abs a X q)
               (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q)))).
        etransitivity; eassumption.

      specializes Hprime Hyp3. inverts Hprime; rewrite <- wfp_sizeP_0_IO_nil in ×...
      destruct n; simpls...
Qed.


Lemma dpd_no_red_base : ∀ p, dpd p → ∀ q, ¬ (p --->* q).
Proof.
  introv Hd Ht. inductions Ht; jauto.
  inductions H; simpl_dpd; jauto.

    destruct Hd as (Hd & _).
    inverts Hd. clear H0.
    destruct n. nat_math.
    assert (Hred : wfp_Abs a X (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) ---> (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X wfp_Nil)))) by constructor¬.
    lets Hyp : io_norm_step Hred.
    specialize (H1 (wfp_Abs a X wfp_Nil) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
    assert (wfp_Abs a X (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))
          ≈ wfp_Par (wfp_Abs a X wfp_Nil) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
      etransitivity. eassumption. simpl wfp_repeat. rewrite wfp_prod_cons.
      applys¬ IObis_congr_par.
    specializes H1 H0. inverts H1 as H1. apply IObis_sizeP_eq in H1; automate.
    simpl wfp_repeat in H1. destruct n. simpls. apply IObis_sizeP_eq in H1; automate.
    simpl wfp_repeat in H1. rewrite wfp_prod_cons in H1. apply IObis_sizeP_eq in H1; automate.

    destruct Hd as (Hd & _ & _).
    inverts Hd. clear H0.
    destruct n. nat_math.
    tests Hs : (wfp_sizeP p > 0).

    assert (Hred : wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))) ---> (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X p)))) by constructor¬.
    lets Hyp : io_norm_step Hred.
    specialize (H2 (wfp_Abs a X p) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))).
    assert (wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))))
          ≈ wfp_Par (wfp_Abs a X p) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))).
      etransitivity. eassumption. simpl wfp_repeat. rewrite wfp_prod_cons.
      applys¬ IObis_congr_par.
    specializes H2 H0. inverts H2 as H2. apply IObis_sizeP_eq in H2; automate.
    simpl wfp_repeat in H2. destruct n. simpls. apply IObis_sizeP_eq in H2; automate.
    simpl wfp_repeat in H2. rewrite wfp_prod_cons in H2. apply IObis_sizeP_eq in H2; automate.

    assert (Hred : wfp_Abs a X (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))) ---> (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X wfp_Nil)))) by constructor¬.
    lets Hyp : io_norm_step Hred.
    specialize (H2 (wfp_Abs a X wfp_Nil) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
    assert (wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))))
          ≈ wfp_Par (wfp_Abs a X wfp_Nil) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
      transitivity (wfp_Abs a X (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))). apply IObis_congr_abs. etransitivity. eapply IObis_congr_par.
      instantiate (1 := wfp_Nil). apply congr_IObis.
      rewrite <- wfp_sizeP_0_wfcgr_nil. nat_math.
      instantiate (1 := wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))).
      gen Hs. clear. intro Hs. inductions n.
        simpl. apply IObis_congr_abs. apply congr_IObis.
        rewrite <- wfp_sizeP_0_wfcgr_nil. nat_math.
      do 2 rewrite wfp_prod_repeat_SS. applys× IObis_congr_par.
        apply IObis_congr_abs. apply congr_IObis.
        rewrite <- wfp_sizeP_0_wfcgr_nil. nat_math.
      apply congr_IObis. etransitivity. apply wfcgr_par_com.
      apply wfcgr_nil_r.
      etransitivity. eassumption. simpl wfp_repeat. rewrite wfp_prod_cons.
      applys¬ IObis_congr_par.

    specializes H2 H0. inverts H2 as H2. apply IObis_sizeP_eq in H2; automate.
    simpl wfp_repeat in H2. destruct n. simpls. apply IObis_sizeP_eq in H2; automate.
    simpl wfp_repeat in H2. rewrite wfp_prod_cons in H2. apply IObis_sizeP_eq in H2; automate.
Qed.

Lemma dpd_normal_form : ∀ p, dpd p → normal_form p.
Proof.
  introv Hd. rewrite nf_equiv_par_nil. rewrite dpd_equiv_par_nil in Hd.
  splits×. destruct Hd as (Hfpn_p & Hdp). rewrite <- nf_cannot_reduce.
  introv Ht. inductions Ht; jauto.
  inverts H.
  destruct H0 as (x´ & y´ & Hc1 & Hc2 & Hred).
  apply remove_par_nils_red in Hred.
  eapply dpd_no_red_base. Focus 2. eassumption.
  eapply dpd_remove_nil_congr; eassumption.
Qed.

Lemma dpd_components_normal_form : ∀ dp, dpd dp →
  (Forall (fun p : wfprocess ⇒ normal_form p) (components dp)).
Proof with automate.
  induction dp using (measure_induction wfp_size); destruct_wf dp;
  simpl_components; introv Hdp; simpl_dpd; try solve [do 2 constructor*].
    constructor. constructor. specializes H Hdp...
    applys¬ dpd_normal_form. constructor.

    assert (Hnf: normal_form (wfp_Abs a X p)).
    apply dpd_normal_form; simpl_dpd; jauto.
    constructor¬. constructor.

    apply Forall_app; applys× H...
Qed.


Lemma wfprocess_exists_list_prime_nf : ∀ p, ∃ lp,
  Forall (fun p : wfprocess ⇒ prime p) lp ∧
  Forall (fun p : wfprocess ⇒ normal_form p) lp ∧
  p ≈ wfp_prod lp.
Proof.
  introv.
  lets (dp & Hio & Hdp) : deep_prime_decomposition_exists p.
  ∃ (components dp); splits.
    applys¬ dpd_components_prime.
    applys¬ dpd_components_normal_form.
    etransitivity. eassumption.
    apply wfp_prod_components_lr.
Qed.

Lemma send_separation : ∀ (p : wfprocess), num_send p > 0 →
  ∃ a p´ lp, p ≈ wfp_Par (wfp_Send a p´) (wfp_prod lp) ∧
  normal_form p´ ∧
  Forall (fun p : wfprocess ⇒ prime p) lp ∧
  Forall (fun p : wfprocess ⇒ normal_form p) lp.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpls; introv Hns; try solve [false; nat_math].

  + clear Hns. lets Hnorm : normalization_stops p0.
    inverts Hnorm as Hnorm.
    - ∃ a p0 (@nil wfprocess); splits*; try solve [constructor*].
      applys¬ congr_IObis. constructor×.
    - inverts Hnorm as Hnorm.
      × ∃ a (remove_par_nils p0) (@nil wfprocess); splits*; try solve [constructor*].
        applys¬ congr_IObis. etransitivity. apply wfcgr_send.
        apply remove_par_nils_wfcgr. constructor×.
      × destruct Hnorm as (p´ & Hiop´ & Hnfp´).
        ∃ a p´ (@nil wfprocess); splits*; try solve [constructor*].
        etransitivity. apply IObis_congr_send.
        apply io_extcgr_full. eassumption.
        simpl. apply IObis_congr_nil_l.

  + assert (num_send p1 > 0 ∨ num_send p2 > 0) by nat_math.
    inverts H0 as Hyp; clear Hns.
    - specializes H Hyp...
      destruct H as (a & p´ & lp1 & Hiop1 & Hnp1 & Hplp1 & Hnlp1).
      lets (lp2 & Hplp2 & Hnlp2 & Hiop2) : wfprocess_exists_list_prime_nf p2.
      ∃ a p´ (lp1 ++ lp2). splits*; try solve [applys× Forall_app].
      etransitivity. apply IObis_congr_par; eassumption.
      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      symmetry. apply wfp_prod_IO_app.
    - specializes H Hyp...
      destruct H as (a & p´ & lp2 & Hiop2 & Hnp2 & Hplp2 & Hnlp2).
      lets (lp1 & Hplp1 & Hnlp1 & Hiop1) : wfprocess_exists_list_prime_nf p1.
      ∃ a p´ (lp1 ++ lp2). splits*; try solve [applys× Forall_app].
      etransitivity. apply IObis_congr_par; eassumption.
      etransitivity. apply IObis_par_assoc_l. etransitivity.
      apply IObis_congr_par. apply IObis_congr_par_com. reflexivity.
      etransitivity. apply IObis_par_assoc_r.
      applys¬ IObis_congr_par. symmetry. apply wfp_prod_IO_app.
Qed.




Program Fixpoint get_vars (p : wfprocess) {measure (wfp_size p)} :=
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_vars wfp ++ get_vars wfq
  | mkWfP (Gvar X) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Next Obligation.
  automate.
Qed.
Next Obligation.
  automate.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.

Lemma get_vars_eq : ∀ p, get_vars p =
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_vars wfp ++ get_vars wfq
  | mkWfP (Gvar X) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Proof.
intros.
  unfold get_vars at 1. rewrite Wf.Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.

Lemma get_vars_eq_send : ∀ p a, get_vars (wfp_Send a p) = nil.
Proof.
  introv. rewrite get_vars_eq; simpls¬.
Qed.

Lemma get_vars_eq_abs : ∀ p a X, get_vars (wfp_Abs a X p) = nil.
Proof.
  introv. rewrite get_vars_eq; simpls¬.
Qed.

Lemma get_vars_eq_gvar : ∀ X, get_vars (wfp_Gvar X) = (wfp_Gvar X :: nil).
Proof.
  introv. rewrite get_vars_eq; simpls¬.
Qed.

Lemma get_vars_eq_par : ∀ p q, get_vars (wfp_Par p q) = get_vars p ++ get_vars q.
Proof.
  introv. rewrite get_vars_eq; simpls.
  assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
  assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.

Lemma get_vars_eq_nil : get_vars wfp_Nil = nil.
Proof.
  introv. rewrite get_vars_eq; simpls¬.
Qed.

Ltac simpl_get_vars := repeat
  (repeat rewrite get_vars_eq_send in *;
   repeat rewrite get_vars_eq_abs in *;
   repeat rewrite get_vars_eq_gvar in *;
   repeat rewrite get_vars_eq_par in *;
   repeat rewrite get_vars_eq_nil in × ).

Lemma get_vars_spec : ∀ p q, Mem q (get_vars p) →
  (∃ X, q = wfp_Gvar X ∧ ∃ p´, p ≡* wfp_Par (wfp_Gvar X) p´).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_get_vars; simpls~; introv Hm; try solve [inverts¬ Hm].
  inverts Hm. ∃ X. splits¬. ∃ wfp_Nil. constructor×. inverts H1.

  rewrite Mem_app_or_eq in Hm; inverts Hm as Hm; specializes H Hm...
    destruct H as (X & (Heq_q & (p1´ & Heq_p1))).
    ∃ X. splits¬. ∃ (wfp_Par p1´ p2).
    etransitivity. apply wfcgr_par. eassumption. reflexivity.
    constructor. apply WfCgrPar_assoc2.
    destruct H as (X & (Heq_q & (p2´ & Heq_p2))).
    ∃ X. splits¬. ∃ (wfp_Par p1 p2´).
    etransitivity. apply wfcgr_par. reflexivity. eassumption.
    etransitivity. constructor. apply WfCgrPar_assoc1.
    etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity.
    constructor. apply WfCgrPar_assoc2.
Qed.

Program Fixpoint get_outs (p : wfprocess) {measure (wfp_size p)} :=
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_outs wfp ++ get_outs wfq
  | mkWfP (Send a p´) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Next Obligation.
  automate.
Qed.
Next Obligation.
  automate.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.

Lemma get_outs_eq : ∀ p, get_outs p =
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_outs wfp ++ get_outs wfq
  | mkWfP (Send a p´) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Proof.
intros.
  unfold get_outs at 1. rewrite Wf.Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.

Lemma get_outs_eq_send : ∀ p a, get_outs (wfp_Send a p) = (wfp_Send a p :: nil).
Proof.
  introv. rewrite get_outs_eq; simpls¬.
Qed.

Lemma get_outs_eq_abs : ∀ p a X, get_outs (wfp_Abs a X p) = nil.
Proof.
  introv. rewrite get_outs_eq; simpls¬.
Qed.

Lemma get_outs_eq_gvar : ∀ X, get_outs (wfp_Gvar X) = nil.
Proof.
  introv. rewrite get_outs_eq; simpls¬.
Qed.

Lemma get_outs_eq_par : ∀ p q, get_outs (wfp_Par p q) = get_outs p ++ get_outs q.
Proof.
  introv. rewrite get_outs_eq; simpls.
  assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
  assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.

Lemma get_outs_eq_nil : get_outs wfp_Nil = nil.
Proof.
  introv. rewrite get_outs_eq; simpls¬.
Qed.

Ltac simpl_get_outs := repeat
  (repeat rewrite get_outs_eq_send in *;
   repeat rewrite get_outs_eq_abs in *;
   repeat rewrite get_outs_eq_gvar in *;
   repeat rewrite get_outs_eq_par in *;
   repeat rewrite get_outs_eq_nil in × ).

Lemma get_outs_spec : ∀ p q, Mem q (get_outs p) →
  (∃ a p´, q = wfp_Send a p´ ∧ ∃ p´´, p ≡* wfp_Par (wfp_Send a p´) p´´).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_get_outs; simpls~; introv Hm; try solve [inverts¬ Hm].
  inverts Hm. ∃ a p0. splits¬. ∃ wfp_Nil. constructor×. inverts H1.

  rewrite Mem_app_or_eq in Hm; inverts Hm as Hm; specializes H Hm...
    destruct H as (a & p´ & (Heq_q & (p1´ & Heq_p1))).
    ∃ a p´. splits¬. ∃ (wfp_Par p1´ p2).
    etransitivity. apply wfcgr_par. eassumption. reflexivity.
    constructor. apply WfCgrPar_assoc2.
    destruct H as (a & p´ & (Heq_q & (p2´ & Heq_p2))).
    ∃ a p´. splits¬. ∃ (wfp_Par p1 p2´).
    etransitivity. apply wfcgr_par. reflexivity. eassumption.
    etransitivity. constructor. apply WfCgrPar_assoc1.
    etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity.
    constructor. apply WfCgrPar_assoc2.
Qed.

Program Fixpoint get_ins (p : wfprocess) {measure (wfp_size p)} :=
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_ins wfp ++ get_ins wfq
  | mkWfP (Receive a X p´) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Next Obligation.
  automate.
Qed.
Next Obligation.
  automate.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
  splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.

Lemma get_ins_eq : ∀ p, get_ins p =
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         get_ins wfp ++ get_ins wfq
  | mkWfP (Receive a X p´) wfc ⇒ (p :: nil)
  | _ ⇒ (@nil wfprocess)
end.
Proof.
intros.
  unfold get_ins at 1. rewrite Wf.Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.

Lemma get_ins_eq_send : ∀ p a, get_ins (wfp_Send a p) = nil.
Proof.
  introv. rewrite get_ins_eq; simpls¬.
Qed.

Lemma get_ins_eq_abs : ∀ p a X, get_ins (wfp_Abs a X p) = (wfp_Abs a X p :: nil).
Proof.
  introv. rewrite get_ins_eq; simpls¬.
Qed.

Lemma get_ins_eq_gvar : ∀ X, get_ins (wfp_Gvar X) = nil.
Proof.
  introv. rewrite get_ins_eq; simpls¬.
Qed.

Lemma get_ins_eq_par : ∀ p q, get_ins (wfp_Par p q) = get_ins p ++ get_ins q.
Proof.
  introv. rewrite get_ins_eq; simpls.
  assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
  assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.

Lemma get_ins_eq_nil : get_ins wfp_Nil = nil.
Proof.
  introv. rewrite get_ins_eq; simpls¬.
Qed.

Ltac simpl_get_ins := repeat
  (repeat rewrite get_ins_eq_send in *;
   repeat rewrite get_ins_eq_abs in *;
   repeat rewrite get_ins_eq_gvar in *;
   repeat rewrite get_ins_eq_par in *;
   repeat rewrite get_ins_eq_nil in × ).

Lemma get_ins_spec : ∀ p q, Mem q (get_ins p) →
  (∃ a X p´, q = wfp_Abs a X p´ ∧ ∃ p´´, p ≡* wfp_Par (wfp_Abs a X p´) p´´).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_get_ins; simpls~; introv Hm; try solve [inverts¬ Hm].
  inverts Hm. ∃ a X p0. splits¬. ∃ wfp_Nil. constructor×. inverts H1.

  rewrite Mem_app_or_eq in Hm; inverts Hm as Hm; specializes H Hm...
    destruct H as (a & X & p´ & (Heq_q & (p1´ & Heq_p1))).
    ∃ a X p´. splits¬. ∃ (wfp_Par p1´ p2).
    etransitivity. apply wfcgr_par. eassumption. reflexivity.
    constructor. apply WfCgrPar_assoc2.
    destruct H as (a & X & p´ & (Heq_q & (p2´ & Heq_p2))).
    ∃ a X p´. splits¬. ∃ (wfp_Par p1 p2´).
    etransitivity. apply wfcgr_par. reflexivity. eassumption.
    etransitivity. constructor. apply WfCgrPar_assoc1.
    etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity.
    constructor. apply WfCgrPar_assoc2.
Qed.

Ltac simpl_gets := repeat (simpl_get_vars; simpl_get_outs; simpl_get_ins).

Lemma get_vars_sizeP : ∀ p, (Forall (fun p ⇒ wfp_sizeP p > 0) (get_vars p)).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_gets; try solve [constructor*].
  constructor... constructor.
  apply Forall_app; apply H...
Qed.

Lemma get_outs_sizeP : ∀ p, (Forall (fun p ⇒ wfp_sizeP p > 0) (get_outs p)).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_gets; try solve [constructor*].
  constructor... constructor.
  apply Forall_app; apply H...
Qed.

Lemma get_ins_sizeP : ∀ p, (Forall (fun p ⇒ wfp_sizeP p > 0) (get_ins p)).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_gets; try solve [constructor*].
  constructor... constructor.
  apply Forall_app; apply H...
Qed.

Lemma get_vars_wfp_prod_app : ∀ l1 l2, get_vars (wfp_prod (l1 ++ l2)) =
  get_vars (wfp_prod l1) ++ get_vars (wfp_prod l2).
Proof.
  induction l1 using (measure_induction length); destruct l1.
  + introv; rewrite app_nil_l; simpls; simpl_gets. rewrite¬ app_nil_l.
  + destruct l1.
    - introv; rewrite app_cons in *; rewrite app_nil_l in ×.
      simpl (wfp_prod (w :: nil)). clear H.
      gen w. induction l2 using (measure_induction length); destruct l2; introv.
      × simpl; simpl_gets; rewrite¬ app_nil_r.
      × rewrite wfp_prod_cons. simpl_gets; jauto.
    - introv; repeat rewrite app_cons; repeat rewrite wfp_prod_cons; simpl_gets.
      repeat rewrite app_assoc. fequals.
      rewrite <- app_cons. apply H. rew_length; nat_math.
Qed.

Lemma get_outs_wfp_prod_app : ∀ l1 l2, get_outs (wfp_prod (l1 ++ l2)) =
  get_outs (wfp_prod l1) ++ get_outs (wfp_prod l2).
Proof.
  induction l1 using (measure_induction length); destruct l1.
  + introv; rewrite app_nil_l; simpls; simpl_gets. rewrite¬ app_nil_l.
  + destruct l1.
    - introv; rewrite app_cons in *; rewrite app_nil_l in ×.
      simpl (wfp_prod (w :: nil)). clear H.
      gen w. induction l2 using (measure_induction length); destruct l2; introv.
      × simpl; simpl_gets; rewrite¬ app_nil_r.
      × rewrite wfp_prod_cons. simpl_gets; jauto.
    - introv; repeat rewrite app_cons; repeat rewrite wfp_prod_cons; simpl_gets.
      repeat rewrite app_assoc. fequals.
      rewrite <- app_cons. apply H. rew_length; nat_math.
Qed.

Lemma get_ins_wfp_prod_app : ∀ l1 l2, get_ins (wfp_prod (l1 ++ l2)) =
  get_ins (wfp_prod l1) ++ get_ins (wfp_prod l2).
Proof.
  induction l1 using (measure_induction length); destruct l1.
  + introv; rewrite app_nil_l; simpls; simpl_gets. rewrite¬ app_nil_l.
  + destruct l1.
    - introv; rewrite app_cons in *; rewrite app_nil_l in ×.
      simpl (wfp_prod (w :: nil)). clear H.
      gen w. induction l2 using (measure_induction length); destruct l2; introv.
      × simpl; simpl_gets; rewrite¬ app_nil_r.
      × rewrite wfp_prod_cons. simpl_gets; jauto.
    - introv; repeat rewrite app_cons; repeat rewrite wfp_prod_cons; simpl_gets.
      repeat rewrite app_assoc. fequals.
      rewrite <- app_cons. apply H. rew_length; nat_math.
Qed.

Definition get_components (p : wfprocess) := get_vars p ++ get_outs p ++ get_ins p.


Definition ordered (p : wfprocess) := wfp_prod (get_components p).

Lemma wfp_prod_wfcgr_cons : ∀ l p, wfp_prod (p :: l) ≡* wfp_Par p (wfp_prod l).
Proof.
  inductions l; introv. simpls; constructor×.
  rewrite wfp_prod_cons. etransitivity. apply wfcgr_par.
  reflexivity. apply IHl. apply wfcgr_par. reflexivity.
  symmetry. apply IHl.
Qed.

Lemma wfp_prod_wfcgr_app : ∀ l1 l2, wfp_prod (l1 ++ l2) ≡* wfp_Par (wfp_prod l1) (wfp_prod l2).
Proof.
  induction l1 using (measure_induction length); introv;
  destruct l1; repeat rewrite app_nil_l; repeat rewrite app_nil_r;
  try solve [constructor*].
  etransitivity. Focus 2. constructor. apply WfCgrPar_com. constructor×.

  rewrite app_cons. specializes H l1 l2. rew_length; nat_math.
  etransitivity. apply wfp_prod_wfcgr_cons.
  etransitivity. apply wfcgr_par. reflexivity. apply H.
  etransitivity. Focus 2. apply wfcgr_par. symmetry. apply wfp_prod_wfcgr_cons.
  reflexivity. constructor. apply WfCgrPar_assoc1.
Qed.

Lemma ordered_wfcgr : ∀ p, p ≡* ordered p.
Proof with (try solve [constructor*]; automate).
  induction p using (measure_induction wfp_size).
  unfolds ordered. unfolds get_components.
  destruct_wf p; simpl_gets; simpls¬...
  etransitivity. apply wfcgr_par. apply H... apply H...

  etransitivity. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  etransitivity. Focus 2. symmetry. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. apply wfcgr_par.
    symmetry. apply wfp_prod_wfcgr_app. symmetry. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  etransitivity. Focus 2. symmetry. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...
Qed.

Lemma ordered_par : ∀ p1 p2,
  ordered (wfp_Par p1 p2) ≡* wfp_Par (ordered p1) (ordered p2).
Proof with (try solve [constructor*]).
  introv; unfolds ordered; unfolds get_components; simpl_gets. symmetry.

  etransitivity. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  etransitivity. Focus 2. symmetry. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. apply wfcgr_par.
    symmetry. apply wfp_prod_wfcgr_app. symmetry. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry. constructor. apply WfCgrPar_assoc2.
  apply wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  apply wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry. apply wfcgr_par; apply wfp_prod_wfcgr_app.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  etransitivity. Focus 2. symmetry. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...

  etransitivity. constructor. apply WfCgrPar_com.
  etransitivity. constructor. apply WfCgrPar_assoc2.
  applys¬ wfcgr_par...
Qed.

Lemma wfp_size_wfp_prod_app : ∀ l1 l2, wfp_size (wfp_prod (l1 ++ l2)) = wfp_size (wfp_prod (l2 ++ l1)).
Proof.
  induction l1 using (measure_induction length).
  destruct l1; destruct l2; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *; try solve [nat_math].

  lets Hyp1 : H l1 (w0 :: l2). rew_length; nat_math.
  rewrite app_cons. replace (wfp_prod (w :: l1 ++ w0 :: l2)) with (wfp_Par w (wfp_prod (l1 ++ w0 :: l2))).
  Focus 2. clear. gen w w0 l2. destruct l1; introv; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in ×.
  rewrite¬ wfp_prod_cons. repeat rewrite app_cons. rewrite wfp_prod_cons. auto.
  replace (wfp_size (wfp_prod ((w0 :: l2) ++ w :: l1))) with (wfp_size (wfp_prod (w :: (w0 :: l2) ++ l1))).
  replace (wfp_prod (w :: (w0 :: l2) ++ l1)) with (wfp_Par w (wfp_prod ((w0 :: l2) ++ l1))). automate.
  rewrite app_cons. rewrite¬ wfp_prod_cons.
  remember (w0 :: l2) as l. clear. rename l1 into l2. rename l into l1.
  rewrite <- app_cons. replace (l1 ++ w :: l2) with ((l1 & w) ++ l2).
  Focus 2. gen w l2. inductions l1; introv; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in ×.
  rewrite app_cons. rewrite¬ app_nil_l.
  repeat rewrite app_cons. fequals.
  gen w l2; inductions l1; introv; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in ×. auto.
  replace (wfp_size (wfp_prod ((w :: a :: l1) ++ l2))) with
          (wfp_size (wfp_prod ((a :: w :: l1) ++ l2))).
  repeat rewrite app_cons. rewrite wfp_prod_cons.
  replace (wfp_size (wfp_prod (a :: l1 & w ++ l2))) with (wfp_size (wfp_Par a (wfp_prod (l1 & w ++ l2)))).
  unfolds wfp_size. specializes IHl1 w l2. rewrite app_cons in ×. automate.
  symmetry. clear. destruct l1; destruct l2; repeat (repeat rewrite app_cons; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in × ). simpls¬.
  repeat rewrite¬ wfp_prod_cons. rewrite¬ wfp_prod_cons. rewrite¬ wfp_prod_cons.
  clear. destruct l1; destruct l2; repeat (repeat rewrite app_cons; repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in × ). simpls; automate.
  repeat rewrite wfp_prod_cons. automate.
  repeat rewrite wfp_prod_cons. automate.
  repeat rewrite wfp_prod_cons. automate.
Qed.

Lemma wfp_size_wfp_prod_lt : ∀ l1 l2, l1 ≠ nil → l2 ≠ nil → wfp_size (wfp_prod (l1 ++ l2)) = S (wfp_size (wfp_prod l1) + wfp_size (wfp_prod l2)).
Proof.
  induction l1 using (measure_induction length); introv Hn1 Hn2.
  destruct l1; destruct l2; try solve [false*]; clear Hn1 Hn2.
  rewrite app_cons. replace (wfp_size (wfp_prod (w :: l1 ++ w0 :: l2))) with
  (wfp_size (wfp_Par w (wfp_prod (l1 ++ w0 :: l2)))).
  specializes H l1 (w0 :: l2). rew_length; nat_math.
  Focus 2. clear. destruct l1; repeat rewrite app_cons; repeat rewrite app_nil_l.
  rewrite¬ wfp_prod_cons. repeat rewrite¬ wfp_prod_cons.
  destruct l1. rewrite app_nil_l. automate.
  assert (w1 :: l1 ≠ nil) by (introv Hyp; inverts Hyp).
  assert (w0 :: l2 ≠ nil) by (introv Hyp; inverts Hyp).
  specializes¬ H H1. rewrite wfp_prod_cons. automate.
Qed.

Lemma wfp_size_ordered_le : ∀ p, wfp_size (ordered p) ≤ wfp_size p.
Proof with (try solve [introv HH; inverts HH]; automate).
  induction p using (measure_induction wfp_size); destruct_wf p;
  unfolds ordered; unfolds get_components; simpl_gets; simpls; try nat_math.

  assert (Hp1 : wfp_size p1 < wfp_size (wfp_Par p1 p2)) by automate.
  assert (Hp2 : wfp_size p2 < wfp_size (wfp_Par p1 p2)) by automate.
  apply H in Hp1. apply H in Hp2. clear H.

  destruct (get_vars p1); destruct (get_vars p2); destruct (get_outs p1);
  destruct (get_outs p2); destruct (get_ins p1); destruct (get_ins p2);
  repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *;
  try solve [automate];
  try solve [repeat (rewrite wfp_size_wfp_prod_lt in *; try solve [introv HH; inverts HH]); simpls; automate].
Qed.

Lemma IObis_cancellation_stronger : ∀ p q r s,
  wfp_Par p r ≈ wfp_Par q s → r ≈ s → p ≈ q.
Proof.
  introv Hio1 Hio2.
  apply IObis_cancellation with (r := r). etransitivity. eassumption.
  applys¬ IObis_congr_par.
Qed.

Lemma has_top_nil_wfp_prod_app : ∀ l1 l2,
  has_top_nil (wfp_prod (l1 ++ l2)) ↔
    match l1 with
     | nil ⇒ has_top_nil (wfp_prod l2)
     | _ ⇒ (has_top_nil (wfp_prod l1)) ∨ match l2 with
                                              | nil ⇒ False
                                              | _ ⇒ has_top_nil (wfp_prod l2)
                                             end
    end.
Proof.
  induction l1 using (measure_induction length); destruct l1.
  clear H. introv; rewrite app_nil_l. intuition.
  destruct l2. rewrite app_nil_r. intuition.
  destruct l1. repeat rewrite app_cons. repeat rewrite app_nil_l.
  rewrite wfp_prod_cons. simpl (wfp_prod (w :: nil)). simpl_has_top_nil. intuition.
  repeat rewrite app_cons. repeat rewrite wfp_prod_cons.
  simpl_has_top_nil. specializes H (w1 :: l1) (w0 :: l2). rew_length; nat_math.
Qed.

Lemma has_top_nil_get_vars : ∀ p, wfp_sizeP p = 0 → get_vars p = nil.
Proof.
  induction p using (measure_induction wfp_size); introv Hs.
  destruct_wf p; simpl_gets; auto; try solve [false; automate].
  do 2 (rewrite H; automate).
Qed.

Lemma has_top_nil_get_outs : ∀ p, wfp_sizeP p = 0 → get_outs p = nil.
Proof.
  induction p using (measure_induction wfp_size); introv Hs.
  destruct_wf p; simpl_gets; auto; try solve [false; automate].
  do 2 (rewrite H; automate).
Qed.

Lemma has_top_nil_get_ins : ∀ p, wfp_sizeP p = 0 → get_ins p = nil.
Proof.
  induction p using (measure_induction wfp_size); introv Hs.
  destruct_wf p; simpl_gets; auto; try solve [false; automate].
  do 2 (rewrite H; automate).
Qed.

Lemma has_top_nil_ordered : ∀ p, has_top_nil (ordered p) ↔ wfp_sizeP p = 0.
Proof.
  induction p using (measure_induction wfp_size).
  destruct_wf p; unfolds ordered; unfolds get_components;
  simpl_gets; simpl_has_top_nil; repeat rewrite app_nil_l in *;
  repeat rewrite app_nil_r in *; try solve [simpls; simpl_has_top_nil;
  splits; introv Hyp; intuition; unfolds wfp_sizeP; simpls; nat_math].

  assert (Hp1 : wfp_size p1 < wfp_size (wfp_Par p1 p2)) by automate.
  assert (Hp2 : wfp_size p2 < wfp_size (wfp_Par p1 p2)) by automate.
  apply H in Hp1. apply H in Hp2. clear H.
  tests Hyp1 : (wfp_sizeP p1 = 0); tests Hyp2 : (wfp_sizeP p2 = 0).

  lets Hp1v : has_top_nil_get_vars Hyp1.
  lets Hp1o : has_top_nil_get_outs Hyp1.
  lets Hp1i : has_top_nil_get_ins Hyp1.
  lets Hp2v : has_top_nil_get_vars Hyp2.
  lets Hp2o : has_top_nil_get_outs Hyp2.
  lets Hp2i : has_top_nil_get_ins Hyp2.
  rewrite Hp1v, Hp1o, Hp1i, Hp2v, Hp2o, Hp2i; repeat rewrite app_nil_l.
  simpls; simpl_has_top_nil. splits; intros Hyp; intuition. automate.

  lets Hp1v : has_top_nil_get_vars Hyp1.
  lets Hp1o : has_top_nil_get_outs Hyp1.
  lets Hp1i : has_top_nil_get_ins Hyp1.
  rewrite Hp1v, Hp1o, Hp1i. repeat rewrite app_nil_l. rewrite Hp2.
  splits; introv Hyp; intuition. automate.

  lets Hp2v : has_top_nil_get_vars Hyp2.
  lets Hp2o : has_top_nil_get_outs Hyp2.
  lets Hp2i : has_top_nil_get_ins Hyp2.
  rewrite Hp2v, Hp2o, Hp2i. repeat rewrite app_nil_r. rewrite Hp1.
  splits; introv Hyp; intuition. automate.

  assert (H0 : wfp_sizeP (wfp_Par p1 p2) = 0 ↔ False) by automate.
  assert (H1 : wfp_sizeP p1 = 0 ↔ False) by automate.
  assert (H2 : wfp_sizeP p2 = 0 ↔ False) by automate.
  rewrite H0; rewrite H1 in Hp1; rewrite H2 in Hp2; clear H0 H1 H2.

  assert (H1 : ¬ has_top_nil (wfp_prod (get_vars p1 ++ get_outs p1 ++ get_ins p1))).
  intuition. clear Hp1.
  assert (H2 : ¬ has_top_nil (wfp_prod (get_vars p2 ++ get_outs p2 ++ get_ins p2))).
  intuition. clear Hp2.
  splits; introv Hyp; try solve [intuition].

  destruct (get_vars p1); destruct (get_vars p2); destruct (get_outs p1);
  destruct (get_outs p2); destruct (get_ins p1); destruct (get_ins p2);
  repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *;
  repeat rewrite app_cons in *; try solve [intuition];
  try solve [repeat (rewrite <- app_cons in *; rewrite has_top_nil_wfp_prod_app in × ); intuition].
Qed.

Lemma ordered_par_nil_l : ∀ p q, wfp_sizeP p = 0 → ordered (wfp_Par p q) = ordered q.
Proof.
  introv Hyp; unfolds ordered; unfolds get_components; simpl_gets.
  rewrite¬ has_top_nil_get_ins; rewrite¬ has_top_nil_get_outs;
  rewrite¬ has_top_nil_get_vars.
Qed.

Lemma ordered_par_nil_r : ∀ p q, wfp_sizeP q = 0 → ordered (wfp_Par p q) = ordered p.
Proof.
  introv Hyp; unfolds ordered; unfolds get_components; simpl_gets.
  rewrite¬ (has_top_nil_get_ins q); rewrite¬ (has_top_nil_get_outs q);
  rewrite¬ (has_top_nil_get_vars q). repeat rewrite¬ app_nil_r.
Qed.

Lemma dpd_wfp_prod_app :
  ∀ l1, (Forall (fun p ⇒ wfp_sizeP p > 0) l1) →
     ∀ l2, (Forall (fun p ⇒ wfp_sizeP p > 0) l2) →
       (dpd (wfp_prod (l1 ++ l2)) ↔ dpd (wfp_prod l1) ∧ dpd (wfp_prod l2)).
Proof.
  induction l1 using (measure_induction length); destruct l1.
    + introv Hl1 Hl2; rewrite app_nil_l. simpl; simpl_dpd. intuition.
    + introv; destruct l1; repeat (try rewrite app_cons; try rewrite app_nil_l).
      - destruct l2; introv Hl2.
          × simpl; simpl_dpd. intuition.
          × rewrite app_cons. rewrite app_nil_l. rewrite wfp_prod_cons.
            simpl (wfp_prod (w :: nil)).
            splits; introv Hyp; simpl_dpd; jauto. splits×.
              inverts¬ H0. destruct l2. simpls. inverts¬ Hl2.
              rewrite wfp_prod_cons. inverts Hl2. automate.
      - introv Hl1 Hl2. specializes H (w0 :: l1) l2. rew_length; nat_math.
        inverts¬ Hl1. specializes H Hl2. repeat rewrite app_cons.
        repeat rewrite wfp_prod_cons; splits; introv Hyp; simpl_dpd.
          × inverts Hyp. rewrite and_assoc. repeat splits×.
            inverts¬ Hl1. inverts H5. destruct l1. simpls¬.
            rewrite wfp_prod_cons. automate.
          × inverts Hyp. inverts H0. splits×.
            inverts Hl1. inverts H6. destruct (l1 ++ l2).
            simpls¬. rewrite wfp_prod_cons; automate.
Qed.

Lemma ordered_dpd_invariant : ∀ p, dpd p → dpd (ordered p).
Proof.
  induction p using (measure_induction wfp_size); destruct_wf p;
  unfolds ordered; unfolds get_components; simpl_gets;
  repeat rewrite app_nil_l; repeat rewrite app_nil_r; simpl; repeat simpl_dpd;
  try solve [intuition].

  + introv (Hsp1 & Hsp2 & Hdp1 & Hdp2). repeat rewrite app_assoc.
    apply H in Hdp1; solve_wfp_size. apply H in Hdp2; solve_wfp_size.

    repeat (rewrite dpd_wfp_prod_app in *;
    try solve [repeat (try apply Forall_app; try apply get_vars_sizeP;
               try apply get_outs_sizeP; try apply get_ins_sizeP)]; intuition).
Qed.

Lemma normal_form_wfp_prod_app : ∀ l1 l2,
  (Forall (fun p ⇒ wfp_sizeP p > 0) l1) →
  (Forall (fun p ⇒ wfp_sizeP p > 0) l2) →
  (normal_form (wfp_prod (l1 ++ l2)) ↔ normal_form (wfp_prod l1) ∧ normal_form (wfp_prod l2)).
Proof.
  induction l1 using (measure_induction length); destruct l1; introv Hl1 Hl2.
    + rewrite app_nil_l in ×. simpl. intuition.
    + destruct l1; repeat (try rewrite app_cons; try rewrite app_nil_l).
      - destruct l2.
          × simpl. intuition.
          × rewrite wfp_prod_cons. simpl (wfp_prod (w :: nil)). splits; introv Hyp.
              inverts Hyp; subst_wfp. constructor×. inverts¬ Hl1.
              inverts Hl2. destruct l2; simpl; simpl_sizes; nat_math.
      - specializes H (w0 :: l1) l2. rew_length; nat_math.
        inverts Hl1. specializes H H3 Hl2.
        repeat rewrite wfp_prod_cons; splits; introv Hyp; rewrite <- app_cons in ×.
          × remember (wfp_prod ((w0 :: l1) ++ l2)) as r. inverts Hyp; subst_wfp.
            rewrite H in H7; splits×. constructor×.
            rewrite wfp_prod_cons_wfp_sizeP. inverts H3. nat_math.
          × inverts Hyp. remember (wfp_prod (w0 :: l1)) as r.
            inverts H0; subst_wfp.
            constructor×. inverts H3.
            rewrite app_cons. rewrite wfp_prod_cons_wfp_sizeP. nat_math.
Qed.

Lemma ordered_nf_invariant : ∀ p, normal_form p → normal_form (ordered p).
Proof.
  induction p using (measure_induction wfp_size); destruct_wf p;
  unfolds ordered; unfolds get_components; simpl_gets;
  repeat rewrite app_nil_l; repeat rewrite app_nil_r;
  try solve [simpl; intuition].

  + introv Hyp; inverts Hyp; subst_wfp.
    apply H in H4; solve_wfp_size. apply H in H5; solve_wfp_size.

    repeat (rewrite normal_form_wfp_prod_app in *;
    try solve [repeat (try apply Forall_app; try apply get_vars_sizeP;
               try apply get_outs_sizeP; try apply get_ins_sizeP)]; intuition).
Qed.

Lemma wfp_prod_app_wfp_sizeP : ∀ l1 l2,
  wfp_sizeP (wfp_prod (l1 ++ l2)) = wfp_sizeP (wfp_prod l1) + wfp_sizeP (wfp_prod l2).
Proof.
  induction l1 using (measure_induction length); destruct l1.
    + introv; simpls. rewrite¬ app_nil_l.
    + destruct l1; introv; repeat rewrite app_cons.
      - repeat rewrite app_nil_l.
        rewrite wfp_prod_cons_wfp_sizeP. simpls¬.
      - repeat rewrite wfp_prod_cons. rewrite <- app_cons.
        unfolds wfp_sizeP. remember (w0 :: l1) as l. simpl.
        rewrite <- plus_assoc. fequals. apply H. rew_length; nat_math.
Qed.

Lemma wfp_sizeP_ordered_eq : ∀ p,
  wfp_sizeP (ordered p) = wfp_sizeP p.
Proof with automate.
  unfolds ordered; unfolds get_components.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpl_gets; repeat rewrite app_nil_l;
  repeat rewrite app_nil_r; try solve [simpls*].

  lets H1 : H p1; lets H2 : H p2.
  repeat rewrite wfp_prod_app_wfp_sizeP in ×.
  unfolds wfp_sizeP; simpls.
  rewrite <- H1...
Qed.

Fixpoint num_of_pars (p : process) :=
match p with
  | Par p1 p2 ⇒ S (num_of_pars p1 + num_of_pars p2)
  | _ ⇒ 0
end.

Definition wfp_num_of_pars (p : wfprocess) :=
  num_of_pars (proc p).

Lemma num_of_pars_wfp_prod_app_comm : ∀ l1 l2,
  num_of_pars (wfp_prod (l1 ++ l2)) = num_of_pars (wfp_prod (l2 ++ l1)).
Proof.
  induction l1 using (measure_induction length).
  destruct l1. introv; rewrite app_nil_l; rewrite¬ app_nil_r.
  destruct l2. rewrite app_nil_l; rewrite¬ app_nil_r.
  repeat rewrite app_cons.

  replace (wfp_prod (w :: l1 ++ w0 :: l2)) with (wfp_Par w (wfp_prod (l1 ++ w0 :: l2))).
  Focus 2. clear. simpls. destruct l1; destruct l2;
  repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *;
  repeat rewrite app_cons in *; auto.
  replace (wfp_prod (w0 :: l2 ++ w :: l1)) with (wfp_Par w0 (wfp_prod (l2 ++ w :: l1))).
  Focus 2. clear. simpls. destruct l1; destruct l2;
  repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *;
  repeat rewrite app_cons in *; auto.

  rewrite app_last; rewrite (app_last w). simpl num_of_pars. fequals.

Lemma num_of_pars_aux_1 : ∀ l1 w l2, num_of_pars (wfp_prod (l1 & w ++ l2)) =
  num_of_pars (wfp_prod (w :: l1 ++ l2)).
Proof.
  induction l1 using (measure_induction length).
  destruct l1. introv; rewrite app_nil_l in ×. rewrite¬ app_cons.
  introv. rewrite <- app_last. rewrite app_cons. rewrite app_last.
  replace (wfp_prod (w :: l1 & w0 ++ l2)) with (wfp_Par w (wfp_prod (l1 & w0 ++ l2))).
  Focus 2. clear. simpls. destruct l1; destruct l2;
  repeat rewrite app_nil_l in *; repeat rewrite app_nil_r in *;
  repeat rewrite app_cons in *; auto.
  simpl num_of_pars at 1. rewrite H. Focus 2. rew_length; nat_math.
  rewrite app_cons. replace (num_of_pars (wfp_prod (w0 :: w :: l1 ++ l2))) with
  (num_of_pars (wfp_prod (w :: w0 :: l1 ++ l2))). simpls¬.
  clear. remember (l1 ++ l2) as l. clear. destruct l.
  simpls; nat_math. repeat rewrite wfp_prod_cons; simpls; nat_math.
Qed.

  do 2 rewrite num_of_pars_aux_1.
  destruct l1; destruct l2; repeat rewrite app_nil_l;
  repeat rewrite app_nil_r. simpl; nat_math.
  repeat rewrite wfp_prod_cons; simpl; nat_math.
  repeat rewrite wfp_prod_cons; simpl; nat_math.
  replace (wfp_prod (w0 :: (w1 :: l1) ++ w2 :: l2)) with
          (wfp_Par w0 (wfp_prod ((w1 :: l1) ++ (w2 :: l2)))).
  replace (wfp_prod (w :: (w2 :: l2) ++ w1 :: l1)) with
          (wfp_Par w (wfp_prod ((w2 :: l2) ++ (w1 :: l1)))).
  specializes H (w1 :: l1) (w2 :: l2). rew_length; nat_math.
  simpls; nat_math.

  destruct l1; destruct l2; repeat rewrite app_cons;
  repeat rewrite app_nil_l; repeat rewrite app_nil_r; simpls¬.
  destruct l1; destruct l2; repeat rewrite app_cons;
  repeat rewrite app_nil_l; repeat rewrite app_nil_r; simpls¬.
Qed.

Lemma num_of_pars_wfp_prod_app : ∀ l1 l2,
  num_of_pars (wfp_prod (l1 ++ l2)) ≤ S (num_of_pars (wfp_prod l1) + num_of_pars (wfp_prod l2)).
Proof.
  induction l1 using (measure_induction length); destruct l1.
  introv; rewrite app_nil_l. simpls; nat_math.

  destruct l1. introv; rewrite app_cons. rewrite app_nil_l.
  simpl (wfp_prod (w :: nil)). clear. gen w.
  induction l2 using (measure_induction length). destruct l2.
  simpls; nat_math.
  introv; rewrite wfp_prod_cons. destruct l2. simpls; nat_math.
  repeat rewrite wfp_prod_cons. specializes H (w1 :: l2) w. rew_length; nat_math.
  rewrite wfp_prod_cons in H. simpls; nat_math.

  introv. repeat rewrite app_cons. rewrite wfp_prod_cons.
  specializes H (w0 :: l1) l2. rew_length. nat_math.
  rewrite wfp_prod_cons. rewrite app_cons in ×. simpls; nat_math.
Qed.

Lemma num_of_pars_wfp_prod_app_eq : ∀ l1 l2, l1 ≠ nil → l2 ≠ nil →
  num_of_pars (wfp_prod (l1 ++ l2)) = S (num_of_pars (wfp_prod l1) + num_of_pars (wfp_prod l2)).
Proof.
  induction l1 using (measure_induction length); destruct l1.
  introv; rewrite app_nil_l. intros; false×.

  destruct l1. introv; rewrite app_cons. rewrite app_nil_l.
  simpl (wfp_prod (w :: nil)). clear. intros _; gen w.
  induction l2 using (measure_induction length). destruct l2.
  intros; false×.
  introv _; rewrite wfp_prod_cons. destruct l2. simpls; nat_math.
  repeat rewrite wfp_prod_cons. specializes H (w1 :: l2) w. rew_length; nat_math.

  introv _ Hl2. repeat rewrite app_cons. rewrite wfp_prod_cons.
  specializes H (w0 :: l1) l2 Hl2. rew_length. nat_math. intro Hyp; inverts Hyp.
  rewrite wfp_prod_cons. rewrite app_cons in ×. simpls; nat_math.
Qed.

Lemma num_of_pars_cancel_f : ∀ l l1 l2, l1 ≠ nil → l2 ≠ nil →
  (num_of_pars (wfp_prod (l ++ l1)) = num_of_pars (wfp_prod (l ++ l2)) ↔
  num_of_pars (wfp_prod l1) = num_of_pars (wfp_prod l2)).
Proof.
  induction l using (measure_induction length); destruct l.
    + introv Hl1 Hl2; repeat rewrite app_nil_l; intuition.
    + destruct l.
      - introv Hl1 Hl2; repeat rewrite app_cons; repeat rewrite app_nil_l.
        clear H. gen Hl1 l2 w. destruct l1; destruct l2;
        repeat rewrite app_nil_l; repeat rewrite app_nil_r; intuition.
          rewrite wfp_prod_cons in ×. simpls. nat_math.
          repeat rewrite wfp_prod_cons. simpls. nat_math.
      - introv Hl1 Hl2; repeat rewrite app_cons; repeat rewrite wfp_prod_cons.
        specializes H (w0 :: l) Hl1 Hl2. rew_length; nat_math.
        repeat rewrite <- app_cons. simpls; nat_math.
Qed.

Lemma num_of_pars_cancel_b : ∀ l l1 l2, l1 ≠ nil → l2 ≠ nil →
  (num_of_pars (wfp_prod (l1 ++ l)) = num_of_pars (wfp_prod (l2 ++ l)) ↔
  num_of_pars (wfp_prod l1) = num_of_pars (wfp_prod l2)).
Proof.
  introv Hl1 Hl2. do 2 rewrite num_of_pars_wfp_prod_app_comm with (l2 := l).
  applys¬ num_of_pars_cancel_f.
Qed.

Lemma num_of_pars_ordered_par : ∀ p1 p2,
  num_of_pars (ordered (wfp_Par p1 p2)) ≤ S (num_of_pars (ordered p1) + num_of_pars (ordered p2)).
Proof.
  unfolds ordered; unfolds get_components; introv; simpl_gets.
  replace (num_of_pars
     (wfp_prod
        ((get_vars p1 ++ get_vars p2) ++
         (get_outs p1 ++ get_outs p2) ++ get_ins p1 ++ get_ins p2))) with
    (num_of_pars
          (wfp_prod
             ((get_vars p1 ++ get_outs p1 ++ get_ins p1) ++
              get_vars p2 ++ get_outs p2 ++ get_ins p2))).
  apply num_of_pars_wfp_prod_app.

 Ltac rew_tactic_f := let H := fresh "H" in
    (rewrite× num_of_pars_cancel_f; try solve [repeat rewrite app_cons; intros H; inverts H]).

  Ltac rew_tactic_b := let H := fresh "H" in
    (rewrite× num_of_pars_cancel_b; try solve [repeat rewrite app_cons; intros H; inverts H]).

  Ltac rew_tactic_f2 := repeat (rewrite× num_of_pars_wfp_prod_app_comm; rewrite app_assoc; rew_tactic_f).

  Ltac back_to_front := repeat rewrite <- app_assoc; rewrite num_of_pars_wfp_prod_app_comm; repeat rewrite× app_assoc.

  Ltac rew_cancel := repeat rewrite app_assoc; repeat rew_tactic_f; auto;
                     repeat rewrite <- app_assoc; repeat rew_tactic_b; auto;
                     repeat rewrite app_assoc;
                     try solve [rewrite¬ num_of_pars_wfp_prod_app_comm];
                     try solve [rew_tactic_f2]; try solve [back_to_front].

  destruct (get_vars p1); destruct (get_vars p2); destruct (get_outs p1);
  destruct (get_outs p2); destruct (get_ins p1); destruct (get_ins p2);
  repeat (try rewrite app_cons; try rewrite app_nil_l; try rewrite app_nil_r); auto;
  repeat rewrite <- app_cons; rew_cancel; do 2 back_to_front; rew_cancel.
Qed.

Lemma num_of_pars_ordered_par_eq : ∀ p1 p2,
  wfp_sizeP p1 > 0 → wfp_sizeP p2 > 0 → num_of_pars (ordered (wfp_Par p1 p2)) = S (num_of_pars (ordered p1) + num_of_pars (ordered p2)).
Proof.
  introv Hsp1 Hsp2. lets Hcgr1 : ordered_wfcgr p1. lets Hcgr2 : ordered_wfcgr p2.
  unfolds ordered; unfolds get_components; introv; simpl_gets.
  replace (num_of_pars
     (wfp_prod
        ((get_vars p1 ++ get_vars p2) ++
         (get_outs p1 ++ get_outs p2) ++ get_ins p1 ++ get_ins p2))) with
    (num_of_pars
          (wfp_prod
             ((get_vars p1 ++ get_outs p1 ++ get_ins p1) ++
              get_vars p2 ++ get_outs p2 ++ get_ins p2))).

  apply num_of_pars_wfp_prod_app_eq.

  destruct (get_vars p1); destruct (get_outs p1); destruct (get_ins p1);
  repeat rewrite app_nil_l; repeat rewrite app_nil_r;
  try solve [intro Hyp; inverts Hyp]. false; simpls.
  assert (p1 ≈ wfp_Nil).
    ∃ wfcgr; splits×. apply congr_IObisimulation.
  rewrite <- wfp_sizeP_0_IO_nil in H. nat_math.

  destruct (get_vars p2); destruct (get_outs p2); destruct (get_ins p2);
  repeat rewrite app_nil_l; repeat rewrite app_nil_r;
  try solve [intro Hyp; inverts Hyp]. false; simpls.
  assert (p2 ≈ wfp_Nil).
    ∃ wfcgr; splits×. apply congr_IObisimulation.
  rewrite <- wfp_sizeP_0_IO_nil in H. nat_math.

  destruct (get_vars p1); destruct (get_vars p2); destruct (get_outs p1);
  destruct (get_outs p2); destruct (get_ins p1); destruct (get_ins p2);
  repeat (try rewrite app_cons; try rewrite app_nil_l; try rewrite app_nil_r); auto;
  repeat rewrite <- app_cons; rew_cancel; do 2 back_to_front; rew_cancel.
Qed.

Lemma num_of_pars_ordered_le : ∀ p, num_of_pars (ordered p) ≤ num_of_pars p.
Proof.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpls; try nat_math.

  assert (H1 : wfp_size p1 < wfp_size (wfp_Par p1 p2)) by automate.
  assert (H2 : wfp_size p2 < wfp_size (wfp_Par p1 p2)) by automate.
  apply H in H1. apply H in H2. clear H.
  lets Hyp : num_of_pars_ordered_par p1 p2. nat_math.
Qed.

Lemma has_top_nil_sizeP_0 : ∀ p, wfp_sizeP p = 0 → has_top_nil p.
Proof.
  induction p using (measure_induction wfp_size); destruct_wf p;
  unfolds wfp_sizeP; simpls; simpl_has_top_nil; auto; introv Hyp;
  try solve [false; nat_math].
  assert (sizeP p1 = 0) by nat_math.
  left; applys¬ H. automate.
Qed.

Lemma has_top_nil_num_of_pars_ordered : ∀ p,
  has_top_nil p ↔ (wfp_sizeP p = 0 ∨ num_of_pars (ordered p) < num_of_pars p).
Proof.
  induction p using (measure_induction wfp_num_of_pars).
  destruct_wf p; simpl_has_top_nil; unfolds wfp_sizeP; simpls;
  try solve [intuition; try nat_math; try inverts× H1]. splits; intro Hyp.

  assert (Hp1 : wfp_num_of_pars p1 < wfp_num_of_pars (wfp_Par p1 p2)) by
    (unfolds wfp_num_of_pars; simpls; nat_math).
  assert (Hp2 : wfp_num_of_pars p2 < wfp_num_of_pars (wfp_Par p1 p2)) by
    (unfolds wfp_num_of_pars; simpls; nat_math).
  apply H in Hp1. apply H in Hp2.
  lets Hpar : num_of_pars_ordered_par p1 p2.
  lets Hnill : ordered_par_nil_l. lets Hnilr : ordered_par_nil_r. unfolds wfp_sizeP.
  tests H1 : (has_top_nil p1); tests H2 : (has_top_nil p2);
  try solve [false*]; clear Hyp; rewrite Hp1 in H1; rewrite Hp2 in H2;
  clear Hp1 Hp2.

  tests Hn1 : (sizeP p1 = 0); tests Hn2 : (sizeP p2 = 0);
  try solve [left; nat_math]; right.
  apply Hnill with (q := p2) in Hn1. rewrite Hn1.
  inverts H2; try solve [false*]; nat_math.
  apply Hnilr with (p := p1) in Hn2. rewrite Hn2.
  inverts H1; try solve [false*]; nat_math.
  inverts H1; try solve [false*]; inverts H2; try solve [false*]; nat_math.

  rew_logic in H2; destruct H2 as (H2 & H3).
  assert (Heq_p2 : num_of_pars (ordered p2) = num_of_pars p2).
    lets Hyp : num_of_pars_ordered_le p2. nat_math. clear H3.
  tests Hn1 : (sizeP p1 = 0); right.
  apply Hnill with (q := p2) in Hn1. rewrite Hn1 in *; nat_math.
  inverts H1; try solve [false*]. nat_math.

  rew_logic in H1; destruct H1 as (H1 & H3).
  assert (Heq_p1 : num_of_pars (ordered p1) = num_of_pars p1).
    lets Hyp : num_of_pars_ordered_le p1. nat_math. clear H3.
  tests Hn1 : (sizeP p2 = 0); right.
  apply Hnilr with (p := p1) in Hn1. rewrite Hn1 in *; nat_math.
  inverts H2; try solve [false*]. nat_math.

  inverts Hyp as Hyp.

  left; apply has_top_nil_sizeP_0. automate.

  assert (Hp1 : wfp_num_of_pars p1 < wfp_num_of_pars (wfp_Par p1 p2)) by
    (unfolds wfp_num_of_pars; simpls; nat_math).
  assert (Hp2 : wfp_num_of_pars p2 < wfp_num_of_pars (wfp_Par p1 p2)) by
    (unfolds wfp_num_of_pars; simpls; nat_math).
  lets Hp1´ : H Hp1. lets Hp2´ : H Hp2.
  tests Hn1 : (has_top_nil p1); tests Hn2 : (has_top_nil p2); jauto.

  unfolds wfp_num_of_pars. false.
  rewrite Hp1´ in Hn1; rewrite Hp2´ in Hn2. clear Hp1´ Hp2´.
  rew_logic in ×. destruct Hn1; destruct Hn2.
  assert (Heq_p1 : num_of_pars (ordered p1) = num_of_pars p1).
    lets H4 : num_of_pars_ordered_le p1. nat_math.
  assert (Heq_p2 : num_of_pars (ordered p2) = num_of_pars p2).
    lets H4 : num_of_pars_ordered_le p2. nat_math. clear H1 H3.

  cut (num_of_pars (ordered (wfp_Par p1 p2)) = S (num_of_pars p1 + num_of_pars p2)).
  introv; nat_math.

  clear H Hyp. rewrite <- Heq_p1. rewrite <- Heq_p2. clear Heq_p1 Heq_p2 Hp1 Hp2.
  apply num_of_pars_ordered_par_eq; automate.
Qed.

Lemma num_of_pars_ordered : ∀ p, wfp_num_of_pars (ordered p) = 0 → ¬ has_top_nil p → p = ordered p.
Proof.
  induction p using (measure_induction wfp_size).
  destruct_wf p; try solve [unfolds ordered; unfolds get_components; simpl_gets;
  repeat rewrite app_nil_l; repeat rewrite app_nil_r; jauto].

  lets Hyp : has_top_nil_ordered.

  unfolds wfp_num_of_pars. simpl_has_top_nil. introv Hnum Hnil.
  rew_logic in Hnil; destruct Hnil as (Hnil1 & Hnil2).

  rewrite has_top_nil_num_of_pars_ordered in ×. rew_logic in ×.
  destruct Hnil1; destruct Hnil2.
  assert (Heq_p1 : num_of_pars (ordered p1) = num_of_pars p1).
    lets H4 : num_of_pars_ordered_le p1. nat_math.
  assert (Heq_p2 : num_of_pars (ordered p2) = num_of_pars p2).
    lets H4 : num_of_pars_ordered_le p2. nat_math. clear H1 H3.

  lets Hyp´ : num_of_pars_ordered_par_eq.
  assert (Hsp1 : wfp_sizeP p1 > 0) by nat_math.
  assert (Hsp2 : wfp_sizeP p2 > 0) by nat_math.
  specializes Hyp´ Hsp1. specializes Hyp´ Hsp2.
  rewrite Hnum in Hyp´. false; nat_math.
Qed.

Lemma num_of_pars_eq : ∀ p, ¬ has_top_nil p → num_of_pars p = num_of_pars (ordered p).
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpls¬.

  simpl_has_top_nil; introv Hyp. rew_logic in Hyp.
  destruct Hyp as (Hp1 & Hp2).
  lets Hp1´ : H Hp1... lets Hp2´ : H Hp2...

  rewrite has_top_nil_num_of_pars_ordered in ×. rew_logic in ×.
  destruct Hp1; destruct Hp2.
  symmetry. rewrite Hp1´, Hp2´. apply num_of_pars_ordered_par_eq; nat_math.
Qed.



Lemma IObis_abs_inv_ch : ∀ a X p b Y q,
  wfp_Abs a X p ≈ wfp_Abs b Y q → a = b.
Proof.
  introv Hio.

  lets Htl : TrIn a X p.
  lets (fq & Htr & _) : IObis_in Hio Htl.
  apply wfp_trans_in_chan_eq in Htr. auto.
Qed.

Lemma IObis_abs_inv_var : ∀ a X p Y q,
  wfp_Abs a X p ≈ wfp_Abs a Y q → ∃ r, wfp_Abs a Y q = wfp_Abs a X r.
Proof.
  introv Hio.

  tests Heq : (Y = X).

  + ∃¬ q.
  + ∃ (wfp_subst (wfp_Gvar X) Y q).
    apply wfp_Abs_eq. lets Hf : gfresh_IObis X Hio.
    do 2 rewrite wfp_gfresh_Abs in ×. intuition.
Qed.

Lemma IObis_abs_inv_body : ∀ a X p q,
  wfp_Abs a X p ≈ wfp_Abs a X q → p ≈ q.
Proof.
  introv Hio.

  lets Htl : TrIn a X p.
  lets (fq & Htr & Hio´) : IObis_in_full Hio Htl.
  apply wfp_trans_in_abs_eq in Htr. specializes Hio´ X. inverts Htr as Htr.

  + simpls. repeat rewrite wfp_subst_gvar_idem in *; auto.
  + destruct Htr as (Y & Hneq & Hf & Heq). subst.
    simpls. rewrite <- wfp_subst_decomposition_g in Hio´; auto.
    repeat rewrite wfp_subst_gvar_idem in *; auto.
Qed.

Lemma abs_not_prime : ∀ a X p, ¬ prime (wfp_Abs a X p) →
  ∃ n p´, n > 1 ∧
    wfp_Abs a X p ≈ wfp_prod (wfp_repeat n (wfp_Abs a X p´)) ∧
      normal_form (wfp_Abs a X p´).
Proof with automate.
  introv Hnp. unfold prime in Hnp. rew_logic in Hnp. inverts Hnp as Hio_par.
  apply IObis_sizeP_eq in Hio_par. simpl_sizes. nat_math.

  destruct Hio_par as (p1 & Hio_par). rew_logic in ×.
  destruct Hio_par as (p2 & Hio_par). rew_logic in ×.
  destruct Hio_par as (Hio_par & Hnp1 & Hnp2).

  lets (dp1 & Hio_p1 & Hd_p1) : deep_prime_decomposition_exists p1.
  lets (dp2 & Hio_p2 & Hd_p2) : deep_prime_decomposition_exists p2.

  assert (Hs_p1 : wfp_sizeP (ordered dp1) > 0).
    rewrite <- wfp_sizeP_0_IO_nil in Hnp1.
    apply IObis_sizeP_eq in Hio_p1. rewrite wfp_sizeP_ordered_eq. nat_math.

  assert (Hs_p2 : wfp_sizeP (ordered dp2) > 0).
    rewrite <- wfp_sizeP_0_IO_nil in Hnp2.
    apply IObis_sizeP_eq in Hio_p2. rewrite wfp_sizeP_ordered_eq. nat_math.

  assert (Hio_main : wfp_Abs a X p ≈ wfp_Par dp1 dp2).
    etransitivity. eassumption. applys¬ IObis_congr_par.

  clear dependent p1. clear dependent p2.

  lets Hn_p1 : dpd_normal_form Hd_p1. apply ordered_nf_invariant in Hn_p1.
  lets Hn_p2 : dpd_normal_form Hd_p2. apply ordered_nf_invariant in Hn_p2.

  assert (Hgv_dp1 : get_vars dp1 = nil).
  {
    lets Hspec : get_vars_spec dp1.
    destruct (get_vars dp1); auto.
    false. lets (Y & Heq & (dp1´ & Hcgr)) : Hspec w. constructor¬.
    apply congr_IObis in Hcgr.

    lets Htr : TrRem Y. apply act1_rem with (p2 := dp1´) in Htr.
    lets Hio´ : IObis_var Htr. symmetry. eassumption.
    destruct Hio´ as (q´ & Htr´ & _).
    apply act1_rem with (p2 := dp2) in Htr´.
    lets Hio´´ : IObis_var Htr´. symmetry. eassumption.
    destruct Hio´´ as (q´´ & Htr´´ & _).
    inverts Htr´´.
  }

  assert (Hgv_dp2 : get_vars dp2 = nil).
  {
    lets Hspec : get_vars_spec dp2.
    destruct (get_vars dp2); auto.
    false. lets (Y & Heq & (dp2´ & Hcgr)) : Hspec w. constructor¬.
    apply congr_IObis in Hcgr.

    lets Htr : TrRem Y. apply act1_rem with (p2 := dp2´) in Htr.
    lets Hio´ : IObis_var Htr. symmetry. eassumption.
    destruct Hio´ as (q´ & Htr´ & _).
    apply act2_rem with (p1 := dp1) in Htr´.
    lets Hio´´ : IObis_var Htr´. symmetry. eassumption.
    destruct Hio´´ as (q´´ & Htr´´ & _).
    inverts Htr´´.
  }

  assert (Hgo_dp1 : get_outs dp1 = nil).
  {
    lets Hspec : get_outs_spec dp1.
    destruct (get_outs dp1); auto.
    false. lets (a0 & p0 & Heq & (dp1´ & Hcgr)) : Hspec w. constructor¬.
    apply congr_IObis in Hcgr.

    lets Htr : TrOut a0 p0. apply act1_out with (p2 := dp1´) in Htr.
    lets Hio´ : IObis_out Htr. symmetry. eassumption.
    destruct Hio´ as (q´ & q´´ & Htr´ & _).
    apply act1_out with (p2 := dp2) in Htr´.
    lets Hio´´ : IObis_out Htr´. symmetry. eassumption.
    destruct Hio´´ as (q´´´ & q´´´´ & Htr´´ & _).
    inverts Htr´´.
  }
  assert (Hgo_dp2 : get_outs dp2 = nil).
  {
    lets Hspec : get_outs_spec dp2.
    destruct (get_outs dp2); auto.
    false. lets (a0 & p0 & Heq & (dp2´ & Hcgr)) : Hspec w. constructor¬.
    apply congr_IObis in Hcgr.

    lets Htr : TrOut a0 p0. apply act1_out with (p2 := dp2´) in Htr.
    lets Hio´ : IObis_out Htr. symmetry. eassumption.
    destruct Hio´ as (q´ & q´´ & Htr´ & _).
    apply act2_out with (p1 := dp1) in Htr´.
    lets Hio´´ : IObis_out Htr´. symmetry. eassumption.
    destruct Hio´´ as (q´´´ & q´´´´ & Htr´´ & _).
    inverts Htr´´.
  }

  apply ordered_dpd_invariant in Hd_p1.
  apply ordered_dpd_invariant in Hd_p2.

  assert (Hio : wfp_Abs a X p ≈ wfp_Par (ordered dp1) (ordered dp2)).
    etransitivity. eassumption.
    apply IObis_congr_par; apply congr_IObis; apply ordered_wfcgr.

  clear Hio_main.

  unfolds ordered. unfolds get_components.
  rewrite Hgv_dp1, Hgv_dp2, Hgo_dp1, Hgo_dp2 in ×.
  repeat rewrite app_nil_l in ×.
  clear Hgv_dp1 Hgv_dp2 Hgo_dp1 Hgo_dp2.

  remember (get_ins dp1) as l1. remember (get_ins dp2) as l2.

  assert (Hs_l1 : Forall (fun p ⇒ wfp_sizeP p > 0) l1).
    subst. apply get_ins_sizeP.
  assert (Hs_l2 : Forall (fun p ⇒ wfp_sizeP p > 0) l2).
    subst. apply get_ins_sizeP.

  assert (Hn_l1 : Forall (fun p ⇒ normal_form p) l1).
    gen Hs_l1 Hn_p1. clear. inductions l1; intros.
    constructor. inverts Hs_l1. specializes IHl1 H2.
    destruct l1. simpls. constructor×.
    repeat rewrite wfp_prod_cons in ×.
    remember (wfp_prod (w :: l1)) as r. inverts Hn_p1...
    constructor×.

  assert (Hn_l2 : Forall (fun p ⇒ normal_form p) l2).
    gen Hs_l2 Hn_p2. clear. inductions l2; intros.
    constructor. inverts Hs_l2. specializes IHl2 H2.
    destruct l2. simpls. constructor×.
    repeat rewrite wfp_prod_cons in ×.
    remember (wfp_prod (w :: l2)) as r. inverts Hn_p2...
    constructor×.

  clear Hn_p1 Hn_p2.

Lemma components_wfp_prod : ∀ l1, Forall (fun p ⇒ wfp_sizeP p > 0) l1 →
  Forall (fun p ⇒ wfp_num_of_pars p = 0) l1 → components (wfp_prod l1) = l1.
Proof.
  induction l1 using (measure_induction length). destruct l1; introv Hs Hnp.

  + simpls; simpl_components; auto.

  + destruct l1.
    - simpls. destruct_wf w; simpl_components; auto.
      inverts Hnp. unfolds wfp_num_of_pars. simpls. nat_math.
      inverts Hs. solve_wfp_sizeP.
    - rewrite wfp_prod_cons. simpl_components.
      inverts Hs. inverts Hnp.
      replace w with (wfp_prod (w :: nil)).
      rewrite¬ H. rewrite¬ H. rew_length; nat_math.
      rew_length; nat_math. repeat constructor×.
      repeat constructor×.
      simpls¬.
Qed.

  assert (Hp_l1 : Forall (fun p ⇒ prime p) l1).
    lets Hyp : dpd_components_prime Hd_p1.
    rewrite components_wfp_prod in Hyp; auto.
    lets Hspec : get_ins_spec dp1; subst.
    rewrite <- Forall_Mem. introv Hm.
    specializes Hspec Hm. destruct Hspec as (a0 & X0 & p0 & Heq & _).
    subst; unfolds wfp_num_of_pars; simpls¬.

  assert (Hp_l2 : Forall (fun p ⇒ prime p) l2).
    lets Hyp : dpd_components_prime Hd_p2.
    rewrite components_wfp_prod in Hyp; auto.
    lets Hspec : get_ins_spec dp2; subst.
    rewrite <- Forall_Mem. introv Hm.
    specializes Hspec Hm. destruct Hspec as (a0 & X0 & p0 & Heq & _).
    subst; unfolds wfp_num_of_pars; simpls¬.

  clear Hd_p1 Hd_p2.

Lemma wfp_prod_fresh : ∀ X l1, X # wfp_prod l1 →
  Forall (fun (p : wfprocess) ⇒ X # p) l1.
Proof.
  inductions l1; introv Hyp. constructor.
    destruct l1. simpls. repeat constructor¬.
    rewrite wfp_prod_cons in ×. simpls; rewrite gfresh_par_iff in Hyp.
    constructor×.
Qed.

  assert (Hf_l1 : Forall (fun (p : wfprocess) ⇒ X # p) l1).
    apply wfp_prod_fresh. apply gfresh_IObis with (X := X) in Hio.
    simpls; fresh_solve. rewrite¬ wfp_gfresh_Abs.

  assert (Hf_l2 : Forall (fun (p : wfprocess) ⇒ X # p) l2).
    apply wfp_prod_fresh. apply gfresh_IObis with (X := X) in Hio.
    simpls; fresh_solve. rewrite¬ wfp_gfresh_Abs.

Lemma wfp_prod_in : ∀ l p, Mem p l → ∀ a fp,
  {{p -- LabIn a ->> AA fp}} → ∃ fl, {{wfp_prod l -- LabIn a ->> AA fl}}.
Proof.
  inductions l; introv Hm Ht. inverts Hm.
  inverts Hm. destruct l. simpls. eexists; eassumption.
  rewrite wfp_prod_cons. eexists. eapply act1_in; eassumption.
  specializes¬ IHl Ht.
  destruct l. simpls. inverts IHl. inverts H.
  rewrite wfp_prod_cons. inverts IHl. eexists. apply act2_in. eassumption.
Qed.

  assert (Hspec_l1 : Forall (fun p ⇒ ∃ p´, p = wfp_Abs a X p´) l1).
    lets Hspec : get_ins_spec dp1. rewrite <- Forall_Mem.
    introv Hm. subst; specializes Hspec Hm. destruct Hspec as (a0 & X0 & p0 & Heq & _).
    subst. cut (a0 = a). introv Hyp; subst.
    tests Heq : (X0 = X); eexists. reflexivity. eapply wfp_Abs_eq.
    rewrite <- Forall_Mem in Hf_l1. specializes Hf_l1 Hm.
    rewrite wfp_gfresh_Abs in Hf_l1. intuition.
    lets Ht : TrIn a0 X0 p0. apply wfp_prod_in with (l := get_ins dp1) in Ht; auto.
    destruct Ht as (fl & Ht). apply act1_in with (p2 := (wfp_prod (get_ins dp2))) in Ht.
    eapply IObis_in_full in Ht. Focus 2. symmetry. eassumption.
    destruct Ht as (fq & Ht & _). apply wfp_trans_in_chan_eq in Ht; auto.

  assert (Hspec_l2 : Forall (fun p ⇒ ∃ p´, p = wfp_Abs a X p´) l2).
    lets Hspec : get_ins_spec dp2. rewrite <- Forall_Mem.
    introv Hm. subst; specializes Hspec Hm. destruct Hspec as (a0 & X0 & p0 & Heq & _).
    subst. cut (a0 = a). introv Hyp; subst.
    tests Heq : (X0 = X); eexists. reflexivity. eapply wfp_Abs_eq.
    rewrite <- Forall_Mem in Hf_l2. specializes Hf_l2 Hm.
    rewrite wfp_gfresh_Abs in Hf_l2. intuition.
    lets Ht : TrIn a0 X0 p0. apply wfp_prod_in with (l := get_ins dp2) in Ht; auto.
    destruct Ht as (fl & Ht). apply act2_in with (p1 := (wfp_prod (get_ins dp1))) in Ht.
    eapply IObis_in_full in Ht. Focus 2. symmetry. eassumption.
    destruct Ht as (fq & Ht & _). apply wfp_trans_in_chan_eq in Ht; auto.

  clear dependent dp1; clear dependent dp2.

  destruct l1; destruct l2; solve_wfp_sizeP.

  inverts Hspec_l1. destruct H1 as (p1 & Heq). subst. rename H2 into Hspec_l1.
  inverts Hspec_l2. destruct H1 as (p2 & Heq). subst. rename H2 into Hspec_l2.

Lemma IO_pointwise_IObis : ∀ lp1 lp2, IO_pointwise lp1 lp2 →
  ∀ p, Mem p lp1 → ∃ q, Mem q lp2 ∧ p ≈ q.
Proof.
  inductions lp1; introv Hio Hm. inverts Hm.

  destruct lp2. apply IO_pw_len in Hio. rew_length in *; nat_math.
  inverts Hm. simpls. ∃ w; splits×. constructor.
  simpls. inverts Hio. specializes IHlp1 H1 H0.
  destruct IHlp1 as (q & Hmq & Hio).
  ∃ q; splits×. repeat constructor¬.
Qed.

  assert (Hio_p1p2 : p1 ≈ p2).
  {
    assert (Hio_rev_1 : wfp_Abs a X p ≈ wfp_Par (wfp_Abs a X p1) (wfp_Par (wfp_Abs a X p2) (wfp_prod (l1 ++ l2)))).
    {
      etransitivity. eassumption. etransitivity.
      apply IObis_congr_par; symmetry; applys¬ wfp_prod_cons_inv.
      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      etransitivity. apply IObis_congr_par_com.
      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      etransitivity. apply IObis_congr_par_com. symmetry; apply wfp_prod_IO_app.
    } clear Hio.

    remember (wfp_prod (l1 ++ l2)) as q; clear Heqq.

    lets Ht1 : TrIn a X p1. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p2) q) in Ht1.
    symmetry in Hio_rev_1. lets Htr : IObis_in_full Hio_rev_1 Ht1. destruct Htr as (fq & Htr1 & Hinst_p1). simpls wfp_inst_Abs.

    assert (Hio_rev_2 : wfp_Par (wfp_Abs a X p2) (wfp_Par (wfp_Abs a X p1) q) ≈ wfp_Abs a X p).
    {
      etransitivity. Focus 2. eassumption.
      etransitivity. apply IObis_par_assoc_l.
      etransitivity. Focus 2. apply IObis_par_assoc_r.
      applys¬ IObis_congr_par. apply IObis_congr_par_com.
    }

    lets Ht2 : TrIn a X p2. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p1) q) in Ht2.
    lets Htr : IObis_in_full Hio_rev_2 Ht2. destruct Htr as (fr & Htr2 & Hinst_p2). simpls wfp_inst_Abs.

    specializes Hinst_p1 X; specializes Hinst_p2 X; rewrite wfp_subst_gvar_idem in ×.

    assert (Hinst_eq : wfp_inst_Abs fq (wfp_Gvar X) = wfp_inst_Abs fr (wfp_Gvar X)).
    {
      apply wfp_trans_in_abs_eq in Htr1; apply wfp_trans_in_abs_eq in Htr2.
      inverts Htr1; inverts¬ Htr2; simpls wfp_inst_Abs.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqq & Hfy & Heq); subst.
        destruct H0 as (Z & Hneqr & Hfz & Heq); subst. simpls wfp_inst_Abs.
        do 2 rewrite¬ <- wfp_subst_decomposition_g.
    }

    rewrite Hinst_eq in ×.

    assert (Hio : wfp_Par (wfp_Par p1 (wfp_Abs a X p2)) q ≈ wfp_Par (wfp_Par p2 (wfp_Abs a X p1)) q).
    {
      etransitivity. apply IObis_par_assoc_r. etransitivity. eassumption.
      etransitivity. symmetry. eassumption. apply IObis_par_assoc_l.
    }

    apply IObis_cancellation in Hio. symmetry in Hio.
    clear dependent fq. clear dependent fr. clear Hio_rev_1 Hio_rev_2 Ht1 Ht2.
    apply IObis_abs_inv_body with (a := a) (X := X).

    lets (lp1 & Hio_lp1 & Hpr_lp1) : prime_decomposition_exists p1.
    lets (lp2 & Hio_lp2 & Hpr_lp2) : prime_decomposition_exists p2.

    assert (Hpd_1 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p1 :: lp2)).
    {
      splits. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. inverts¬ Hp_l1.
    }

    assert (Hpd_2 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p2 :: lp1)).
    {
      splits. etransitivity. eassumption. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. inverts¬ Hp_l2.
    }

    assert (Hs_lp1 : Forall (fun p ⇒ wfp_sizeP p ≤ wfp_sizeP p1) lp1).
    {
      gen Hio_lp1. clear; intros. gen p1. inductions lp1; intros. constructor.
      constructor. assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
      specializes IHlp1 (wfp_prod lp1). rewrite <- Forall_Mem in ×. introv Hm.
      transitivity (wfp_sizeP (wfp_prod lp1)). applys¬ IHlp1.
      assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
    }

    assert (Hnio_lp1 : Forall (fun p ⇒ ¬ p ≈ wfp_Abs a X p1) lp1).
    {
      rewrite <- Forall_Mem. introv Hm Hio_x.
      apply IObis_sizeP_eq in Hio_x. rewrite <- Forall_Mem in Hs_lp1.
      specializes Hs_lp1 Hm. simpl_sizes; nat_math.
    }

    lets (lp1´ & lp2´ & Hp1 & Hp2 & Hio_pw) : prime_decomposition_unique Hpd_1 Hpd_2.

    assert (Hm : Mem (wfp_Abs a X p1) lp1´).
    eapply permut_mem. eassumption. constructor.

    lets Hpw : IO_pointwise_IObis Hio_pw Hm.
    destruct Hpw as (r & Hmr & Hio_r).
    eapply permut_mem in Hmr. Focus 2. apply permut_sym. eassumption.
    inverts Hmr as Hmr; auto.
    rewrite <- Forall_Mem in Hnio_lp1. specializes Hnio_lp1 Hmr.
    false×.
  }

  assert (Hio_l1 : Forall (fun p ⇒ wfp_Abs a X p1 ≈ p) l1).
  {
    clear Hio_p1p2. rename p2 into r. rewrite <- Forall_Mem. introv Hm.
    lets Hx : Hspec_l1. rewrite <- Forall_Mem in Hx; specializes Hx Hm.
    destruct Hx as (p2 & Heq); subst. apply IObis_congr_abs.

    rename l1 into l1´. apply permut_mem_exists in Hm. destruct Hm as (l1 & Hper).

    assert (Hio_rev_1 : wfp_Abs a X p ≈ wfp_Par (wfp_Abs a X p1) (wfp_Par (wfp_Abs a X p2) (wfp_prod (wfp_Abs a X r :: l1 ++ l2)))).
    {
      etransitivity. eassumption. etransitivity.
      apply IObis_congr_par; symmetry; applys¬ wfp_prod_cons_inv.
      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      etransitivity. apply IObis_congr_par_com.
      etransitivity. apply IObis_par_assoc_r.
      etransitivity. Focus 2. apply IObis_congr_par.
      reflexivity. apply wfp_prod_cons_inv.
      etransitivity. Focus 2. apply IObis_congr_par_com.
      etransitivity. Focus 2. apply IObis_par_assoc_l. applys¬ IObis_congr_par.
      etransitivity. Focus 2. apply IObis_congr_par. symmetry. apply wfp_prod_IO_app. reflexivity.
      etransitivity. Focus 2. apply IObis_congr_par. apply IObis_congr_par_com. reflexivity.
      etransitivity. Focus 2. apply IObis_par_assoc_l. applys¬ IObis_congr_par.
      apply wfp_prod_IO_permut in Hper. etransitivity. symmetry; eassumption.
      etransitivity. Focus 2. apply IObis_congr_par_com. symmetry. apply wfp_prod_cons_inv.
    } clear Hio.

    remember (wfp_prod (wfp_Abs a X r :: l1 ++ l2)) as q; clear Heqq.
    clear dependent r.

    lets Ht1 : TrIn a X p1. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p2) q) in Ht1.
    symmetry in Hio_rev_1. lets Htr : IObis_in_full Hio_rev_1 Ht1. destruct Htr as (fq & Htr1 & Hinst_p1). simpls wfp_inst_Abs.

    assert (Hio_rev_2 : wfp_Par (wfp_Abs a X p2) (wfp_Par (wfp_Abs a X p1) q) ≈ wfp_Abs a X p).
    {
      etransitivity. Focus 2. eassumption.
      etransitivity. apply IObis_par_assoc_l.
      etransitivity. Focus 2. apply IObis_par_assoc_r.
      applys¬ IObis_congr_par. apply IObis_congr_par_com.
    }

    lets Ht2 : TrIn a X p2. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p1) q) in Ht2.
    lets Htr : IObis_in_full Hio_rev_2 Ht2. destruct Htr as (fr & Htr2 & Hinst_p2). simpls wfp_inst_Abs.

    specializes Hinst_p1 X; specializes Hinst_p2 X; rewrite wfp_subst_gvar_idem in ×.

    assert (Hinst_eq : wfp_inst_Abs fq (wfp_Gvar X) = wfp_inst_Abs fr (wfp_Gvar X)).
    {
      apply wfp_trans_in_abs_eq in Htr1; apply wfp_trans_in_abs_eq in Htr2.
      inverts Htr1; inverts¬ Htr2; simpls wfp_inst_Abs.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqq & Hfy & Heq); subst.
        destruct H0 as (Z & Hneqr & Hfz & Heq); subst. simpls wfp_inst_Abs.
        do 2 rewrite¬ <- wfp_subst_decomposition_g.
    }

    rewrite Hinst_eq in ×.

    assert (Hio : wfp_Par (wfp_Par p1 (wfp_Abs a X p2)) q ≈ wfp_Par (wfp_Par p2 (wfp_Abs a X p1)) q).
    {
      etransitivity. apply IObis_par_assoc_r. etransitivity. eassumption.
      etransitivity. symmetry. eassumption. apply IObis_par_assoc_l.
    }

    apply IObis_cancellation in Hio. symmetry in Hio.
    clear dependent fq. clear dependent fr. clear Hio_rev_1 Hio_rev_2 Ht1 Ht2.
    apply IObis_abs_inv_body with (a := a) (X := X).

    lets (lp1 & Hio_lp1 & Hpr_lp1) : prime_decomposition_exists p1.
    lets (lp2 & Hio_lp2 & Hpr_lp2) : prime_decomposition_exists p2.

    assert (Hpd_1 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p1 :: lp2)).
    {
      splits. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. inverts¬ Hp_l1.
    }

    assert (Hpd_2 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p2 :: lp1)).
    {
      splits. etransitivity. eassumption. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. inverts Hp_l1. eapply Forall_permut in H2; try eassumption. inverts¬ H2.
    }

    assert (Hs_lp1 : Forall (fun p ⇒ wfp_sizeP p ≤ wfp_sizeP p1) lp1).
    {
      gen Hio_lp1. clear; intros. gen p1. inductions lp1; intros. constructor.
      constructor. assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
      specializes IHlp1 (wfp_prod lp1). rewrite <- Forall_Mem in ×. introv Hm.
      transitivity (wfp_sizeP (wfp_prod lp1)). applys¬ IHlp1.
      assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
    }

    assert (Hnio_lp1 : Forall (fun p ⇒ ¬ p ≈ wfp_Abs a X p1) lp1).
    {
      rewrite <- Forall_Mem. introv Hm Hio_x.
      apply IObis_sizeP_eq in Hio_x. rewrite <- Forall_Mem in Hs_lp1.
      specializes Hs_lp1 Hm. simpl_sizes; nat_math.
    }

    lets (lp1´ & lp2´ & Hp1 & Hp2 & Hio_pw) : prime_decomposition_unique Hpd_1 Hpd_2.

    assert (Hm : Mem (wfp_Abs a X p1) lp1´).
    eapply permut_mem. eassumption. constructor.

    lets Hpw : IO_pointwise_IObis Hio_pw Hm.
    destruct Hpw as (r & Hmr & Hio_r).
    eapply permut_mem in Hmr. Focus 2. apply permut_sym. eassumption.
    inverts Hmr as Hmr; auto.
    rewrite <- Forall_Mem in Hnio_lp1. specializes Hnio_lp1 Hmr.
    false×.
  }

  assert (Hio_l2 : Forall (fun p ⇒ wfp_Abs a X p1 ≈ p) l2).
  {
    clear Hio_p1p2. rename p2 into r. rewrite <- Forall_Mem. introv Hm.
    lets Hx : Hspec_l2. rewrite <- Forall_Mem in Hx; specializes Hx Hm.
    destruct Hx as (p2 & Heq); subst. apply IObis_congr_abs.

    rename l2 into l2´. apply permut_mem_exists in Hm. destruct Hm as (l2 & Hper).

    assert (Hio_rev_1 : wfp_Abs a X p ≈ wfp_Par (wfp_Abs a X p1) (wfp_Par (wfp_Abs a X p2) (wfp_prod (wfp_Abs a X r :: l1 ++ l2)))).
    {
      etransitivity. eassumption. etransitivity.
      apply IObis_congr_par; symmetry; apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
      apply wfp_prod_IO_permut in Hper. symmetry; eassumption.
      etransitivity. apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
      symmetry. apply wfp_prod_cons_inv.
      etransitivity. Focus 2. apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
      apply wfp_prod_cons_inv.
      etransitivity. Focus 2. apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
      apply IObis_congr_par. reflexivity. symmetry; apply wfp_prod_IO_app.

      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      etransitivity. apply IObis_par_assoc_l. etransitivity. apply IObis_congr_par_com.
      etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
      etransitivity. apply IObis_par_assoc_l. etransitivity. apply IObis_congr_par_com.
      applys¬ IObis_congr_par. apply IObis_congr_par_com.
    } clear Hio.

    remember (wfp_prod (wfp_Abs a X r :: l1 ++ l2)) as q; clear Heqq.
    inverts Hp_l2. clear dependent r.

    lets Ht1 : TrIn a X p1. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p2) q) in Ht1.
    symmetry in Hio_rev_1. lets Htr : IObis_in_full Hio_rev_1 Ht1. destruct Htr as (fq & Htr1 & Hinst_p1). simpls wfp_inst_Abs.

    assert (Hio_rev_2 : wfp_Par (wfp_Abs a X p2) (wfp_Par (wfp_Abs a X p1) q) ≈ wfp_Abs a X p).
    {
      etransitivity. Focus 2. eassumption.
      etransitivity. apply IObis_par_assoc_l.
      etransitivity. Focus 2. apply IObis_par_assoc_r.
      applys¬ IObis_congr_par. apply IObis_congr_par_com.
    }

    lets Ht2 : TrIn a X p2. apply act1_in with (p2 := wfp_Par (wfp_Abs a X p1) q) in Ht2.
    lets Htr : IObis_in_full Hio_rev_2 Ht2. destruct Htr as (fr & Htr2 & Hinst_p2). simpls wfp_inst_Abs.

    specializes Hinst_p1 X; specializes Hinst_p2 X; rewrite wfp_subst_gvar_idem in ×.

    assert (Hinst_eq : wfp_inst_Abs fq (wfp_Gvar X) = wfp_inst_Abs fr (wfp_Gvar X)).
    {
      apply wfp_trans_in_abs_eq in Htr1; apply wfp_trans_in_abs_eq in Htr2.
      inverts Htr1; inverts¬ Htr2; simpls wfp_inst_Abs.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqr & Hfy & Heq); subst. simpls wfp_inst_Abs.
        rewrite¬ <- wfp_subst_decomposition_g.
      + destruct H as (Y & Hneqq & Hfy & Heq); subst.
        destruct H0 as (Z & Hneqr & Hfz & Heq); subst. simpls wfp_inst_Abs.
        do 2 rewrite¬ <- wfp_subst_decomposition_g.
    }

    rewrite Hinst_eq in ×.

    assert (Hio : wfp_Par (wfp_Par p1 (wfp_Abs a X p2)) q ≈ wfp_Par (wfp_Par p2 (wfp_Abs a X p1)) q).
    {
      etransitivity. apply IObis_par_assoc_r. etransitivity. eassumption.
      etransitivity. symmetry. eassumption. apply IObis_par_assoc_l.
    }

    apply IObis_cancellation in Hio. symmetry in Hio.
    clear dependent fq. clear dependent fr. clear Hio_rev_1 Hio_rev_2 Ht1 Ht2.
    apply IObis_abs_inv_body with (a := a) (X := X).

    lets (lp1 & Hio_lp1 & Hpr_lp1) : prime_decomposition_exists p1.
    lets (lp2 & Hio_lp2 & Hpr_lp2) : prime_decomposition_exists p2.

    assert (Hpd_1 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p1 :: lp2)).
    {
      splits. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. inverts¬ Hp_l1.
    }

    assert (Hpd_2 : prime_decomposition (wfp_Par p2 (wfp_Abs a X p1)) (wfp_Abs a X p2 :: lp1)).
    {
      splits. etransitivity. eassumption. etransitivity. Focus 2. apply wfp_prod_cons_inv.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      constructor¬. eapply Forall_permut in H2; try eassumption. inverts¬ H2.
    }

    assert (Hs_lp1 : Forall (fun p ⇒ wfp_sizeP p ≤ wfp_sizeP p1) lp1).
    {
      gen Hio_lp1. clear; intros. gen p1. inductions lp1; intros. constructor.
      constructor. assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
      specializes IHlp1 (wfp_prod lp1). rewrite <- Forall_Mem in ×. introv Hm.
      transitivity (wfp_sizeP (wfp_prod lp1)). applys¬ IHlp1.
      assert (Hio : p1 ≈ wfp_Par a (wfp_prod lp1)).
      etransitivity. eassumption. symmetry. apply wfp_prod_cons_inv.
      apply IObis_sizeP_eq in Hio; simpl_sizes. nat_math.
    }

    assert (Hnio_lp1 : Forall (fun p ⇒ ¬ p ≈ wfp_Abs a X p1) lp1).
    {
      rewrite <- Forall_Mem. introv Hm Hio_x.
      apply IObis_sizeP_eq in Hio_x. rewrite <- Forall_Mem in Hs_lp1.
      specializes Hs_lp1 Hm. simpl_sizes; nat_math.
    }

    lets (lp1´ & lp2´ & Hp1 & Hp2 & Hio_pw) : prime_decomposition_unique Hpd_1 Hpd_2.

    assert (Hm : Mem (wfp_Abs a X p1) lp1´).
    eapply permut_mem. eassumption. constructor.

    lets Hpw : IO_pointwise_IObis Hio_pw Hm.
    destruct Hpw as (r & Hmr & Hio_r).
    eapply permut_mem in Hmr. Focus 2. apply permut_sym. eassumption.
    inverts Hmr as Hmr; auto.
    rewrite <- Forall_Mem in Hnio_lp1. specializes Hnio_lp1 Hmr.
    false×.
  }

  ∃ (S (length l1) + S (length l2)) p1; splits; [nat_math | | inverts¬ Hn_l1].

  etransitivity. eassumption. gen Hio_l1 Hio_l2 Hio_p1p2 Hspec_l1 Hspec_l2. clear. inductions l1; intros.

  + clear Hio_l1. inductions l2.
    - simpls. applys¬ IObis_congr_par. applys¬ IObis_congr_abs.
    - inverts Hspec_l2. specializes¬ IHl2 H2. inverts¬ Hio_l2. eassumption.
      rewrite wfp_prod_cons. simpl (wfp_prod (wfp_Abs a X p1 :: nil)) in ×.
      replace (S (length nil) + S (length (a0 :: l2))) with (S (S (S (length l2)))); try (rew_length; nat_math).
      replace (S (length nil) + S (length l2)) with (S (S (length l2))) in IHl2; try (rew_length; nat_math).
      repeat rewrite wfp_prod_repeat_SS in ×. applys¬ IObis_congr_par.
      apply IObis_congr_par. applys¬ IObis_congr_abs.
      apply IObis_cancellation with (r := wfp_Abs a X p1).
      etransitivity. Focus 2. apply IObis_congr_par_com.
      etransitivity. Focus 2. eassumption.
      etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
      etransitivity. symmetry. apply wfp_prod_cons_inv.
      etransitivity. Focus 2. apply wfp_prod_cons_inv. applys¬ IObis_congr_par.
      destruct H1 as (p´ & Heq); subst. inverts¬ Hio_l2.

  + inverts Hio_l1. inverts Hspec_l1. specializes¬ IHl1 Hspec_l2.
    replace (S (length l1) + S (length l2)) with (S (S (length l1 + length l2))) in *; try (rew_length; nat_math).
    replace (S (length (a0 :: l1)) + S (length l2)) with (S (S (S (length l1 + length l2)))); try (rew_length; nat_math).
    repeat rewrite wfp_prod_repeat_SS in ×. rewrite wfp_prod_cons.
    etransitivity. apply IObis_par_assoc_r. applys¬ IObis_congr_par.
    etransitivity. Focus 2. eassumption. etransitivity.
    apply IObis_congr_par; symmetry; apply wfp_prod_cons_inv.
    etransitivity. Focus 2. apply IObis_congr_par; apply wfp_prod_cons_inv.
    repeat apply¬ IObis_congr_par. applys¬ IObis_congr_abs.
Qed.


Lemma completeness_lr : ∀ p q, normal_form p → normal_form q → p ≈ q → p ≡* q.
Proof with automate.

  cut (∀ p,
         ((∃ a X p´, p = wfp_Abs a X p´) → normal_form p → prime p) ∧
         (((∃ a X p´, p = wfp_Abs a X p´) → normal_form p → prime p) → normal_form p →
            ∀ q, ((∃ a X q´, q = wfp_Abs a X q´) → normal_form q → prime q) → normal_form q → p ≈ q → p ≡* q)).
  introv Hyp Hnfp Hnfq Hio. eapply Hyp; auto. eapply Hyp. eapply Hyp.

  induction p using (measure_induction wfp_sizeP);
  rename H into IH; splits.

  {
    introv (a & X & p´ & Heq) Hnfp. destruct_wf p; try solve [inverts¬ Hyp];
    try solve [inverts¬ H].

    clear Hyp a0 X0 p0. apply not_not_elim; introv Hnp.

    apply abs_not_prime in Hnp.
    destruct Hnp as (n & q & Hn & Hio & Hnq).
    assert (Ht : {{wfp_Abs a X p´ -- LabIn a ->> AA (AbsPure X p´)}}) by constructor.
    assert (Htq : {{wfp_Abs a X q -- LabIn a ->> AA (AbsPure X q )}}) by constructor.
    lets Hyp : IObis_in Ht. eassumption. simpls.
    destruct n. nat_math. destruct n. nat_math.
    simpl wfp_repeat in Hio. destruct Hyp as (fq & Htp & Hio´).

    assert (∀ Y, wfp_inst_Abs fq (wfp_Gvar Y) ≈
                        wfp_Par (wfp_subst (wfp_Gvar Y) X q) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q)))).
    {
      
      gen Htp. clear. intro Htp. inductions n.

      + simpls. inverts Htp...

        - destruct ap; inverts H3.
          simpls. introv. applys¬ IObis_congr_par.
          apply wfp_trans_in_abs_eq in H2; inverts H2 as H2.
          simpls¬. destruct H2 as (Z & Hneq & Hf & Heq). subst. simpls¬.
          rewrite <- wfp_subst_decomposition_g; auto.

        - destruct aq; inverts H3.
          simpls. introv. etransitivity. apply IObis_congr_par_com. applys¬ IObis_congr_par.
          apply wfp_trans_in_abs_eq in H2; inverts H2 as H2.
          simpls¬. destruct H2 as (Z & Hneq & Hf & Heq). subst. simpls¬.
          rewrite <- wfp_subst_decomposition_g; auto.

     + rewrite wfp_prod_repeat_SS in Htp. remember (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X q))) as r.
       inverts Htp... remember (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X q))) as r.

       - destruct ap; inverts H3.
         apply wfp_trans_in_abs_eq in H2; inverts H2 as H2; introv.
         simpls¬. destruct H2 as (Z & Hneq & Hf & Heq). subst a0. simpl.
         rewrite <- wfp_subst_decomposition_g; auto.

      - remember (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X q))) as r. destruct aq; inverts H3. simpl. introv; substs.
        specializes IHn H2. specializes IHn Y.
        apply IObis_congr_par with (p1 := (wfp_Abs a X q)) (p2 := (wfp_Abs a X q)) in IHn; auto.
        etransitivity. eassumption. simpl wfp_repeat.
        etransitivity. apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
        symmetry. apply wfp_prod_cons_inv.
        rewrite wfp_prod_cons. etransitivity. Focus 2.
        apply IObis_congr_par. reflexivity. apply IObis_congr_par. reflexivity.
        apply wfp_prod_cons_inv. etransitivity. apply IObis_par_assoc_l.
        etransitivity. Focus 2. apply IObis_par_assoc_r.
        applys¬ IObis_congr_par. applys IObis_congr_par_com.
    }

    
    lets (Z & Hfz) : find_fresh ((proc (wfp_Abs a X p´)) :: (proc (wfp_prod (wfp_repeat (S (S n)) (wfp_Abs a X q)))) :: nil).
    rewrite Forall_to_conj_2 in Hfz. destruct Hfz as (Hfz1 & Hfz2). specializes¬ Hio´ Hfz2. specializes H Z.
    assert (Hio_red : wfp_subst (wfp_Gvar Z) X p´ ≈
                        wfp_Par (wfp_subst (wfp_Gvar Z) X q) (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q)))) by
      (etransitivity; eassumption). clear Hio´ H.

    assert (Hio´ : p´ ≈ wfp_Par q (wfp_swap X Z (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q))))).
    {
      
      tests Heq : (Z = X).

      + do 2 rewrite wfp_subst_gvar_idem in Hio_red. rewrite wfp_swap_equal. auto.

      +
        assert (Hfz1_p : Z # p´) by (rewrite wfp_gfresh_Abs in Hfz1; inverts× Hfz1).
        assert (Hfz1_q : Z # q).
        {
          
          gen Hfz2 Heq; clear; intros Hfz2 Heq. inductions n.

          + assert (Hfz_abs : Z # wfp_Abs a X q) by (simpls; rewrite× gfresh_par_iff in Hfz2).
            rewrite wfp_gfresh_Abs in Hfz_abs; inverts× Hfz_abs.

          + applys¬ IHn. rewrite wfp_prod_repeat_SS in Hfz2.
            simpls; rewrite gfresh_par_iff in Hfz2; jauto.
        }

        do 2 (rewrite wfp_gfresh_subst_is_swap in Hio_red; auto).

        apply IObis_swap with (X := X) (Y := Z) in Hio_red...
        do 2 rewrite¬ wfp_swap_involutive in Hio_red.
    }
        
    clear Hio_red Hio.
    rewrite <- wfp_gfresh_subst_is_swap in Hio´; [ | simpls; rewrite gfresh_par_iff in Hfz2; jauto].
    rewrite wfp_prod_repeat_subst in Hio´...
    rewrite wfp_eq_subst_abs1 in Hio´.

    tests Hsq : (wfp_sizeP q > 0).

    assert (Hcgr : p´ ≡* wfp_Par q (wfp_prod (wfp_repeat (S n) (wfp_Abs a X q)))).
    {
      apply IH... apply IH...
      apply nf_abs_eq in Hnfp; jauto.
      apply IH... apply IObis_sizeP_eq in Hio´. rewrite <- Hio´...
      constructor×. clear.

      inductions n.
        simpls... rewrite wfp_prod_repeat_SS. simpl_sizes...

      apply nf_abs_eq in Hnq; jauto.

      gen Hnq. remember (wfp_Abs a X q) as r.
      assert (Hsr : wfp_sizeP r > 0) by (subst r; automate).
      gen Hsr; clear; intros Hsr Hnr.
      inductions n. simpls¬. simpls wfp_repeat. rewrite wfp_prod_cons. constructor×.
        destruct n; simpls¬. simpl_sizes. nat_math.
    }

    
    apply nf_abs_eq in Hnfp. inverts Hnfp. applys¬ (H0 (S n))...

    assert (Hcgrq : q ≡* wfp_Nil). apply wfp_sizeP_0_wfcgr_nil. nat_math. clear Hsq.

    assert (Hcgr : p´ ≡* (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))).
    {
      apply IH... apply IH...
      apply nf_abs_eq in Hnfp; jauto.

      apply IH...
      replace (wfp_sizeP (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil)))) with
                 (wfp_sizeP p´)...
        apply IObis_sizeP_eq in Hio´. rewrite Hio´.
        apply wfp_sizeP_0_wfcgr_nil in Hcgrq. simpl_sizes. rewrite Hcgrq.
        gen Hcgrq. clear. inductions n; intros.
          simpl. simpl_sizes. nat_math.
          repeat rewrite wfp_prod_repeat_SS. simpl_sizes. rewrite <- (IHn q); auto. nat_math.

      clear; inductions n.
        simpl. constructor×.
        introv Hn Hcgr. destruct n. nat_math. destruct n.
          simpls. apply wfcgr_sizeP in Hcgr. simpl_sizes. nat_math.
          rewrite wfp_prod_repeat_SS in Hcgr. apply wfcgr_sizeP in Hcgr.
          simpl_sizes. nat_math.
        rewrite wfp_prod_repeat_SS. constructor.
        simpl_sizes. nat_math. destruct n. simpl; simpl_sizes; nat_math.
        rewrite wfp_prod_repeat_SS; simpl_sizes. nat_math.
        constructor×. introv Hn Hcgr. destruct n0. nat_math. destruct n0.
          simpls. apply wfcgr_sizeP in Hcgr. simpl_sizes. nat_math.
          rewrite wfp_prod_repeat_SS in Hcgr. apply wfcgr_sizeP in Hcgr.
          simpl_sizes. nat_math. auto.

      etransitivity. eassumption. etransitivity.
      apply IObis_congr_par. apply congr_IObis. eassumption.
      instantiate (1 := wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))).
      gen Hcgrq. clear. introv Hcgrq. inductions n.
        simpls. apply IObis_congr_abs. applys¬ congr_IObis.
        repeat rewrite wfp_prod_repeat_SS. applys× IObis_congr_par.
        apply IObis_congr_abs. applys¬ congr_IObis.

      etransitivity. applys IObis_congr_par_com.
      applys IObis_congr_nil_r.
    }

    
    apply nf_abs_eq in Hnfp; jauto. inverts Hnfp.
    eapply (H0 (S n)). nat_math. instantiate (1 := wfp_Nil).
    etransitivity. eassumption. etransitivity.
    apply wfcgr_nil_l. apply wfcgr_par_com.
  }

  
  {
    
    cut (((∃ (a : chan) (X : var) (p´ : wfprocess), p = wfp_Abs a X p´) → normal_form p → prime p) →
         ∀ q : wfprocess, ((∃ (a : chan) (X : var) (q´ : wfprocess), q = wfp_Abs a X q´) → normal_form q → prime q) →
           normal_form p → normal_form q → (ordered p) ≈ (ordered q) → (ordered p) ≡* (ordered q)).

    introv Hyp HH Hn1 Hn2 Hio.
    transitivity (ordered p). apply ordered_wfcgr.
    transitivity (ordered q).
      applys¬ Hyp; try solve [applys× ordered_nf_invariant].
      transitivity p. symmetry.
        apply congr_IObis. apply ordered_wfcgr.
        transitivity q. auto. apply congr_IObis. apply ordered_wfcgr.
        symmetry; apply ordered_wfcgr.

    rewrite <- wfp_sizeP_ordered_eq in IH.

    introv Hyp_abs_p Hyp_abs_q Hyp_norm Hnfq Hio.
    unfolds ordered; unfolds get_components; remember (get_vars p) as lvp;
    remember (get_outs p) as lop; remember (get_ins p) as lip.

    assert (H_ordered : ordered p = wfp_prod (lvp ++ lop ++ lip)) by substs¬.

    destruct lvp. Focus 2.

      apply ordered_nf_invariant in Hyp_norm. unfold ordered in Hyp_norm.
      unfold get_components in Hyp_norm. rewrite <- Heqlvp in ×.
      rewrite <- Heqlop in ×. rewrite <- Heqlip in ×.
      apply ordered_nf_invariant in Hnfq. unfold ordered in Hnfq.
      unfold get_components in Hnfq.
      rewrite app_cons in ×. etransitivity. apply wfp_prod_wfcgr_cons.

      assert (Hw : Mem w (get_vars p)) by (rewrite <- Heqlvp; constructor).
      lets (X & Heqw & Hyp) : (get_vars_spec) Hw. subst w.

      assert (Hio_q : wfp_Par (wfp_Gvar X) (wfp_prod (lvp ++ lop ++ lip)) ≈ ordered q).
      {
        etransitivity. Focus 2. eassumption.
        destruct (lvp ++ lop ++ lip).
          simpls. apply IObis_congr_nil_r.
          rewrite¬ wfp_prod_cons.
      }
    
      
      assert (Ht : {{wfp_Gvar X -- LabRem X ->> AP wfp_Nil}}) by constructor.
      apply act1_rem with (p2 := (wfp_prod (lvp ++ lop ++ lip))) in Ht.
      lets (q´ & Htq & _) : IObis_var Hio_q Ht.
      apply trans_rem_wfcgr in Htq. destruct Htq as (q´´ & Hcgr & Hfpn).
      etransitivity. Focus 2. symmetry. eassumption. apply wfcgr_par. reflexivity.

      remember (lvp ++ lop ++ lip) as l. clear Heql.

      tests Hsq´´ : (wfp_sizeP q´´ > 0).

        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        destruct l. simpls×. rewrite wfp_prod_cons in Hyp_norm. inverts¬ Hyp_norm...
        apply IH... apply IObis_sizeP_eq in Hio_q. apply wfcgr_sizeP in Hcgr.
        rewrite Hcgr in Hio_q. rewrite wfp_prod_cons_wfp_sizeP in ×. simpl_sizes. nat_math.
        apply nf_congr_invariant in Hcgr; jauto. inverts¬ Hcgr...
        simpls; subst_wfp; rew_logic; splits*; introv Heq. inverts Heq.
        rewrite <- wfprocess_eq in Heq. subst. solve_wfp_sizeP.
        apply IObis_cancellation with (r := (wfp_Gvar X)).
        etransitivity. apply IObis_congr_par_com.
        etransitivity. Focus 2. apply IObis_congr_par_com.
        etransitivity. Focus 2. apply congr_IObis. apply Hcgr.
        etransitivity. eassumption. auto.

        assert (q´´ ≡* wfp_Nil). apply wfp_sizeP_0_wfcgr_nil. nat_math.
        etransitivity. Focus 2. symmetry. eassumption.
        apply wfp_sizeP_0_wfcgr_nil. apply IObis_sizeP_eq in Hio_q.
        apply wfcgr_sizeP in Hcgr. simpl_sizes. nat_math.


    lets Hnfp : Hyp_norm. apply ordered_nf_invariant in Hyp_norm. unfold ordered in Hyp_norm.
    unfold get_components in Hyp_norm. rewrite <- Heqlvp in ×.
    rewrite <- Heqlop in ×. rewrite <- Heqlip in ×.
    rewrite app_nil_l in ×. clear Heqlvp.

    destruct lop. Focus 2.

    apply ordered_nf_invariant in Hnfq. unfold ordered in Hnfq.
    unfold get_components in Hnfq.

    rewrite app_cons in ×. etransitivity. apply wfp_prod_wfcgr_cons.
    assert (Hw : Mem w (get_outs p)) by (rewrite <- Heqlop; constructor).
    lets (a & p´´ & Heqw & Hyp) : (get_outs_spec) Hw. subst w.

    assert (Hio_q : wfp_Par (wfp_Send a p´´) (wfp_prod (lop ++ lip)) ≈ ordered q).
    {
      etransitivity. Focus 2. eassumption.
      destruct (lop ++ lip). simpls¬. apply IObis_congr_nil_r.
      rewrite¬ wfp_prod_cons.
    } clear Hio.

    assert (Ht : {{wfp_Send a p´´ -- LabOut a p´´ ->> AP wfp_Nil}}) by constructor.
    apply act1_out with (p2 := (wfp_prod (lop ++ lip))) in Ht.
    lets (q´ & q´´´ & Htq & Hio) : IObis_out Hio_q Ht.
    apply trans_out_wfcgr in Htq. destruct Htq as (q´´ & Hcgr & Hfpn).
    destruct Hio as (_ & Hio).
    clear q´. remember (remove_par_nils q´´´) as q´.
    assert (¬ has_free_par_nil q´). subst. apply remove_nil_no_par_nil.
    assert (Hio´ : p´´ ≈ q´). etransitivity. eassumption. subst.
      apply congr_IObis. apply remove_par_nils_wfcgr.
    clear Hio. clear dependent q´´´.

    assert (wfp_Send a p´´ ≡* wfp_Send a q´).
    {
      
      tests Hsq´´ : (wfp_sizeP q´´ > 0).

        apply wfcgr_send. remember (lop ++ lip) as l. clear Heql.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        destruct l. simpls×. inverts Hyp_norm... rewrite wfp_prod_cons in Hyp_norm. inverts¬ Hyp_norm...
        assert (p0 = wfp_Send a p´´) by rewrite_wfp_equal. subst p0. inverts H4...
        apply IH... apply IObis_sizeP_eq in Hio_q. apply wfcgr_sizeP in Hcgr.
        rewrite Hcgr in Hio_q. rewrite wfp_prod_cons_wfp_sizeP in ×. simpl_sizes. nat_math.
        apply nf_congr_invariant in Hcgr; jauto. inverts¬ Hcgr...
        assert (p0 = wfp_Send a q´) by rewrite_wfp_equal. subst p0. inverts H4...
        simpls; subst_wfp; rew_logic; splits*; introv Heq. inverts Heq.
        rewrite <- wfprocess_eq in Heq. subst. solve_wfp_sizeP.

        assert (q´´ ≡* wfp_Nil). apply wfp_sizeP_0_wfcgr_nil. nat_math.
        remember (wfp_prod (lop ++ lip)) as r. assert (r ≡* wfp_Nil).
        apply wfp_sizeP_0_wfcgr_nil. apply IObis_sizeP_eq in Hio_q.
        apply IObis_sizeP_eq in Hio´. apply wfcgr_sizeP in Hcgr. simpl_sizes. nat_math.
        assert (Hio_q´ : wfp_Send a p´´ ≈ ordered q).
          etransitivity. apply IObis_congr_nil_l.
          etransitivity. Focus 2. eassumption.
          applys¬ IObis_congr_par. symmetry. applys¬ congr_IObis.
        clear Hio_q. assert (Hcgr´ : ordered q ≡* wfp_Send a q´).
          etransitivity. eassumption. etransitivity. apply wfcgr_par.
          reflexivity. eassumption. apply wfcgr_nil_r. clear Hcgr.
        assert (Hyp_norm´ : normal_form (wfp_Send a p´´)).
          destruct (lop ++ lip). simpls¬. rewrite wfp_prod_cons in ×.
          inverts Hyp_norm... assert (p0 = wfp_Send a p´´) by rewrite_wfp_equal.
          subst p0; auto. clear Hyp_norm.
        clear dependent r. clear dependent q´´.

        apply wfcgr_send.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        inverts Hyp_norm´...
        apply IH...

        replace (wfp_sizeP q´) with (wfp_sizeP p´´).
        rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
          apply IObis_sizeP_eq in Hio_q´.
          apply wfcgr_sizeP in Hcgr´. simpl_sizes. nat_math.

        apply nf_congr_invariant in Hcgr´; auto.
        inverts Hcgr´...
    }

    etransitivity. Focus 2. symmetry. eassumption. applys¬ wfcgr_par.

    remember (lop ++ lip) as l. clear Heql.

      tests Hsq´´ : (wfp_sizeP q´´ > 0).

        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        apply IH... rewrite wfp_prod_cons_wfp_sizeP; solve_wfp_sizeP.
        destruct l. simpls×. rewrite wfp_prod_cons in Hyp_norm. inverts¬ Hyp_norm...
        apply IH... apply IObis_sizeP_eq in Hio_q. apply wfcgr_sizeP in Hcgr.
        rewrite Hcgr in Hio_q. rewrite wfp_prod_cons_wfp_sizeP in ×. simpl_sizes. nat_math.
        apply nf_congr_invariant in Hcgr; jauto. inverts¬ Hcgr...
        simpls; subst_wfp; rew_logic; splits*; introv Heq. inverts Heq.
        rewrite <- wfprocess_eq in Heq. subst. solve_wfp_sizeP.
        apply IObis_cancellation_stronger with (r := wfp_Send a p´´) (s := wfp_Send a q´).
        etransitivity. apply IObis_congr_par_com.
        etransitivity. Focus 2. apply IObis_congr_par_com.
        etransitivity. Focus 2. apply congr_IObis. apply Hcgr.
        etransitivity. eassumption. auto.
        applys¬ congr_IObis.

        assert (q´´ ≡* wfp_Nil). apply wfp_sizeP_0_wfcgr_nil. nat_math.
        etransitivity. Focus 2. symmetry. eassumption.
        apply wfp_sizeP_0_wfcgr_nil. apply IObis_sizeP_eq in Hio_q.
        apply wfcgr_sizeP in Hcgr. apply IObis_sizeP_eq in Hio´. simpl_sizes. nat_math.


    destruct lip.
    intros. simpls. symmetry. applys¬ IObis_wfcgr_nil_iff.


    rewrite app_nil_l in ×. clear Heqlop.

    assert (Habs : Forall (fun q ⇒ ∃ a X p, q = wfp_Abs a X p) (w :: lip)).
    {
      gen Heqlip. clear; intro Heqlip. rewrite <- Forall_Mem. introv Hm.
      assert (Mem x (get_ins p)). rewrite¬ <- Heqlip.
      apply get_ins_spec in H. destruct H as (a & Y & p´ & Heq & _).
      ∃¬ a Y p´.
    } clear Heqlip.

    inverts Habs as Habsw. rename H3 into Habs.
    destruct Habsw as (a & X & p´ & Heq). subst w.

    assert (Hsize : Forall (fun q ⇒ wfp_sizeP q < wfp_sizeP (wfp_prod (wfp_Abs a X p´ :: lip))) lip).
    {
      clear. inductions lip; introv. constructor. rename a into w.
      replace (wfp_sizeP (wfp_prod (wfp_Abs a0 X p´ :: w :: lip))) with
              (wfp_sizeP (wfp_prod (w :: wfp_Abs a0 X p´ :: lip))).
      constructor. rewrite wfp_prod_cons in ×.
      lets Hyp : wfp_prod_cons_wfp_sizeP (wfp_Abs a0 X p´) lip. automate.
      Focus 2. repeat rewrite wfp_prod_cons_wfp_sizeP...
      specializes IHlip a0 X p´. rewrite <- Forall_Mem in *; introv Hm.
      specializes IHlip Hm. automate.
    }

    
    assert (Hnorm : Forall (fun q ⇒ normal_form q) lip).
    {
      gen Hyp_norm. clear. inductions lip; introv Hn. constructor.
      rename a into w. assert (normal_form (wfp_prod (w :: wfp_Abs a0 X p´ :: lip))).
        gen Hn. clear. gen w; destruct lip; introv Hn. simpls.
        constructor; inverts Hn...
        repeat rewrite wfp_prod_cons in ×. remember (wfp_prod (w :: lip)) as r.
        clear Heqr. inverts Hn... inverts H4...
        constructor×. simpl_sizes. nat_math.
      rewrite wfp_prod_cons in ×. constructor. inverts H...
      apply (IHlip a0 X p´). inverts H...
    }

    
    assert (Hprime : Forall (fun p ⇒ prime p) lip).
    {
      rewrite <- Forall_Mem in *; introv Hm; apply IH...
      applys¬ Habs.
    }

    
    assert (Hnorm´ : normal_form (wfp_Abs a X p´)).
      destruct lip; simpls~; inverts Hyp_norm...

    clear Hyp_norm. destruct lip.
    clear Hnorm Habs Hprime Hsize. simpls.


    assert (p = wfp_Abs a X p´).
    {
      rewrite <- H_ordered. apply num_of_pars_ordered.
      rewrite H_ordered. unfolds. simpls¬.
      introv Htnp. apply nf_no_par_nil in Hnfp. apply Hnfp.
      assert (wfp_sizeP p > 0). rewrite <- wfp_sizeP_ordered_eq.
      rewrite H_ordered. solve_wfp_sizeP.
      applys¬ has_top_has_free_nil. introv Heq. subst. solve_wfp_sizeP.
    }

    
    specializes Hyp_abs_p Hnfp. ∃¬ a X p´.
    substs. clear Hnfp H_ordered.

    apply ordered_nf_invariant in Hnfq. unfold ordered in Hnfq.
    unfold get_components in Hnfq.

    assert (get_vars q = nil).
    {
      lets Hspec : get_vars_spec q.
      destruct (get_vars q); auto.
      false. lets (Y & Heq & _) : Hspec w. constructor¬.
      subst. rewrite app_cons in ×. clear Hspec.
      remember (l ++ get_outs q ++ get_ins q) as l´. clear Heql´.
      lets Hyp : wfp_prod_cons_inv (wfp_Gvar Y) l´.
      lets Htr : TrRem Y. apply act1_rem with (p2 := wfp_prod l´) in Htr.
      lets Hio´ : IObis_var Htr. etransitivity. eassumption.
      symmetry. apply Hio. destruct Hio´ as (q´ & Htr´ & _). inverts× Htr´.
    } rewrite H in *; rewrite app_nil_l in *; clear H.

    assert (get_outs q = nil).
    {
      lets Hspec : get_outs_spec q.
      destruct (get_outs q); auto.
      false. lets (b & p´´ & Heq & _) : Hspec w. constructor¬.
      subst. rewrite app_cons in ×. clear Hspec.
      remember (l ++ get_ins q) as l´. clear Heql´.
      lets Hyp : wfp_prod_cons_inv (wfp_Send b p´´) l´.
      lets Htr : TrOut b p´´. apply act1_out with (p2 := wfp_prod l´) in Htr.
      lets Hio´ : IObis_out Htr. etransitivity. eassumption.
      symmetry. apply Hio. destruct Hio´ as (q´ & q´´ & Htr´ & _). inverts× Htr´.
    } rewrite H in *; rewrite app_nil_l in *; clear H.

    lets Hspec : get_ins_spec q.
    destruct (get_ins q).
      simpls. false. apply IObis_sizeP_eq in Hio. solve_wfp_sizeP.

     destruct l. Focus 2.
      false. rewrite wfp_prod_cons in ×.
      destruct Hyp_abs_p as (_ & Hyp_abs).
      specializes Hyp_abs Hio. inverts Hyp_abs.
      lets (b & Y & q´ & Heq & _) : Hspec w. constructor×.
      subst. apply IObis_sizeP_eq in H. solve_wfp_sizeP.
      lets (b & Y & q´ & Heq & _) : Hspec w0. do 2 constructor×.
      subst. destruct l; apply IObis_sizeP_eq in H. simpls. solve_wfp_sizeP.
      rewrite wfp_prod_cons in ×. simpl_sizes. nat_math.

    lets (b & Y & q´ & Heq & _) : Hspec w. constructor×.
    subst. simpls. clear Hspec.

    assert (b = a).
    {
      lets Htr : TrIn a X p´.
      lets Htr´ : IObis_in Hio Htr.
      destruct Htr´ as (fq & Htr´ & Hio´).
      lets¬ Heq : wfp_trans_in_chan_eq Htr´.
    } subst b.

    tests Heq_XY : (Y = X).

      apply wfcgr_abs. apply IH... apply IH...
      apply nf_abs_eq in Hnorm´; jauto.
      apply IH... apply IObis_sizeP_eq in Hio. simpl_sizes. nat_math.
      apply nf_abs_eq in Hnfq; jauto.

      lets Htr : TrIn a X p´.
      lets Htr´ : IObis_in_full Hio Htr.
      destruct Htr´ as (fq & Htr´ & Hio´).
      lets Heq : wfp_trans_in_abs_eq Htr´. inverts Heq as Heq.
      specializes Hio´ X. simpls. do 2 rewrite wfp_subst_gvar_idem in Hio´; auto.
      destruct Heq as (Y & Hneq & Hfy & Heq). subst.
      specializes Hio´ X. simpls. rewrite wfp_subst_gvar_idem in Hio´.
      rewrite <- wfp_subst_decomposition_g in Hio´; auto.
      rewrite wfp_subst_gvar_idem in Hio´; auto.

      assert (X # q´).
      {
        lets Hyp : gfresh_IObis X Hio.
        do 2 rewrite wfp_gfresh_Abs in ×. intuition.
      }
      lets Heq : wfp_Abs_eq a Y H. rewrite Heq in ×.
      remember (wfp_subst (wfp_Gvar X) Y q´) as r. clear Heqr H Heq q´.
      clear dependent Y. rename r into q´.

      apply wfcgr_abs. apply IH... apply IH...
      apply nf_abs_eq in Hnorm´; jauto.
      apply IH... apply IObis_sizeP_eq in Hio. simpl_sizes. nat_math.
      apply nf_abs_eq in Hnfq; jauto.

      lets Htr : TrIn a X p´.
      lets Htr´ : IObis_in_full Hio Htr.
      destruct Htr´ as (fq & Htr´ & Hio´).
      lets Heq : wfp_trans_in_abs_eq Htr´. inverts Heq as Heq.
      specializes Hio´ X. simpls. do 2 rewrite wfp_subst_gvar_idem in Hio´; auto.
      destruct Heq as (Y & Hneq & Hfy & Heq). subst.
      specializes Hio´ X. simpls. rewrite wfp_subst_gvar_idem in Hio´.
      rewrite <- wfp_subst_decomposition_g in Hio´; auto.
      rewrite wfp_subst_gvar_idem in Hio´; auto.


    assert (Hpd_v1 : prime_decomposition q (wfp_Abs a X p´ :: w :: lip)).
    {
      splits×. etransitivity. Focus 2. symmetry. eassumption.
      transitivity (ordered q); jauto. apply congr_IObis. apply ordered_wfcgr.
      constructor×. apply IH...
      inverts Habs. destruct H1 as (a´ & X´ & q´ & Heq). subst w.
      destruct lip. simpls; simpl_sizes. nat_math.
      repeat rewrite wfp_prod_cons; simpl_sizes; nat_math.
    }

    
    assert (Hno_var : ∀ Z q, ¬ {{wfp_prod (wfp_Abs a X p´ :: w :: lip) -- LabRem Z ->> q}}).
    {
      gen Habs. clear. introv Habs. introv; rewrite wfp_prod_cons; introv Ht.
      inverts Ht... destruct ap; inverts H3.
      gen w. clear a X p´.
      inductions lip; intros. inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H3.
      destruct aq; inverts H3...
      inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H2.
      destruct aq; inverts H4. specializes IHlip H2. inverts¬ Habs. auto.
      destruct ap; inverts H4. inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H2. destruct aq; inverts H4.
      specializes IHlip H2. inverts¬ Habs. auto.
    }

    
    assert (Hno_out : ∀ c p´ p´´ q, ¬ {{wfp_prod (wfp_Abs a X p´ :: w :: lip) -- LabOut c p´´ ->> q}}).
    {
      gen Habs. clear. introv Habs. introv; rewrite wfp_prod_cons; introv Ht.
      inverts Ht... destruct ap; inverts H3.
      gen w. clear a X p´.
      inductions lip; intros. inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H3.
      destruct aq; inverts H3...
      inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H2.
      destruct aq; inverts H4. specializes IHlip H2. inverts¬ Habs. auto.
      destruct ap; inverts H4. inverts Habs. destruct H1 as (b & Y & q & Heq).
      subst. inverts H2. destruct aq; inverts H4.
      specializes IHlip H2. inverts¬ Habs. auto.
    }

    
    lets Hnfq_orig : Hnfq. apply ordered_nf_invariant in Hnfq.
    unfold ordered in Hnfq. unfold get_components in Hnfq.
    assert (H_ord_q : ordered q = wfp_prod (get_vars q ++ get_outs q ++ get_ins q))
      by auto.

    assert (Hvq : get_vars q = nil).
    {
      lets Hspec : get_vars_spec q.
      destruct (get_vars q); auto.
      false. lets (Y & Heq & _) : Hspec w0. constructor¬.
      subst. rewrite app_cons in ×. clear Hspec.
      remember (l ++ get_outs q ++ get_ins q) as l´. clear Heql´.
      lets Hyp : wfp_prod_cons_inv (wfp_Gvar Y) l´.
      lets Htr : TrRem Y. apply act1_rem with (p2 := wfp_prod l´) in Htr.
      lets Hio´ : IObis_var Htr. etransitivity. eassumption.
      symmetry. apply Hio. destruct Hio´ as (q´ & Htr´ & _).
      eapply Hno_var. eassumption.
    } rewrite Hvq in *; rewrite app_nil_l in ×.

    assert (Hoq : get_outs q = nil).
    {
      lets Hspec : get_outs_spec q.
      destruct (get_outs q); auto.
      false. lets (b & p´´ & Heq & _) : Hspec w0. constructor¬.
      subst. rewrite app_cons in ×. clear Hspec.
      remember (l ++ get_ins q) as l´. clear Heql´.
      lets Hyp : wfp_prod_cons_inv (wfp_Send b p´´) l´.
      lets Htr : TrOut b p´´. apply act1_out with (p2 := wfp_prod l´) in Htr.
      lets Hio´ : IObis_out Htr. etransitivity. eassumption.
      symmetry. apply Hio. destruct Hio´ as (q´ & q´´ & Htr´ & _).
      eapply Hno_out. eassumption.
    } rewrite Hoq in *; rewrite app_nil_l in ×.

    clear Hno_var Hno_out.

    assert (Hpd_v2 : prime_decomposition q (get_ins q)).
    {
      splits×. transitivity (ordered q).
      apply congr_IObis. apply ordered_wfcgr.
      unfolds ordered. unfolds get_components.
      rewrite Hvq, Hoq. do 2 rewrite¬ app_nil_l.
      clear Hvq Hoq. lets Hspec : get_ins_spec q.
      destruct (get_ins q). constructor.

      destruct l. constructor; [ | constructor].
      lets (b & Y & q´ & Heq & _) : Hspec w0. constructor.
      subst. simpl (wfp_prod (wfp_Abs b Y q´ :: nil)) in ×. clear Hspec.

      assert (Hord : q = ordered q). apply num_of_pars_ordered.
      rewrite H_ord_q. unfolds. simpls¬.
      introv Htnp. apply nf_no_par_nil in Hnfq_orig. apply Hnfq_orig.
      assert (wfp_sizeP q > 0). rewrite <- wfp_sizeP_ordered_eq.
      rewrite H_ord_q. solve_wfp_sizeP.
      applys¬ has_top_has_free_nil. introv Heq. subst. solve_wfp_sizeP.

      rewrite <- H_ord_q. rewrite <- Hord. apply Hyp_abs_q.
      ∃¬ b Y q´. rewrite Hord; rewrite¬ H_ord_q. auto.

      assert (Forall (fun p ⇒ wfp_sizeP p < wfp_sizeP (wfp_prod (wfp_Abs a X p´ :: w :: lip))) (w0 :: w1 :: l)).
      {
        apply IObis_sizeP_eq in Hio. rewrite Hio.
        lets (a0 & X0 & p0 & Heq & _) : Hspec w0. constructor. subst.
        lets (a1 & X1 & p1 & Heq & _) : Hspec w1. constructor. constructor. subst. gen Hspec. clear. inductions l; intros.
        simpls. constructor... constructor... constructor.
        apply Forall_permut with (l1 := a :: wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: l).
        constructor. destruct l. simpl... repeat rewrite wfp_prod_cons...
        rewrite <- Forall_Mem in ×. introv Hm.

        cut (wfp_sizeP x < wfp_sizeP (wfp_prod (wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: l))).
          introv Hyp. destruct l. simpls. simpl_sizes. nat_math.
          repeat rewrite wfp_prod_cons in ×. simpl_sizes. nat_math.
          specialize (IHl a0 X0 p0 a1 X1 p1). rewrite <- Forall_Mem in IHl.
          applys¬ IHl. introv Hm´. inverts Hm´. apply Hspec. constructor.
          inverts H0. apply Hspec. constructor. constructor.
          apply Hspec. repeat constructor¬.

        replace (a :: wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: l) with
                  ((a :: nil) ++ (wfp_Abs a0 X0 p0 :: nil) ++ (wfp_Abs a1 X1 p1 :: nil) ++ l).
          Focus 2. repeat rewrite app_cons. repeat rewrite¬ app_nil_l.
          replace (wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: a :: l) with
          ((wfp_Abs a0 X0 p0 :: nil) ++ (wfp_Abs a1 X1 p1 :: nil) ++ (a :: nil) ++ l).
          Focus 2. repeat rewrite app_cons. repeat rewrite¬ app_nil_l.
          eapply permut_trans. apply permut_get_3. apply permut_refl.
      }

      
      rewrite <- Forall_Mem in ×. introv Hm; specializes H Hm.
      apply IH... specializes Hspec Hm.
        destruct Hspec as (a0 & X0 & p0 & Heq & _). ∃¬ a0 X0 p0.
        gen Hnfq Hm. clear. gen w0 w1. inductions l; intros.
          simpls. inverts Hnfq... inverts¬ Hm. inverts¬ H0. inverts H5.
          rewrite wfp_prod_cons in Hnfq. remember (wfp_prod (w1 :: a :: l)) as q.
          inverts Hnfq... inverts¬ Hm. eapply IHl; eassumption.
    }

    
    lets H_unique : prime_decomposition_unique Hpd_v1 Hpd_v2.
    destruct H_unique as (lp1 & lp2 & Hp1 & Hp2 & Hiol).
    assert (Hl : length lp1 = length lp2) by applys¬ IO_pw_len.

    rename a into a0, X into X0, p´ into p0.
    inverts Habs. destruct H1 as (a1 & X1 & p1 & Heq). subst.

    assert (wfp_sizeP (wfp_Abs a0 X0 p0) < wfp_sizeP (wfp_prod (wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: lip))).
    {
      destruct lip. simpl... repeat rewrite wfp_prod_cons...
    }

    
    assert (Hslp1 : Forall (fun p ⇒ wfp_sizeP p < wfp_sizeP (wfp_prod (wfp_Abs a0 X0 p0 :: wfp_Abs a1 X1 p1 :: lip))) lp1).
    {
      rewrite <- Forall_Mem. introv Hm. eapply permut_mem in Hm.
      Focus 2. apply permut_sym. eassumption. gen x. rewrite Forall_Mem.
      constructor×.
    }

    
    etransitivity. apply wfp_prod_wfcgr_permut. apply permut_sym. eassumption.
    etransitivity. Focus 2. apply wfp_prod_wfcgr_permut. eassumption.

    lets Hp1´ : Hp1. apply wfp_prod_IO_permut in Hp1.
    apply IObis_sizeP_eq in Hp1. rewrite <- Hp1 in ×.

    assert (Hslp1´ : Forall (fun p ⇒ wfp_sizeP p > 0) lp1).
    {
      eapply Forall_permut. Focus 2. eassumption.
      rewrite <- Forall_Mem in ×. introv Hm.
      inverts Hm... specializes Hprime H1. inverts Hprime.
      rewrite <- wfp_sizeP_0_IO_nil in H0. nat_math.
    }

    
    assert (Hslp2´ : Forall (fun p ⇒ wfp_sizeP p > 0) lp2).
    {
        eapply Forall_permut. Focus 2. eassumption.
        apply get_ins_sizeP.
    }

    
    assert (Hnflp1 : Forall (fun p ⇒ normal_form p) lp1).
    {
      eapply Forall_permut. Focus 2. eassumption. constructor×.
    }

    
    assert (Hnflp2 : Forall (fun p ⇒ normal_form p) lp2).
    {
      eapply Forall_permut. Focus 2. eassumption.
      gen Hnfq. clear. remember (get_ins q) as l. clear Heql.
      inductions l; intros. constructor.
      destruct l. simpls. constructor¬.
      rewrite wfp_prod_cons in ×. inverts Hnfq...
      apply IHl in H4. constructor×.
    }

    
    clear Hp1´ H Hp1 Hpd_v1 Hprime Hnorm Hsize H_ordered.

    destruct lp1; destruct lp2.
      + simpl. reflexivity.
      + rew_length in ×. nat_math.
      + rew_length in ×. nat_math.
      + simpl in Hiol.
        destruct lp1; destruct lp2.
        - false. inverts Hslp1. simpls. nat_math.
        - rew_length in *; nat_math.
        - rew_length in *; nat_math.
        - repeat rewrite wfp_prod_cons. apply wfcgr_par.
          × apply IH... inverts¬ Hslp1. apply IH... inverts¬ Hslp1. inverts¬ Hnflp1.
            apply IH... inverts Hiol. apply IObis_sizeP_eq in H. rewrite <- H.
            inverts¬ Hslp1. inverts¬ Hnflp2.
          × assert (wfp_prod (w1 :: lp1) ≈ (wfp_prod (w2 :: lp2))).
            apply IO_pw_wfp_prod. simpls×.
            apply IH... inverts Hslp1´.
            rewrite wfp_prod_cons... apply IH...
            inverts Hslp1´. rewrite wfp_prod_cons...

            inverts Hnflp1. inverts Hslp1´. gen H4 H6. clear.
            remember (w1 :: lp1) as l. clear.
            inductions l; intros. constructor.
              destruct l. simpls. inverts¬ H4.
              rewrite wfp_prod_cons in ×. inverts H4. inverts H6.
              specializes IHl H2. constructor...
              destruct l; inverts¬ H4. rewrite wfp_prod_cons...

            apply IH... apply IObis_sizeP_eq in H. rewrite <- H.
            inverts Hslp1´. rewrite wfp_prod_cons...

            inverts Hnflp2. inverts Hslp2´. gen H4 H6. clear.
            remember (w2 :: lp2) as l. clear.
            inductions l; intros. constructor.
              destruct l. simpls. inverts¬ H4.
              rewrite wfp_prod_cons in ×. inverts H4. inverts H6.
              specializes IHl H2. constructor...
              destruct l; inverts¬ H4. rewrite wfp_prod_cons...
  }
Qed.

Lemma normal_form_IObis_wfcgr_eq :
  ∀ p q, normal_form p → normal_form q →
    (p ≈ q ↔ p ≡* q).
Proof.
  introv Hnp Hnq. splits; introv Hyp.
    applys¬ completeness_lr.
    applys¬ congr_IObis.
Qed.


Inductive extended_congruence : wfprocess → wfprocess → Prop :=
 | ECore : ∀ a X p n, n > 0 →
             extended_congruence
               (wfp_Abs a X (wfp_Par p (wfp_prod (wfp_repeat n (wfp_Abs a X p)))))
               (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p)))
 | ESend : ∀ p q a,
             extended_congruence p q →
               extended_congruence (wfp_Send a p) (wfp_Send a q)
 | EReceive : ∀ p q a X,
                extended_congruence p q →
                  extended_congruence (wfp_Abs a X p) (wfp_Abs a X q)
 | EParLeft : ∀ p q r,
                extended_congruence p q →
                  extended_congruence (wfp_Par p r) (wfp_Par q r)
 | EParRight : ∀ p q r,
                 extended_congruence p q →
                   extended_congruence (wfp_Par r p) (wfp_Par r q)

 | ECngr : ∀ p q, p ≡* q → extended_congruence p q


 | ESym : ∀ p q, extended_congruence p q → extended_congruence q p
 | ETrans : ∀ p q r, extended_congruence p q → extended_congruence q r → extended_congruence p r.

Hint Resolve ECore ESend EReceive EParLeft EParRight ECngr ESym ETrans.

Infix "≡E" := extended_congruence (at level 60).

Instance ext_cgr_refl : Reflexive extended_congruence.
Proof.
  introv. apply ECngr. reflexivity.
Qed.

Instance ext_cgr_sym : Symmetric extended_congruence.
Proof.
  introv Hyp; jauto.
Qed.

Instance ext_cgr_trans : Transitive extended_congruence.
Proof.
  introv Ht1 Ht2; jauto.
Qed.

Hint Resolve ext_cgr_refl ext_cgr_sym ext_cgr_trans.

Lemma ext_cgr_red : ∀ p q, p -≡->* q → p ≡E q.
Proof.
  introv Hred. inductions Hred; jauto.
  inverts H. destruct H0 as (p´ & q´ & Hcgr1 & Hcgr2 & Hred).
  transitivity p´; jauto. transitivity q´; jauto.
  clear dependent x; clear dependent y.
  inductions Hred; jauto. inductions H; jauto.

  + transitivity (wfp_Abs a X (wfp_Par wfp_Nil (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil))))); jauto.
    apply ECngr. apply wfcgr_abs. etransitivity. apply wfcgr_nil_l. apply wfcgr_par_com.
Qed.

Theorem HOCore_Sound_Complete : ∀ p q, p ≡E q ↔ p ≈ q.
Proof.
  introv; splits; intro Hyp.

  {
    inductions Hyp; jauto.

    + applys io_extcgr_full. constructor.
      tests Hs : (wfp_sizeP p > 0).

      - constructor. eexists. eexists. splits; try reflexivity.
        repeat constructor×.

      - assert (p ≡* wfp_Nil). rewrite <- wfp_sizeP_0_wfcgr_nil. nat_math. clear Hs.
        constructor. ∃ (wfp_Abs a X (wfp_prod (wfp_repeat n (wfp_Abs a X wfp_Nil)))).
        ∃ (wfp_prod (wfp_repeat (S n) (wfp_Abs a X wfp_Nil))). splits.

        × apply wfcgr_abs. etransitivity. apply wfcgr_par_com.
          etransitivity. apply wfcgr_par. reflexivity. eassumption.
          etransitivity. apply wfcgr_nil_r. clear H. inductions n.
          simpls. reflexivity. destruct n. simpls. applys¬ wfcgr_abs.
          repeat rewrite wfp_prod_repeat_SS. applys× wfcgr_par. applys¬ wfcgr_abs.

        × clear H. inductions n. simpls. symmetry. applys¬ wfcgr_abs.
          repeat rewrite wfp_prod_repeat_SS. applys¬ wfcgr_par.
          symmetry; applys¬ wfcgr_abs.

        × repeat constructor×.

    + applys¬ IObis_congr_send.
    + applys¬ IObis_congr_abs.
    + applys¬ IObis_congr_par.
    + applys¬ IObis_congr_par.
    + applys¬ congr_IObis.
  }

  {
    lets Hnp : normalization_stops p.
    lets Hnq : normalization_stops q.

    inverts Hnp as Hnp; inverts Hnq as Hnq.

    + rewrite normal_form_IObis_wfcgr_eq in Hyp; auto.
    + inverts Hnq as Hnq.
      - etransitivity. Focus 2. apply ECngr. symmetry. apply remove_par_nils_wfcgr.
        assert (Hyp´ : p ≈ remove_par_nils q).
          etransitivity. eassumption. apply congr_IObis. apply remove_par_nils_wfcgr.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
      - destruct Hnq as (r & Hred & Hnr).
        etransitivity. Focus 2. symmetry. apply ext_cgr_red. eassumption.
        assert (Hyp´ : p ≈ r).
          etransitivity. eassumption. applys¬ io_extcgr_full.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
    + inverts Hnp as Hnp.
      - etransitivity. apply ECngr. apply remove_par_nils_wfcgr.
        assert (Hyp´ : remove_par_nils p ≈ q).
          etransitivity. Focus 2. eassumption. symmetry. apply congr_IObis. apply remove_par_nils_wfcgr.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
      - destruct Hnp as (r & Hred & Hnr).
        etransitivity. apply ext_cgr_red. eassumption.
        assert (Hyp´ : r ≈ q).
          etransitivity. Focus 2. eassumption. symmetry. applys¬ io_extcgr_full.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
    + inverts Hnp as Hnp; inverts Hnq as Hnq.
      - etransitivity. apply ECngr. apply remove_par_nils_wfcgr.
        etransitivity. Focus 2. apply ECngr. symmetry. apply remove_par_nils_wfcgr.
        assert (Hyp´ : remove_par_nils p ≈ remove_par_nils q).
          transitivity p. symmetry. apply congr_IObis. apply remove_par_nils_wfcgr.
          transitivity q. auto. apply congr_IObis. apply remove_par_nils_wfcgr.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
      - etransitivity. apply ECngr. apply remove_par_nils_wfcgr.
        destruct Hnq as (r & Hred & Hnr).
        etransitivity. Focus 2. symmetry. apply ext_cgr_red. eassumption.
        assert (Hyp´ : remove_par_nils p ≈ r).
          transitivity p. symmetry. apply congr_IObis. apply remove_par_nils_wfcgr.
          transitivity q. auto. applys¬ io_extcgr_full.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
      - destruct Hnp as (r & Hred & Hnr).
        etransitivity. apply ext_cgr_red. eassumption.
        etransitivity. Focus 2. apply ECngr. symmetry. apply remove_par_nils_wfcgr.
        assert (Hyp´ : r ≈ remove_par_nils q).
          transitivity q. Focus 2. apply congr_IObis. apply remove_par_nils_wfcgr.
          transitivity p. symmetry. applys¬ io_extcgr_full. auto.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
      - destruct Hnp as (r & Hredr & Hnr). destruct Hnq as (s & Hreds & Hns).
        etransitivity. apply ext_cgr_red. eassumption.
        etransitivity. Focus 2. symmetry. apply ext_cgr_red. eassumption.
        assert (Hyp´ : r ≈ s).
          transitivity p. symmetry. applys¬ io_extcgr_full.
          transitivity q. auto. applys¬ io_extcgr_full.
        rewrite normal_form_IObis_wfcgr_eq in Hyp´; auto.
  }
Qed.