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 : natType),
    ( n, ( m, m < nP m) → P n) →
    ( n, P n).
Proof.
  introv H. cuts× K: ( n m, m < nP 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 : Anat) (P : ASet),
    ( x, ( y, mu y < mu xP 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 : wfprocessSet),
  ( (a : chan) (p : wfprocess), P pP (wfp_Send a p)) →
  ( (a : chan) (X : var) (p : wfprocess), P pP (wfp_Abs a X p)) →
  ( X : var, P (wfp_Gvar X)) →
  ( p q : wfprocess, P pP qP (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 : wfprocesswfprocessProp :=
 | 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 --->* qwfp_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 --->* qwfp_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 --->* qwfp_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 --->* qwfp_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 ---> qwfp_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 --->* qwfp_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 ---> qwfp_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 --->* qwfp_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 ≡* qR_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 p´´, n > 0 → {{(wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) -- LabOut ->> 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 , n > 0 → {{(wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) -- LabRem Y ->> }}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´´ & Htq & Hrq´ & Hrq´´). 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 ( & Htq & Hrq´). ; splits×.
Qed.

Lemma io_norm_step : p q, p ---> qp 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 --->* qp q.
Proof.
  introv Ht; inductions Ht.
    applys¬ io_norm_step.
    etransitivity; eassumption.
Qed.

Lemma io_extcgr_step : p q, p -≡-> qp q.
Proof.
  introv Ht. inverts Ht...
  destruct H as ( & & 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 -≡->* qp 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 : wfprocessProp :=
 | 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 pnormal_form qnormal_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 ≡* qnormal_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 ).
      apply wfcgr_sizeP. constructor¬.
    assert (Hsq : wfp_sizeP q = wfp_sizeP ).
      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 ≡* qnormal_form p¬ has_free_par_nil qnormal_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 --->* qremove_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
  ( , Core p = Some (wfp_Send a ) →
      , Core q = Some (wfp_Send a ) --->* ).
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 ( & Hcq´ & Hcgrq´) : IHHred1 ...
    rewrite Hcq´ in ×. lets (q´´ & Hcq´´ & Hcgrq´´) : IHHred2 ...
     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 = NoneCore 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; symmetry in H; rewrite wfp_Abs_equal in ×.
    inverts H. clear H0. inverts . 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 ( & & 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 ( & & 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 ) as q.
    gen Ht Hnr H. clear. introv Ht. assert ( , wfp_Abs a X r ---> ).
      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 & & Heq). specializes Hcgr Hn; subst.
        apply (Hcgr ). reflexivity.
      × destruct Ht as ( & _ & Hr).
        apply (Hred ). constructor.
        eexists. eexists. splits×.
        reflexivity. reflexivity. constructor¬.

  + introv Ht. inverts Ht...
    destruct H0 as ( & & 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 ( & & Hc1 & Hc2 & Ht).

    assert (Hcp´ : Core = 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 ) 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 ( & & 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 pwfp_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 pnormal_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 ( & & H1 & H2 & H3).
    repeat constructor. (wfp_Send a ) (wfp_Send a ).
    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 ( & & H1 & H2 & H3).
    repeat constructor. (wfp_Par p2) (wfp_Par 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 ( & & H1 & H2 & H3).
    repeat constructor. (wfp_Par p1 ) (wfp_Par p1 ).
    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 ( & & H1 & H2 & H3).
    repeat constructor.
     (wfp_Abs a X ) (wfp_Abs a X ).
    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 premove_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 ( & & Hc1 & Hc2 & Hr).
  constructor. . ; splits*; etransitivity; try eassumption.
  symmetry. apply remove_par_nils_wfcgr. apply remove_par_nils_wfcgr.

  introv Hr. inverts Hr. destruct H as ( & & Hc1 & Hc2 & Hr).
  constructor. . ; 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 -≡->* qremove_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 ( & & Hc1 & Hc2 & Hr).
  constructor. . ; splits*; etransitivity; try eassumption.
  symmetry. apply remove_par_nils_wfcgr.

  introv Hr. inverts Hr. destruct H as ( & & Hc1 & Hc2 & Hr).
  constructor. . ; 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 .
    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 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 .

    lets Hwf : wf_cond (wfp_Abs a Y ). 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 ---> qlist_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 -≡-> qlist_sum (nested_abs n q) < list_sum (nested_abs n p).
Proof.
  introv Ht. inductions Ht.
  destruct H as ( & & 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 -≡->* qlist_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 ( & Htq´ & Hnfq´).
    eexists; splits. Focus 2. eassumption.
    etransitivity; eassumption.
Qed.


Lemma prime_characterization : p, prime p
  (( a , p wfp_Send a )
   ( X, p wfp_Gvar X)
   ( a X , p wfp_Abs a X ( n, n > 0 → q, ¬ ( ≡* (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 & & Hyp). a .
        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 & & Hyp1 & Hyp2). a X . 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 & & Hyp). a .
        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 & & Hyp1 & Hyp2). a X . 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 pnormal_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 ( & & 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 : wfprocessnormal_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 : wfprocessprime p) lp
  Forall (fun p : wfprocessnormal_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 lp, p wfp_Par (wfp_Send a ) (wfp_prod lp)
  normal_form
  Forall (fun p : wfprocessprime p) lp
  Forall (fun p : wfprocessnormal_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 ( & Hiop´ & Hnfp´).
         a (@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 & & lp1 & Hiop1 & Hnp1 & Hplp1 & Hnlp1).
      lets (lp2 & Hplp2 & Hnlp2 & Hiop2) : wfprocess_exists_list_prime_nf p2.
       a (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 & & lp2 & Hiop2 & Hnp2 & Hplp2 & Hnlp2).
      lets (lp1 & Hplp1 & Hnlp1 & Hiop1) : wfprocess_exists_list_prime_nf p1.
       a (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 ≡* wfp_Par (wfp_Gvar X) ).
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 ) 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 ) 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 , q = wfp_Send a p´´, p ≡* wfp_Par (wfp_Send a ) 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 & & (Heq_q & (p1´ & Heq_p1))).
     a . splits¬. (wfp_Par p1´ p2).
    etransitivity. apply wfcgr_par. eassumption. reflexivity.
    constructor. apply WfCgrPar_assoc2.
    destruct H as (a & & (Heq_q & (p2´ & Heq_p2))).
     a . 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 ) 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 ) 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 , q = wfp_Abs a X p´´, p ≡* wfp_Par (wfp_Abs a X ) 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 & & (Heq_q & (p1´ & Heq_p1))).
     a X . splits¬. (wfp_Par p1´ p2).
    etransitivity. apply wfcgr_par. eassumption. reflexivity.
    constructor. apply WfCgrPar_assoc2.
    destruct H as (a & X & & (Heq_q & (p2´ & Heq_p2))).
     a 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.

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

Lemma get_vars_sizeP : p, (Forall (fun pwfp_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 pwfp_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 pwfp_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 nill2 nilwfp_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 sr sp 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
     | nilhas_top_nil (wfp_prod l2)
     | _(has_top_nil (wfp_prod l1)) match l2 with
                                              | nilFalse
                                              | _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 pwfp_sizeP p > 0) l1) →
      l2, (Forall (fun pwfp_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 pdpd (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 pwfp_sizeP p > 0) l1) →
  (Forall (fun pwfp_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 pnormal_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 p2S (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 nill2 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 nill2 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 nill2 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