# Library PiCalc.bangpack

Require Export alglaws.

Section structural_congruence3.

Fixpoint cf_f_act (p q : proc) (n : nat) {struct n} : proc :=
match n with
| Opar q (bang p)
| S mpar p (cf_f_act p q m)
end.

Fixpoint cf_b_act (p : proc) (q : name proc) (n : nat) {struct n} :
name proc :=
match n with
| Ofun n : namepar (q n) (bang p)
| S mfun n : namepar p (cf_b_act p q m n)
end.

Fixpoint cf_tau1 (p q : proc) (r : name proc) (x : name)
(n m : nat) {struct m} : proc :=
match m with
| Opar (r x) (cf_f_act p q n)
| S m'par p (cf_tau1 p q r x n m')
end.

Fixpoint cf_tau2 (p q : proc) (r : name proc) (x : name)
(n m : nat) {struct m} : proc :=
match m with
| Opar q (cf_b_act p r n x)
| S m'par p (cf_tau2 p q r x n m')
end.

Fixpoint cf_tau3 (p : proc) (q r : name proc) (n m : nat) {struct m} :
proc :=
match m with
| Onu (fun n0 : namepar (q n0) (cf_b_act p r n n0))
| S m'par p (cf_tau3 p q r n m')
end.

Fixpoint frepl1 (p q : proc) (n : nat) {struct n} : proc :=
match n with
| Oq
| S mpar p (frepl1 p q m)
end.

Fixpoint frepl2 (p q : proc) (r : name proc) (x : name)
(n m : nat) {struct m} : proc :=
match m with
| Opar (r x) (frepl1 p q n)
| S m'par p (frepl2 p q r x n m')
end.

Fixpoint frepl3 (p q : proc) (r : name proc) (x : name)
(n m : nat) {struct m} : proc :=
match m with
| Opar q (frepl1 p (r x) n)
| S m'par p (frepl3 p q r x n m')
end.

Fixpoint frepl4 (p : proc) (q r : name proc) (n m : nat) {struct m} :
proc :=
match m with
| Onu (fun n0 : namepar (q n0) (frepl1 p (r n0) n))
| S m'par p (frepl4 p q r n m')
end.

Lemma BANG_OUT :
(p q : proc) (x y : name),
ftrans (bang p) (Out x y) q
r : proc,
( n : nat, q = cf_f_act p r n ftrans p (Out x y) r).

Proof.

simple induction q; intros; auto.

inversion_clear H; inversion_clear H0.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H1; inversion H2.
p0; 0; simpl in |- *; split; [ trivial | assumption ].
rewrite <- H6 in H5; rewrite <- H6; elim (H0 x y H5); intros.
inversion_clear H8.
inversion_clear H9.
x0; (S x1); split;
[ simpl in |- *; rewrite H8; trivial | assumption ].

inversion_clear H1; inversion_clear H2.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

Qed.

Lemma PRE_BANG_BTR :
(p q : proc) (r : name proc) (a : b_act) (x : name),
notin x (nu r)
notin x p
q = r x
btrans (bang p) a r
s : name proc,
( n : nat, r = cf_b_act p s n btrans p a s).

Proof.

simple induction q; intros; auto.

cut (r = (fun _ : namenil)); [ intro | apply proc_ext with x; auto ].
rewrite H3 in H2; inversion_clear H2.
inversion H4;
[ absurd (par (p0 x) (bang p) = nil);
[ discriminate
| change
((fun n : namepar (p0 n) (bang p)) x = (fun _ : namenil) x)
in |- *; rewrite H8; trivial ]
| absurd (par p (p0 x) = nil);
[ discriminate
| change ((fun n : namepar p (p0 n)) x = (fun _ : namenil) x)
in |- *; rewrite H8; trivial ] ].
apply notin_nu; intros; apply notin_nil.

elim (proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
cut (r = (fun n : namebang (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H4 in H3; inversion_clear H3.
inversion H7;
[ absurd (par (p3 x) (bang p) = bang (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namebang (x0 n)) x) in |- *;
rewrite H11; trivial ]
| absurd (par p (p3 x) = bang (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x = (fun n : namebang (x0 n)) x)
in |- *; rewrite H11; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_bang; auto.

elim (proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
cut (r = (fun n : nametau_pref (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H4 in H3; inversion_clear H3.
inversion H7;
[ absurd (par (p3 x) (bang p) = tau_pref (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : nametau_pref (x0 n)) x) in |- *;
rewrite H11; trivial ]
| absurd (par p (p3 x) = tau_pref (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : nametau_pref (x0 n)) x) in |- *;
rewrite H11; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_tau; auto.

inversion_clear H4.
inversion H5.
p4; 0; simpl in |- *; split; [ trivial | assumption ].
cut (p1 = p4 x); [ intro | rewrite <- H8 in H3; inversion_clear H3; trivial ].
cut (notin x (nu p4)); [ intro | rewrite <- H8 in H1; inversion_clear H1 ].
cut
( s : name proc,
( n : nat, p4 = cf_b_act p s n btrans p a s));
[ intro | apply H0 with x; auto ].
inversion_clear H12.
inversion_clear H13.
inversion_clear H12.
x0; (S x1); split;
[ simpl in |- *; rewrite <- H13; trivial | assumption ].
apply notin_nu; intros; cut (notin x (par p (p4 z))); [ intro | auto ].
inversion_clear H12; assumption.

elim (proc_exp p0 x); intros; elim (proc_exp p1 x); intros.
inversion_clear H5; inversion_clear H6.
rewrite H8 in H3; rewrite H9 in H3.
cut (r = (fun n : namesum (x0 n) (x1 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H6 in H4; inversion_clear H4.
inversion H10;
[ absurd (par (p4 x) (bang p) = sum (x0 x) (x1 x));
[ discriminate
| change
((fun n : namepar (p4 n) (bang p)) x =
(fun n : namesum (x0 n) (x1 n)) x) in |- *;
rewrite H14; trivial ]
| absurd (par p (p4 x) = sum (x0 x) (x1 x));
[ discriminate
| change
((fun n : namepar p (p4 n)) x =
(fun n : namesum (x0 n) (x1 n)) x) in |- *;
rewrite H14; trivial ] ].
apply notin_nu; intros; inversion_clear H7; inversion_clear H5;
apply notin_sum; auto.

elim (ho_proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
cut (r = (fun n : namenu (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H4 in H3; inversion_clear H3.
inversion H7;
[ absurd (par (p3 x) (bang p) = nu (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namenu (x0 n)) x) in |- *; rewrite H11;
trivial ]
| absurd (par p (p3 x) = nu (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x = (fun n : namenu (x0 n)) x)
in |- *; rewrite H11; trivial ] ].

elim (proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
elim (LEM_name n x); intros; elim (LEM_name n0 x); intros.
rewrite H4 in H2; rewrite H7 in H2.
cut (r = (fun n : namematch_ n n (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = match_ x x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namematch_ n n (x0 n)) x) in |- *;
rewrite H13; trivial ]
| absurd (par p (p3 x) = match_ x x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : namematch_ n n (x0 n)) x) in |- *;
rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_match; auto.

rewrite H4 in H2.
cut (r = (fun n : namematch_ n n0 (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = match_ x n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namematch_ n n0 (x0 n)) x) in |- *;
rewrite H13; trivial ]
| absurd (par p (p3 x) = match_ x n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : namematch_ n n0 (x0 n)) x) in |- *;
rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_match; auto.

rewrite H7 in H2.
cut (r = (fun n0 : namematch_ n n0 (x0 n0)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = match_ n x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n0 : namematch_ n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = match_ n x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n0 : namematch_ n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_match; auto.

cut (r = (fun n1 : namematch_ n n0 (x0 n1)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = match_ n n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n1 : namematch_ n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = match_ n n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n1 : namematch_ n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_match; auto.

elim (proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
elim (LEM_name n x); intros; elim (LEM_name n0 x); intros.
rewrite H4 in H2; rewrite H7 in H2.
cut (r = (fun n : namemismatch n n (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = mismatch x x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namemismatch n n (x0 n)) x) in |- *;
rewrite H13; trivial ]
| absurd (par p (p3 x) = mismatch x x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : namemismatch n n (x0 n)) x) in |- *;
rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_mismatch; auto.

rewrite H4 in H2.
cut (r = (fun n : namemismatch n n0 (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = mismatch x n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namemismatch n n0 (x0 n)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = mismatch x n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : namemismatch n n0 (x0 n)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_mismatch; auto.

rewrite H7 in H2.
cut (r = (fun n0 : namemismatch n n0 (x0 n0)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = mismatch n x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n0 : namemismatch n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = mismatch n x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n0 : namemismatch n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_mismatch; auto.

cut (r = (fun n1 : namemismatch n n0 (x0 n1)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = mismatch n n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n1 : namemismatch n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = mismatch n n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n1 : namemismatch n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_mismatch; auto.

elim (ho_proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
elim (LEM_name n x); intros.
rewrite H4 in H2.
cut (r = (fun n : namein_pref n (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H7 in H3; inversion_clear H3.
inversion H8;
[ absurd (par (p3 x) (bang p) = in_pref x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : namein_pref n (x0 n)) x) in |- *;
rewrite H12; trivial ]
| absurd (par p (p3 x) = in_pref x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : namein_pref n (x0 n)) x) in |- *;
rewrite H12; trivial ] ].
apply notin_nu; intros; inversion_clear H5.
cut (notin x (nu (x0 z))); [ intro | auto ].
inversion_clear H5; apply notin_in; intros; auto.

cut (r = (fun n0 : namein_pref n (x0 n0)));
[ intro | apply proc_ext with x; auto ].
rewrite H7 in H3; inversion_clear H3.
inversion H8;
[ absurd (par (p3 x) (bang p) = in_pref n (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n0 : namein_pref n (x0 n0)) x) in |- *;
rewrite H12; trivial ]
| absurd (par p (p3 x) = in_pref n (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n0 : namein_pref n (x0 n0)) x) in |- *;
rewrite H12; trivial ] ].
apply notin_nu; intros; inversion_clear H5.
cut (notin x (nu (x0 z))); [ intro | auto ].
inversion_clear H5; apply notin_in; intros; auto.

elim (proc_exp p0 x); intros.
inversion_clear H4.
rewrite H6 in H2.
elim (LEM_name n x); intros; elim (LEM_name n0 x); intros.
rewrite H4 in H2; rewrite H7 in H2.
cut (r = (fun n : nameout_pref n n (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = out_pref x x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : nameout_pref n n (x0 n)) x) in |- *;
rewrite H13; trivial ]
| absurd (par p (p3 x) = out_pref x x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : nameout_pref n n (x0 n)) x) in |- *;
rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_out; auto.

rewrite H4 in H2.
cut (r = (fun n : nameout_pref n n0 (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = out_pref x n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n : nameout_pref n n0 (x0 n)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = out_pref x n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n : nameout_pref n n0 (x0 n)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_out; auto.

rewrite H7 in H2.
cut (r = (fun n0 : nameout_pref n n0 (x0 n0)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = out_pref n x (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n0 : nameout_pref n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = out_pref n x (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n0 : nameout_pref n n0 (x0 n0)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_out; auto.

cut (r = (fun n1 : nameout_pref n n0 (x0 n1)));
[ intro | apply proc_ext with x; auto ].
rewrite H8 in H3; inversion_clear H3.
inversion H9;
[ absurd (par (p3 x) (bang p) = out_pref n n0 (x0 x));
[ discriminate
| change
((fun n : namepar (p3 n) (bang p)) x =
(fun n1 : nameout_pref n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ]
| absurd (par p (p3 x) = out_pref n n0 (x0 x));
[ discriminate
| change
((fun n : namepar p (p3 n)) x =
(fun n1 : nameout_pref n n0 (x0 n1)) x)
in |- *; rewrite H13; trivial ] ].
apply notin_nu; intros; inversion_clear H5; apply notin_out; auto.

Qed.

Lemma BANG_BTR :
(p : proc) (q : name proc) (a : b_act),
btrans (bang p) a q
r : name proc,
( n : nat, q = cf_b_act p r n btrans p a r).

Proof.

intros; elim (unsat (par p (nu q)) empty); intros; inversion_clear H0;
inversion_clear H1; clear H2; apply PRE_BANG_BTR with (q x) x;
auto.

Qed.

Lemma BANG_TAU :
p q : proc,
ftrans (bang p) tau q
( r : proc, ( n : nat, q = cf_f_act p r n ftrans p tau r))
( r : proc,
( s : name proc,
( x : name,
( y : name,
( n : nat,
( m : nat,
q = cf_tau1 p r s y n m
ftrans p (Out x y) r btrans p (In x) s))))))
( r : proc,
( s : name proc,
( x : name,
( y : name,
( n : nat,
( m : nat,
q = cf_tau2 p r s y n m
ftrans p (Out x y) r btrans p (In x) s))))))
( r : name proc,
( s : name proc,
( x : name,
( n : nat,
( m : nat,
q = cf_tau3 p r s n m
btrans p (In x) r btrans p (bOut x) s)))))
( r : name proc,
( s : name proc,
( x : name,
( n : nat,
( m : nat,
q = cf_tau3 p s r n m
btrans p (In x) r btrans p (bOut x) s))))).

Proof.

simple induction q; intros; auto.

inversion_clear H; inversion_clear H0.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H1; inversion H2.
left; p0; 0; split; [ simpl in |- *; trivial | assumption ].
rewrite <- H6 in H5; rewrite <- H6; elim (H0 H5); intros.
inversion_clear H8.
inversion_clear H9.
inversion_clear H8.
left; x; (S x0); split;
[ simpl in |- *; rewrite H9; trivial | assumption ].
elim H8; intros.
inversion_clear H9.
inversion_clear H10.
inversion_clear H9.
inversion_clear H10.
inversion_clear H9.
inversion_clear H10.
inversion_clear H9.
right; left; x; x0; x1; x2; x3;
(S x4); split; [ simpl in |- *; rewrite H10; trivial | assumption ].
elim H9; intros.
inversion_clear H10.
inversion_clear H11.
inversion_clear H10.
inversion_clear H11.
inversion_clear H10.
inversion_clear H11.
inversion_clear H10.
right; right; left; x; x0; x1; x2; x3;
(S x4); split; [ simpl in |- *; rewrite H11; trivial | assumption ].
elim H10; intros.
inversion_clear H11.
inversion_clear H12.
inversion_clear H11.
inversion_clear H12.
inversion_clear H11.
inversion_clear H12.
right; right; right; left; x; x0; x1; x2;
(S x3); split; [ simpl in |- *; rewrite H11; trivial | assumption ].
inversion_clear H11.
inversion_clear H12.
inversion_clear H11.
inversion_clear H12.
inversion_clear H11.
inversion_clear H12.
right; right; right; right; x; x0; x1; x2;
(S x3); split; [ simpl in |- *; rewrite H11; trivial | assumption ].

elim (BANG_OUT p p1 x y H7); intros.
inversion_clear H8.
inversion_clear H9.
right; left; x0; q1; x; y; x1; 0;
split; [ simpl in |- *; rewrite H8; trivial | split; assumption ].

elim (BANG_BTR p q2 (In x) H7); intros.
inversion_clear H8.
inversion_clear H9.
right; right; left; p0; x0; x; y; x1;
0; split; [ simpl in |- *; rewrite H8; trivial | split; assumption ].

inversion_clear H1; inversion_clear H2.

inversion_clear H0; inversion_clear H1.
elim (BANG_BTR p q2 (bOut x) H2); intros.
inversion_clear H1.
inversion_clear H3.
right; right; right; left; q1; x0; x; x1;
0; split; [ simpl in |- *; rewrite H1; trivial | split; assumption ].
elim (BANG_BTR p q2 (In x) H2); intros.
inversion_clear H1.
inversion_clear H3.
right; right; right; right; x0; q1; x; x1;
0; split; [ simpl in |- *; rewrite H1; trivial | split; assumption ].

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

inversion_clear H0; inversion_clear H1.

Qed.

Lemma SB_CF_F_ACT :
(p q : proc) (n : nat),
StBisim (cf_f_act p q n) (par (frepl1 p q n) (bang p)).

Proof.

simple induction n; intros.

simpl in |- *; apply REF.

simpl in |- *; apply TRANS with (par p (par (frepl1 p q n0) (bang p)));
[ apply PAR_S2; [ apply REF | assumption ] | apply SYM; apply ASS_PAR ].

Qed.

Lemma SB_CF_B_ACT :
(p : proc) (q : name proc) (n : nat) (x : name),
StBisim (cf_b_act p q n x) (par (frepl1 p (q x) n) (bang p)).

Proof.

simple induction n; intros.

simpl in |- *; apply REF.

simpl in |- *; apply TRANS with (par p (par (frepl1 p (q x) n0) (bang p)));
[ apply PAR_S2; [ apply REF | auto ] | apply SYM; apply ASS_PAR ].

Qed.

Lemma SB_CF_TAU1 :
(p q : proc) (r : name proc) (y : name) (n m : nat),
StBisim (cf_tau1 p q r y n m) (par (frepl2 p q r y n m) (bang p)).

Proof.

simple induction m; intros.

simpl in |- *; apply TRANS with (par (r y) (par (frepl1 p q n) (bang p)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT ]
| apply SYM; apply ASS_PAR ].

simpl in |- ×.

simpl in |- *; apply TRANS with (par p (par (frepl2 p q r y n n0) (bang p)));
[ apply PAR_S2; [ apply REF | assumption ] | apply SYM; apply ASS_PAR ].

Qed.

Lemma SB_CF_TAU2 :
(p q : proc) (r : name proc) (y : name) (n m : nat),
StBisim (cf_tau2 p q r y n m) (par (frepl3 p q r y n m) (bang p)).

Proof.

simple induction m; intros.

simpl in |- *; apply TRANS with (par q (par (frepl1 p (r y) n) (bang p)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT ]
| apply SYM; apply ASS_PAR ].

simpl in |- *; apply TRANS with (par p (par (frepl3 p q r y n n0) (bang p)));
[ apply PAR_S2; [ apply REF | assumption ] | apply SYM; apply ASS_PAR ].

Qed.

Lemma SB_CF_TAU3 :
(p : proc) (q r : name proc) (y : name) (n m : nat),
StBisim (cf_tau3 p q r n m) (par (frepl4 p q r n m) (bang p)).

Proof.

simple induction m; intros.

simpl in |- *;
apply
TRANS
with (nu (fun n0 : namepar (q n0) (par (frepl1 p (r n0) n) (bang p))));
[ apply NU_S; intros; apply PAR_S2; [ apply REF | apply SB_CF_B_ACT ]
| apply
TRANS
with
(nu (fun n0 : namepar (par (q n0) (frepl1 p (r n0) n)) (bang p)));
[ apply NU_S; intros; apply SYM; apply ASS_PAR
| change
(StBisim
(nu
(fun n0 : name
par ((fun u : namepar (q u) (frepl1 p (r u) n)) n0)
(bang p)))
(par (nu (fun n0 : namepar (q n0) (frepl1 p (r n0) n)))
(bang p))) in |- *; apply NU_EXTR ] ].

simpl in |- *; apply TRANS with (par p (par (frepl4 p q r n n0) (bang p)));
[ apply PAR_S2; [ apply REF | assumption ] | apply SYM; apply ASS_PAR ].

Qed.

Lemma F_REPL1 :
(p q r s : proc) (n : nat),
StBisim p q StBisim r s StBisim (frepl1 p r n) (frepl1 q s n).

Proof.

simple induction n; intros.
simpl in |- *; assumption.
simpl in |- *; apply PAR_S2; [ assumption | apply H; assumption ].

Qed.

Lemma F_REPL2 :
(p q r s : proc) (t u : name proc) (x : name) (n m : nat),
StBisim p q
StBisim r s
StBisim (t x) (u x) StBisim (frepl2 p r t x n m) (frepl2 q s u x n m).

Proof.

simple induction m; intros.

simpl in |- *; apply PAR_S2; [ assumption | apply F_REPL1; assumption ].

simpl in |- *; apply PAR_S2; auto.

Qed.

Lemma F_REPL3 :
(p q r s : proc) (t u : name proc) (x : name) (n m : nat),
StBisim p q
StBisim r s
StBisim (t x) (u x) StBisim (frepl3 p r t x n m) (frepl3 q s u x n m).

Proof.

simple induction m; intros.

simpl in |- *; apply PAR_S2; [ assumption | apply F_REPL1; assumption ].

simpl in |- *; apply PAR_S2; auto.

Qed.

Lemma FREPL1_NOTIN :
(p q : proc) (n : nat) (x : name),
notin x (frepl1 p q n) notin x q.

Proof.

simple induction n; intros.

simpl in H; assumption.

simpl in H0; inversion_clear H0; apply H; assumption.

Qed.

Lemma F_REPL4 :
(p q : proc) (r s t u : name proc) (n m : nat),
StBisim p q
( x : name, notin x (nu r) notin x (nu s) StBisim (r x) (s x))
( x : name, notin x (nu t) notin x (nu u) StBisim (t x) (u x))
StBisim (frepl4 p r t n m) (frepl4 q s u n m).

Proof.

simple induction m; intros.

simpl in |- *; apply NU_S; intros; apply PAR_S2.
apply H0; inversion_clear H2; apply notin_nu; intros.
cut (notin x (par (r z) (frepl1 p (t z) n))); [ intro | auto ].
inversion_clear H5; assumption.
inversion_clear H3; cut (notin x (par (s z) (frepl1 q (u z) n)));
[ intro | auto ].
inversion_clear H3; assumption.
apply F_REPL1.
assumption.
apply H1; inversion_clear H2; apply notin_nu; intros.
cut (notin x (par (r z) (frepl1 p (t z) n))); [ intro | auto ].
inversion_clear H5.
apply FREPL1_NOTIN with p n; assumption.
inversion_clear H3.
cut (notin x (par (s z) (frepl1 q (u z) n))); [ intro | auto ].
inversion_clear H3.
apply FREPL1_NOTIN with q n; assumption.

simpl in |- *; apply PAR_S2; [ assumption | apply H; auto ].

Qed.

Lemma CF_B_ACT_NOTIN :
(p : proc) (q : name proc) (n : nat) (x : name),
notin x (nu (cf_b_act p q n)) notin x (nu q).

Proof.

simple induction n; intros.

simpl in H; inversion_clear H; apply notin_nu; intros.
cut (notin x (par (q z) (bang p))); [ intro | auto ].
inversion_clear H1; assumption.

simpl in H0; inversion_clear H0; apply H; auto.
apply notin_nu; intros.
cut (notin x (par p (cf_b_act p q n0 z))); [ intro | auto ].
inversion_clear H2; assumption.

Qed.

Lemma BANG_FTR_AUX :
(p q : proc) (a : f_act) (n : nat),
ftrans p a q ftrans (bang p) a (cf_f_act p q n).

Proof.

simple induction n; intros.
simpl in |- *; apply fBANG; apply fPAR1; assumption.
simpl in |- *; apply fBANG; apply fPAR2; apply H; auto.

Qed.

Lemma BANG_BTR_AUX :
(p : proc) (q : name proc) (a : b_act) (n : nat),
btrans p a q btrans (bang p) a (cf_b_act p q n).

Proof.

simple induction n; intros.
simpl in |- *; apply bBANG; apply bPAR1; assumption.
simpl in |- *; apply bBANG; apply bPAR2; apply H; auto.

Qed.

Lemma BANG_TAU_AUX1 :
(p q : proc) (r : name proc) (x y : name) (n m : nat),
ftrans p (Out x y) q
btrans p (In x) r ftrans (bang p) tau (cf_tau1 p q r y n m).

Proof.

simple induction m; intros.
simpl in |- *; apply fBANG; apply COM1 with x;
[ assumption | apply BANG_FTR_AUX; assumption ].
simpl in |- *; apply fBANG; apply fPAR2; apply H; assumption.

Qed.

Lemma BANG_TAU_AUX2 :
(p q : proc) (r : name proc) (x y : name) (n m : nat),
ftrans p (Out x y) q
btrans p (In x) r ftrans (bang p) tau (cf_tau2 p q r y n m).

Proof.

simple induction m; intros.
simpl in |- *; apply fBANG; apply COM2 with x;
[ assumption | apply BANG_BTR_AUX; assumption ].
simpl in |- *; apply fBANG; apply fPAR2; apply H; assumption.

Qed.

Lemma BANG_TAU_AUX3 :
(p : proc) (q r : name proc) (x : name) (n m : nat),
btrans p (In x) q
btrans p (bOut x) r ftrans (bang p) tau (cf_tau3 p q r n m).

Proof.

simple induction m; intros.
simpl in |- *; apply fBANG; apply CLOSE1 with x;
[ assumption | apply BANG_BTR_AUX; assumption ].
simpl in |- *; apply fBANG; apply fPAR2; apply H; assumption.

Qed.

Lemma BANG_TAU_AUX4 :
(p : proc) (q r : name proc) (x : name) (n m : nat),
btrans p (bOut x) q
btrans p (In x) r ftrans (bang p) tau (cf_tau3 p q r n m).

Proof.

simple induction m; intros.
simpl in |- *; apply fBANG; apply CLOSE2 with x;
[ assumption | apply BANG_BTR_AUX; assumption ].
simpl in |- *; apply fBANG; apply fPAR2; apply H; assumption.

Qed.

Inductive BisBANG_S : proc proc Prop :=
bisbang_s :
p q : proc,
StBisim p q
r s : proc,
StBisim r s BisBANG_S (par r (bang p)) (par s (bang q)).

Lemma BANG_S_L6 :
(p q : name proc) (x : name),
notin x (nu p)
notin x (nu q)
BisBANG_S (p x) (q x)
y : name, notin y (nu p) notin y (nu q) BisBANG_S (p y) (q y).

Proof.

intros; elim (LEM_name x y); intro.

rewrite <- H4; assumption.

inversion H1.
elim (proc_exp r x); elim (proc_exp s x); elim (proc_exp p0 x);
elim (proc_exp q0 x); intros.
inversion_clear H9; inversion_clear H10; inversion_clear H11;
inversion_clear H12.
rewrite H14 in H6; rewrite H15 in H5; rewrite H16 in H6; rewrite H17 in H5.
cut (p = (fun n : namepar (x3 n) (bang (x1 n))));
[ intro | apply proc_ext with x; auto ].
cut (q = (fun n : namepar (x2 n) (bang (x0 n))));
[ intro | apply proc_ext with x; auto ].
rewrite H12; rewrite H18; apply bisbang_s; auto.
rewrite H14 in H7; rewrite H15 in H7; apply L6_Light with x; auto.
rewrite H12 in H2; inversion_clear H2; apply notin_nu; intros;
cut (notin y (par (x3 z) (bang (x1 z)))); [ intro | auto ];
inversion_clear H15; inversion_clear H20; inversion_clear H21;
assumption.
rewrite H18 in H3; inversion_clear H3; apply notin_nu; intros;
cut (notin y (par (x2 z) (bang (x0 z)))); [ intro | auto ];
inversion_clear H15; inversion_clear H20; inversion_clear H21;
assumption.
rewrite H16 in H8; rewrite H17 in H8; apply L6_Light with x; auto.
rewrite H12 in H2; inversion_clear H2; apply notin_nu; intros;
cut (notin y (par (x3 z) (bang (x1 z)))); [ intro | auto ];
inversion_clear H15; inversion_clear H20; assumption.
rewrite H18 in H3; inversion_clear H3; apply notin_nu; intros;
cut (notin y (par (x2 z) (bang (x0 z)))); [ intro | auto ];
inversion_clear H15; inversion_clear H20; assumption.
apply notin_nu; intros; apply notin_par;
[ inversion_clear H10; auto | apply notin_bang; inversion_clear H13; auto ].
apply notin_nu; intros; apply notin_par;
[ inversion_clear H11; auto | apply notin_bang; inversion_clear H9; auto ].

Qed.

Lemma BisBANG_S_FTR1 :
p q : proc,
BisBANG_S p q
x y : name,
( p1 : proc,
ftrans p (Out x y) p1
q1 : proc, ftrans q (Out x y) q1 SB_R_SB BisBANG_S p1 q1)
( q1 : proc,
ftrans q (Out x y) q1
p1 : proc, ftrans p (Out x y) p1 SB_R_SB BisBANG_S p1 q1).

Proof.

intros; inversion H; split; intros.

inversion H4.

inversion_clear H1; inversion_clear H10.
elim (H1 (Out x y)); intros.
elim (H10 p4 H9); intros; inversion_clear H13.
(par x0 (bang q0)); split;
[ apply fPAR1; assumption
| unfold SB_R_SB in |- *; (par p4 (bang p0));
(par x0 (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_OUT p0 p4 x y H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11.
elim (H15 (Out x y)); intros.
elim (H11 x0 H12); intros; inversion_clear H18.
(par s (cf_f_act q0 x2 x1)); split.
apply fPAR2; apply BANG_FTR_AUX; assumption.
rewrite H10; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 x0 x1)) (bang p0));
(par (par s (frepl1 q0 x2 x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 x0 x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2;
[ assumption | apply F_REPL1; assumption ]
| apply TRANS with (par s (par (frepl1 q0 x2 x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT; assumption ] ] ].

inversion H4.

inversion_clear H1; inversion_clear H10.
elim (H1 (Out x y)); intros.
elim (H12 p3 H9); intros; inversion_clear H13.
(par x0 (bang p0)); split;
[ apply fPAR1; assumption
| unfold SB_R_SB in |- *; (par x0 (bang p0));
(par p3 (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_OUT q0 p3 x y H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11.
elim (H15 (Out x y)); intros.
elim (H17 x0 H12); intros; inversion_clear H18.
(par r (cf_f_act p0 x2 x1)); split.
apply fPAR2; apply BANG_FTR_AUX; assumption.
rewrite H10; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 x2 x1)) (bang p0));
(par (par s (frepl1 q0 x0 x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 x2 x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2;
[ assumption | apply F_REPL1; assumption ]
| apply TRANS with (par s (par (frepl1 q0 x0 x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT; assumption ] ] ].

Qed.

Lemma BisBANG_S_IN :
p q : proc,
BisBANG_S p q
x : name,
( p1 : name proc,
btrans p (In x) p1
q1 : name proc,
btrans q (In x) q1 ( y : name, SB_R_SB BisBANG_S (p1 y) (q1 y)))
( q1 : name proc,
btrans q (In x) q1
p1 : name proc,
btrans p (In x) p1 ( y : name, SB_R_SB BisBANG_S (p1 y) (q1 y))).

Proof.

intros; inversion H; split; intros.

inversion H4.

inversion_clear H1; inversion_clear H10; inversion_clear H11.
elim (H10 x); intros.
elim (H11 p4 H9); intros; inversion_clear H14.
(fun n : namepar (x0 n) (bang q0)); split;
[ apply bPAR1; assumption
| intro; unfold SB_R_SB in |- *; (par (p4 y) (bang p0));
(par (x0 y) (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_BTR p0 p4 (In x) H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11; inversion_clear H16.
elim (H11 x); intros.
elim (H16 x0 H12); intros; inversion_clear H19.
(fun n : namepar s (cf_b_act q0 x2 x1 n)); split.
apply bPAR2; apply BANG_BTR_AUX; assumption.
rewrite H10; intro; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 (x0 y) x1)) (bang p0));
(par (par s (frepl1 q0 (x2 y) x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 (x0 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2; [ assumption | apply F_REPL1; auto ]
| apply TRANS with (par s (par (frepl1 q0 (x2 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

inversion H4.

inversion_clear H1; inversion_clear H10; inversion_clear H11.
elim (H10 x); intros.
elim (H13 p3 H9); intros; inversion_clear H14.
(fun n : namepar (x0 n) (bang p0)); split;
[ apply bPAR1; assumption
| intro; unfold SB_R_SB in |- *; (par (x0 y) (bang p0));
(par (p3 y) (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_BTR q0 p3 (In x) H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11; inversion_clear H16.
elim (H11 x); intros.
elim (H18 x0 H12); intros; inversion_clear H19.
(fun n : namepar r (cf_b_act p0 x2 x1 n)); split.
apply bPAR2; apply BANG_BTR_AUX; assumption.
rewrite H10; intro; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 (x2 y) x1)) (bang p0));
(par (par s (frepl1 q0 (x0 y) x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 (x2 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2; [ assumption | apply F_REPL1; auto ]
| apply TRANS with (par s (par (frepl1 q0 (x0 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

Qed.

Lemma BisBANG_S_bOUT :
p q : proc,
BisBANG_S p q
x : name,
( p1 : name proc,
btrans p (bOut x) p1
q1 : name proc,
btrans q (bOut x) q1
( y : name,
notin y (nu p1) notin y (nu q1) SB_R_SB BisBANG_S (p1 y) (q1 y)))
( q1 : name proc,
btrans q (bOut x) q1
p1 : name proc,
btrans p (bOut x) p1
( y : name,
notin y (nu p1) notin y (nu q1) SB_R_SB BisBANG_S (p1 y) (q1 y))).

Proof.

intros; inversion H; split; intros.

inversion H4.

inversion_clear H1; inversion_clear H10; inversion_clear H11.
elim (H12 x); intros.
elim (H11 p4 H9); intros; inversion_clear H14.
(fun n : namepar (x0 n) (bang q0)); split;
[ apply bPAR1; assumption
| intros; unfold SB_R_SB in |- *; (par (p4 y) (bang p0));
(par (x0 y) (bang q0)); split;
[ apply REF
| split; [ apply bisbang_s; auto; apply H16; auto | apply REF ] ] ].
inversion_clear H14; apply notin_nu; intros;
cut (notin y (par (p4 z) (bang p0))); [ intro | auto ];
inversion_clear H19; auto.
inversion_clear H17; apply notin_nu; intros;
cut (notin y (par (x0 z) (bang q0))); [ intro | auto ];
inversion_clear H19; auto.

elim (BANG_BTR p0 p4 (bOut x) H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11; inversion_clear H16.
elim (H17 x); intros.
elim (H16 x0 H12); intros; inversion_clear H19.
(fun n : namepar s (cf_b_act q0 x2 x1 n)); split.
apply bPAR2; apply BANG_BTR_AUX; assumption.
rewrite H10; intros; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 (x0 y) x1)) (bang p0));
(par (par s (frepl1 q0 (x2 y) x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 (x0 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2;
[ assumption
| apply F_REPL1; auto; apply H21;
[ apply CF_B_ACT_NOTIN with p0 x1; apply notin_nu; intros;
inversion_clear H19; cut (notin y (par r (cf_b_act p0 x0 x1 z)));
[ intro | auto ]; inversion_clear H19; auto
| apply CF_B_ACT_NOTIN with q0 x1; apply notin_nu; intros;
inversion_clear H22; cut (notin y (par s (cf_b_act q0 x2 x1 z)));
[ intro | auto ]; inversion_clear H22; auto ] ]
| apply TRANS with (par s (par (frepl1 q0 (x2 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

inversion H4.

inversion_clear H1; inversion_clear H10; inversion_clear H11.
elim (H12 x); intros.
elim (H13 p3 H9); intros; inversion_clear H14.
(fun n : namepar (x0 n) (bang p0)); split;
[ apply bPAR1; assumption
| intros; unfold SB_R_SB in |- *; (par (x0 y) (bang p0));
(par (p3 y) (bang q0)); split;
[ apply REF
| split; [ apply bisbang_s; auto; apply H16; auto | apply REF ] ] ].
inversion_clear H14; apply notin_nu; intros;
cut (notin y (par (x0 z) (bang p0))); [ intro | auto ];
inversion_clear H19; auto.
inversion_clear H17; apply notin_nu; intros;
cut (notin y (par (p3 z) (bang q0))); [ intro | auto ];
inversion_clear H19; auto.

elim (BANG_BTR q0 p3 (bOut x) H9); intros; inversion_clear H10;
inversion_clear H11.
inversion H0; inversion_clear H11; inversion_clear H16.
elim (H17 x); intros.
elim (H18 x0 H12); intros; inversion_clear H19.
(fun n : namepar r (cf_b_act p0 x2 x1 n)); split.
apply bPAR2; apply BANG_BTR_AUX; assumption.
rewrite H10; intros; unfold SB_R_SB in |- *;
(par (par r (frepl1 p0 (x2 y) x1)) (bang p0));
(par (par s (frepl1 q0 (x0 y) x1)) (bang q0));
split.
apply TRANS with (par r (par (frepl1 p0 (x2 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s; auto; apply PAR_S2;
[ assumption
| apply F_REPL1; auto; apply H21;
[ apply CF_B_ACT_NOTIN with p0 x1; apply notin_nu; intros;
inversion_clear H19; cut (notin y (par r (cf_b_act p0 x2 x1 z)));
[ intro | auto ]; inversion_clear H19; auto
| apply CF_B_ACT_NOTIN with q0 x1; apply notin_nu; intros;
inversion_clear H22; cut (notin y (par s (cf_b_act q0 x0 x1 z)));
[ intro | auto ]; inversion_clear H22; auto ] ]
| apply TRANS with (par s (par (frepl1 q0 (x0 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

Qed.

Lemma BisBANG_S_FTR2 :
p q : proc,
BisBANG_S p q
( p1 : proc,
ftrans p tau p1
q1 : proc,
ftrans q tau q1
(( p1' : proc,
( q1' : proc,
StBisim p1 p1' BisBANG_S p1' q1' StBisim q1' q1))
( p1' : name proc,
( q1' : name proc,
StBisim p1 (nu p1')
( z : name,
notin z (nu p1') notin z (nu q1') BisBANG_S (p1' z) (q1' z))
StBisim (nu q1') q1))))
( q1 : proc,
ftrans q tau q1
p1 : proc,
ftrans p tau p1
(( p1' : proc,
( q1' : proc,
StBisim p1 p1' BisBANG_S p1' q1' StBisim q1' q1))
( p1' : name proc,
( q1' : name proc,
StBisim p1 (nu p1')
( z : name,
notin z (nu p1') notin z (nu q1') BisBANG_S (p1' z) (q1' z))
StBisim (nu q1') q1)))).

Proof.

intros; inversion H; split; intros.

inversion H4.

inversion_clear H1; inversion_clear H10.
elim (H1 tau); intros.
elim (H10 p4 H9); intros; inversion_clear H13.
(par x (bang q0)); split;
[ apply fPAR1; assumption
| left; (par p4 (bang p0)); (par x (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_TAU p0 p4 H9); intros; inversion_clear H10; inversion_clear H11;
inversion_clear H10.
inversion H0; inversion_clear H10.
elim (H15 tau); intros.
elim (H10 x H12); intros; inversion_clear H18.
(par s (cf_f_act q0 x1 x0)); split;
[ apply fPAR2; apply BANG_FTR_AUX; assumption
| rewrite H11; left; (par (par r (frepl1 p0 x x0)) (bang p0));
(par (par s (frepl1 q0 x1 x0)) (bang q0));
split ].
apply TRANS with (par r (par (frepl1 p0 x x0) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL1; assumption ] ]
| apply TRANS with (par s (par (frepl1 q0 x1 x0) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H16 (Out x1 x2)); elim (H12 x1); intros.
elim (H17 x0 H13); elim (H20 x H11); intros; inversion_clear H22;
inversion_clear H23.
(par s (cf_tau1 q0 x5 x6 x2 x3 x4)); split;
[ apply fPAR2; apply BANG_TAU_AUX1 with x1; assumption
| rewrite H10; left;
(par (par r (frepl2 p0 x x0 x2 x3 x4)) (bang p0));
(par (par s (frepl2 q0 x5 x6 x2 x3 x4)) (bang q0));
split ].
apply TRANS with (par r (par (frepl2 p0 x x0 x2 x3 x4) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU1 ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL2; auto ] ]
| apply TRANS with (par s (par (frepl2 q0 x5 x6 x2 x3 x4) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU1 ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H16 (Out x1 x2)); elim (H12 x1); intros.
elim (H17 x0 H13); elim (H20 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par s (cf_tau2 q0 x5 x6 x2 x3 x4)); split;
[ apply fPAR2; apply BANG_TAU_AUX2 with x1; assumption
| rewrite H11; left;
(par (par r (frepl3 p0 x x0 x2 x3 x4)) (bang p0));
(par (par s (frepl3 q0 x5 x6 x2 x3 x4)) (bang q0));
split ].
apply TRANS with (par r (par (frepl3 p0 x x0 x2 x3 x4) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU2 ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL3; auto ] ]
| apply TRANS with (par s (par (frepl3 q0 x5 x6 x2 x3 x4) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU2 ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H12 x1); elim (H18 x1); intros.
elim (H17 x0 H13); elim (H20 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par s (cf_tau3 q0 x4 x5 x2 x3)); split.
apply fPAR2; apply BANG_TAU_AUX3 with x1; assumption.
rewrite H11; left; (par (par r (frepl4 p0 x x0 x2 x3)) (bang p0));
(par (par s (frepl4 q0 x4 x5 x2 x3)) (bang q0));
split.
apply TRANS with (par r (par (frepl4 p0 x x0 x2 x3) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU3; auto ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL4; auto ] ]
| apply TRANS with (par s (par (frepl4 q0 x4 x5 x2 x3) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU3; assumption ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H12 x1); elim (H18 x1); intros.
elim (H17 x0 H13); elim (H20 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par s (cf_tau3 q0 x5 x4 x2 x3)); split.
apply fPAR2; apply BANG_TAU_AUX4 with x1; assumption.
rewrite H11; left; (par (par r (frepl4 p0 x0 x x2 x3)) (bang p0));
(par (par s (frepl4 q0 x5 x4 x2 x3)) (bang q0));
split.
apply TRANS with (par r (par (frepl4 p0 x0 x x2 x3) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU3; auto ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL4; auto ] ]
| apply TRANS with (par s (par (frepl4 q0 x5 x4 x2 x3) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU3; assumption ] ] ].

elim (BANG_OUT p0 q2 x y H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H20.
elim (H18 (Out x y)); elim (H15 x); intros.
elim (H20 q1 H7); elim (H23 x0 H12); intros; inversion_clear H25;
inversion_clear H26.
(par (x3 y) (cf_f_act q0 x2 x1)); split.
apply COM1 with x; [ assumption | apply BANG_FTR_AUX; assumption ].
rewrite H10; left; (par (par (q1 y) (frepl1 p0 x0 x1)) (bang p0));
(par (par (x3 y) (frepl1 q0 x2 x1)) (bang q0));
split.
apply TRANS with (par (q1 y) (par (frepl1 p0 x0 x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ auto | apply F_REPL1; assumption ] ]
| apply TRANS with (par (x3 y) (par (frepl1 q0 x2 x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT; assumption ] ] ].

elim (BANG_BTR p0 q2 (In x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19.
elim (H11 (Out x y)); elim (H15 x); intros.
elim (H19 x0 H12); elim (H23 q1 H7); intros; inversion_clear H25;
inversion_clear H26.
(par x2 (cf_b_act q0 x3 x1 y)); split.
apply COM2 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; left; (par (par q1 (frepl1 p0 (x0 y) x1)) (bang p0));
(par (par x2 (frepl1 q0 (x3 y) x1)) (bang q0));
split.
apply TRANS with (par q1 (par (frepl1 p0 (x0 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ auto | apply F_REPL1; auto ] ]
| apply TRANS with (par x2 (par (frepl1 q0 (x3 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

elim (BANG_BTR p0 q2 (bOut x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19; inversion_clear H20.
elim (H19 x); elim (H21 x); intros.
elim (H20 x0 H12); elim (H24 q1 H7); intros; inversion_clear H26;
inversion_clear H27.
(nu (fun n : namepar (x2 n) (cf_b_act q0 x3 x1 n))); split.
apply CLOSE1 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; right.
(fun n : namepar (par (q1 n) (frepl1 p0 (x0 n) x1)) (bang p0));
(fun n : namepar (par (x2 n) (frepl1 q0 (x3 n) x1)) (bang q0));
split.
apply NU_S; intros;
apply TRANS with (par (q1 x4) (par (frepl1 p0 (x0 x4) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ intros; apply bisbang_s;
[ assumption
| apply PAR_S2;
[ auto
| apply F_REPL1; auto; apply H30;
[ apply notin_nu; intros; apply FREPL1_NOTIN with p0 x1;
inversion_clear H27;
cut
(notin z (par (par (q1 z0) (frepl1 p0 (x0 z0) x1)) (bang p0)));
[ intro | auto ]; inversion_clear H27;
inversion_clear H34; assumption
| apply notin_nu; intros; apply FREPL1_NOTIN with q0 x1;
inversion_clear H31;
cut
(notin z (par (par (x2 z0) (frepl1 q0 (x3 z0) x1)) (bang q0)));
[ intro | auto ]; inversion_clear H31;
inversion_clear H34; assumption ] ] ]
| apply NU_S; intros;
apply TRANS with (par (x2 x4) (par (frepl1 q0 (x3 x4) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

elim (BANG_BTR p0 q2 (In x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19; inversion_clear H20.
elim (H15 x); elim (H22 x); intros.
elim (H20 q1 H7); elim (H24 x0 H12); intros; inversion_clear H26;
inversion_clear H27.
(nu (fun n : namepar (x3 n) (cf_b_act q0 x2 x1 n))); split.
apply CLOSE2 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; right.
(fun n : namepar (par (q1 n) (frepl1 p0 (x0 n) x1)) (bang p0));
(fun n : namepar (par (x3 n) (frepl1 q0 (x2 n) x1)) (bang q0));
split.
apply NU_S; intros;
apply TRANS with (par (q1 x4) (par (frepl1 p0 (x0 x4) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ intros; apply bisbang_s;
[ assumption
| apply PAR_S2;
[ apply H30;
[ apply notin_nu; intros; inversion_clear H27;
cut
(notin z (par (par (q1 z0) (frepl1 p0 (x0 z0) x1)) (bang p0)));
[ intro | auto ]; inversion_clear H27;
inversion_clear H34; assumption
| apply notin_nu; intros; inversion_clear H31;
cut
(notin z (par (par (x3 z0) (frepl1 q0 (x2 z0) x1)) (bang q0)));
[ intro | auto ]; inversion_clear H31;
inversion_clear H34; assumption ]
| apply F_REPL1; auto ] ]
| apply NU_S; intros;
apply TRANS with (par (x3 x4) (par (frepl1 q0 (x2 x4) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

inversion H4.

inversion_clear H1; inversion_clear H10.
elim (H1 tau); intros.
elim (H12 p3 H9); intros; inversion_clear H13.
(par x (bang p0)); split;
[ apply fPAR1; assumption
| left; (par x (bang p0)); (par p3 (bang q0)); split;
[ apply REF | split; [ apply bisbang_s; auto | apply REF ] ] ].

elim (BANG_TAU q0 p3 H9); intros; inversion_clear H10; inversion_clear H11;
inversion_clear H10.
inversion H0; inversion_clear H10.
elim (H15 tau); intros.
elim (H17 x H12); intros; inversion_clear H18.
(par r (cf_f_act p0 x1 x0)); split;
[ apply fPAR2; apply BANG_FTR_AUX; assumption
| rewrite H11; left; (par (par r (frepl1 p0 x1 x0)) (bang p0));
(par (par s (frepl1 q0 x x0)) (bang q0));
split ].
apply TRANS with (par r (par (frepl1 p0 x1 x0) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL1; assumption ] ]
| apply TRANS with (par s (par (frepl1 q0 x x0) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H16 (Out x1 x2)); elim (H12 x1); intros.
elim (H19 x0 H13); elim (H21 x H11); intros; inversion_clear H22;
inversion_clear H23.
(par r (cf_tau1 p0 x5 x6 x2 x3 x4)); split;
[ apply fPAR2; apply BANG_TAU_AUX1 with x1; assumption
| rewrite H10; left;
(par (par r (frepl2 p0 x5 x6 x2 x3 x4)) (bang p0));
(par (par s (frepl2 q0 x x0 x2 x3 x4)) (bang q0));
split ].
apply TRANS with (par r (par (frepl2 p0 x5 x6 x2 x3 x4) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU1 ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL2; auto ] ]
| apply TRANS with (par s (par (frepl2 q0 x x0 x2 x3 x4) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU1 ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H16 (Out x1 x2)); elim (H12 x1); intros.
elim (H19 x0 H13); elim (H21 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par r (cf_tau2 p0 x5 x6 x2 x3 x4)); split;
[ apply fPAR2; apply BANG_TAU_AUX2 with x1; assumption
| rewrite H11; left;
(par (par r (frepl3 p0 x5 x6 x2 x3 x4)) (bang p0));
(par (par s (frepl3 q0 x x0 x2 x3 x4)) (bang q0));
split ].
apply TRANS with (par r (par (frepl3 p0 x5 x6 x2 x3 x4) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU2 ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL3; auto ] ]
| apply TRANS with (par s (par (frepl3 q0 x x0 x2 x3 x4) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU2 ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H12 x1); elim (H18 x1); intros.
elim (H19 x0 H13); elim (H21 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par r (cf_tau3 p0 x4 x5 x2 x3)); split.
apply fPAR2; apply BANG_TAU_AUX3 with x1; assumption.
rewrite H11; left; (par (par r (frepl4 p0 x4 x5 x2 x3)) (bang p0));
(par (par s (frepl4 q0 x x0 x2 x3)) (bang q0));
split.
apply TRANS with (par r (par (frepl4 p0 x4 x5 x2 x3) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU3; auto ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL4; auto ] ]
| apply TRANS with (par s (par (frepl4 q0 x x0 x2 x3) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU3; assumption ] ] ].

inversion_clear H11; inversion_clear H10; inversion_clear H11;
inversion_clear H10; inversion_clear H11; inversion_clear H10;
inversion_clear H12.
inversion H0; inversion_clear H12; inversion_clear H17.
elim (H12 x1); elim (H18 x1); intros.
elim (H19 x0 H13); elim (H21 x H10); intros; inversion_clear H22;
inversion_clear H23.
(par r (cf_tau3 p0 x5 x4 x2 x3)); split.
apply fPAR2; apply BANG_TAU_AUX4 with x1; assumption.
rewrite H11; left; (par (par r (frepl4 p0 x5 x4 x2 x3)) (bang p0));
(par (par s (frepl4 q0 x0 x x2 x3)) (bang q0));
split.
apply TRANS with (par r (par (frepl4 p0 x5 x4 x2 x3) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_TAU3; auto ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ assumption | apply F_REPL4; auto ] ]
| apply TRANS with (par s (par (frepl4 q0 x0 x x2 x3) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_TAU3; assumption ] ] ].

elim (BANG_OUT q0 q2 x y H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H20.
elim (H18 (Out x y)); elim (H15 x); intros.
elim (H22 q3 H7); elim (H24 x0 H12); intros; inversion_clear H25;
inversion_clear H26.
(par (x3 y) (cf_f_act p0 x2 x1)); split.
apply COM1 with x; [ assumption | apply BANG_FTR_AUX; assumption ].
rewrite H10; left; (par (par (x3 y) (frepl1 p0 x2 x1)) (bang p0));
(par (par (q3 y) (frepl1 q0 x0 x1)) (bang q0));
split.
apply TRANS with (par (x3 y) (par (frepl1 p0 x2 x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_F_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ auto | apply F_REPL1; assumption ] ]
| apply TRANS with (par (q3 y) (par (frepl1 q0 x0 x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_F_ACT; assumption ] ] ].

elim (BANG_BTR q0 q3 (In x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19.
elim (H11 (Out x y)); elim (H15 x); intros.
elim (H22 x0 H12); elim (H24 q2 H7); intros; inversion_clear H25;
inversion_clear H26.
(par x2 (cf_b_act p0 x3 x1 y)); split.
apply COM2 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; left; (par (par x2 (frepl1 p0 (x3 y) x1)) (bang p0));
(par (par q2 (frepl1 q0 (x0 y) x1)) (bang q0));
split.
apply TRANS with (par x2 (par (frepl1 p0 (x3 y) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ apply bisbang_s;
[ assumption | apply PAR_S2; [ auto | apply F_REPL1; auto ] ]
| apply TRANS with (par q2 (par (frepl1 q0 (x0 y) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

elim (BANG_BTR q0 q3 (bOut x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19; inversion_clear H20.
elim (H19 x); elim (H21 x); intros.
elim (H23 x0 H12); elim (H25 q2 H7); intros; inversion_clear H26;
inversion_clear H27.
(nu (fun n : namepar (x2 n) (cf_b_act p0 x3 x1 n))); split.
apply CLOSE1 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; right.
(fun n : namepar (par (x2 n) (frepl1 p0 (x3 n) x1)) (bang p0));
(fun n : namepar (par (q2 n) (frepl1 q0 (x0 n) x1)) (bang q0));
split.
apply NU_S; intros;
apply TRANS with (par (x2 x4) (par (frepl1 p0 (x3 x4) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ intros; apply bisbang_s;
[ assumption
| apply PAR_S2;
[ auto
| apply F_REPL1; auto; apply H30;
[ apply notin_nu; intros; apply FREPL1_NOTIN with p0 x1;
inversion_clear H27;
cut
(notin z (par (par (x2 z0) (frepl1 p0 (x3 z0) x1)) (bang p0)));
[ intro | auto ]; inversion_clear H27;
inversion_clear H34; assumption
| apply notin_nu; intros; apply FREPL1_NOTIN with q0 x1;
inversion_clear H31;
cut
(notin z (par (par (q2 z0) (frepl1 q0 (x0 z0) x1)) (bang q0)));
[ intro | auto ]; inversion_clear H31;
inversion_clear H34; assumption ] ] ]
| apply NU_S; intros;
apply TRANS with (par (q2 x4) (par (frepl1 q0 (x0 x4) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

elim (BANG_BTR q0 q3 (In x) H8); intros; inversion_clear H10;
inversion_clear H11; inversion H0; inversion H1; inversion_clear H11;
inversion_clear H15; inversion_clear H19; inversion_clear H20.
elim (H15 x); elim (H22 x); intros.
elim (H23 q2 H7); elim (H25 x0 H12); intros; inversion_clear H26;
inversion_clear H27.
(nu (fun n : namepar (x3 n) (cf_b_act p0 x2 x1 n))); split.
apply CLOSE2 with x; [ assumption | apply BANG_BTR_AUX; assumption ].
rewrite H10; right.
(fun n : namepar (par (x3 n) (frepl1 p0 (x2 n) x1)) (bang p0));
(fun n : namepar (par (q2 n) (frepl1 q0 (x0 n) x1)) (bang q0));
split.
apply NU_S; intros;
apply TRANS with (par (x3 x4) (par (frepl1 p0 (x2 x4) x1) (bang p0)));
[ apply PAR_S2; [ apply REF | apply SB_CF_B_ACT; assumption ]
| apply SYM; apply ASS_PAR ].
split;
[ intros; apply bisbang_s;
[ assumption
| apply PAR_S2;
[ apply H30;
[ apply notin_nu; intros; inversion_clear H27;
cut
(notin z (par (par (x3 z0) (frepl1 p0 (x2 z0) x1)) (bang p0)));
[ intro | auto ]; inversion_clear H27;
inversion_clear H34; assumption
| apply notin_nu; intros; inversion_clear H31;
cut
(notin z (par (par (q2 z0) (frepl1 q0 (x0 z0) x1)) (bang q0)));
[ intro | auto ]; inversion_clear H31;
inversion_clear H34; assumption ]
| apply F_REPL1; auto ] ]
| apply NU_S; intros;
apply TRANS with (par (q2 x4) (par (frepl1 q0 (x0 x4) x1) (bang q0)));
[ apply ASS_PAR
| apply PAR_S2; [ apply REF | apply SYM; apply SB_CF_B_ACT; assumption ] ] ].

Qed.

Lemma BisBANG_S_UPTO : UpTo BisBANG_S.

Proof.

unfold UpTo in |- *; intros.

split; intros.

rewrite H2 in H; rewrite H3 in H; apply BANG_S_L6 with x; auto.

split; intros.

apply BisBANG_S_FTR1; auto.

split; intros.

apply BisBANG_S_IN; assumption.

split; intros.

apply BisBANG_S_bOUT; assumption.

apply BisBANG_S_FTR2; assumption.

Qed.

Lemma BANG_S : p q : proc, StBisim p q StBisim (bang p) (bang q).

Proof.

intros; apply Completeness; apply Co_Ind with (SBUPTO BisBANG_S);
[ apply UPTO_SB'; exact BisBANG_S_UPTO
| apply sbupto with 0; simpl in |- *; unfold SB_R_SB in |- *;
(par nil (bang p)); (par nil (bang q));
split;
[ apply SYM; apply TRANS with (par (bang p) nil);
[ apply COMM_PAR | apply ID_PAR ]
| split;
[ apply bisbang_s; [ assumption | apply REF ]
| apply TRANS with (par (bang q) nil);
[ apply COMM_PAR | apply ID_PAR ] ] ] ].

Qed.

End structural_congruence3.