Library PiCalc.alglaws
Require Export basiclemmata.
Lemma REF : forall p : proc, StBisim p p.
Proof.
cofix; intro; apply sb; do 3 try (split; intros).
exists p1; split; auto.
exists q1; split; auto.
exists p1; split; [ assumption | intro; auto ].
exists q1; split; [ assumption | intro; auto ].
exists p1; split; [ assumption | intros; auto ].
exists q1; split; [ assumption | intros; auto ].
Qed.
Lemma SYM : forall p q : proc, StBisim p q -> StBisim q p.
Proof.
cofix; intros; apply sb; do 3 try (split; intros).
inversion H.
elim H1; intros.
elim (H4 a); intros.
elim (H7 p1 H0); intros.
elim H8; intros; exists x; split; [ assumption | apply SYM; assumption ].
inversion H.
elim H1; intros.
elim (H4 a); intros.
elim (H6 q1 H0); intros.
elim H8; intros; exists x; split; [ assumption | apply SYM; assumption ].
inversion H.
elim H1; intros.
elim H5; intros.
elim (H6 x); intros.
elim (H9 p1 H0); intros.
elim H10; intros; exists x0; split; [ assumption | intro; apply SYM; auto ].
inversion H.
elim H1; intros.
elim H5; intros.
elim (H6 x); intros.
elim (H8 q1 H0); intros.
elim H10; intros; exists x0; split; [ assumption | intro; apply SYM; auto ].
inversion H.
elim H1; intros.
elim H5; intros.
elim (H7 x); intros.
elim (H9 p1 H0); intros.
elim H10; intros; exists x0; split;
[ assumption | intros; apply SYM; apply H12; auto ].
inversion H.
elim H1; intros.
elim H5; intros.
elim (H7 x); intros.
elim (H8 q1 H0); intros.
elim H10; intros; exists x0; split;
[ assumption | intros; apply SYM; apply H12; auto ].
Qed.
Lemma TRANS : forall p q r : proc, StBisim p q -> StBisim q r -> StBisim p r.
Proof.
cofix.
do 4 intro.
inversion_clear H.
intro.
inversion_clear H.
apply sb.
split.
intro.
cut
((forall p1 : proc,
ftrans p a p1 -> exists q1 : proc, ftrans q a q1 /\ StBisim p1 q1) /\
(forall q1 : proc,
ftrans q a q1 -> exists p1 : proc, ftrans p a p1 /\ StBisim p1 q1)).
intro.
cut
((forall p1 : proc,
ftrans q a p1 -> exists q1 : proc, ftrans r a q1 /\ StBisim p1 q1) /\
(forall q1 : proc,
ftrans r a q1 -> exists p1 : proc, ftrans q a p1 /\ StBisim p1 q1)).
intro.
inversion_clear H.
inversion_clear H2.
split.
intros.
cut (exists q1 : proc, ftrans q a q1 /\ StBisim p1 q1).
intro.
inversion_clear H6.
cut (exists q1 : proc, ftrans r a q1 /\ StBisim x q1).
intro.
inversion_clear H6.
exists x0.
split.
tauto.
apply TRANS with x.
tauto.
tauto.
apply H.
tauto.
apply H3.
assumption.
intros.
cut (exists p1 : proc, ftrans q a p1 /\ StBisim p1 q1).
intro.
inversion_clear H6.
cut (exists p1 : proc, ftrans p a p1 /\ StBisim p1 x).
intro.
inversion_clear H6.
exists x0.
split.
tauto.
apply TRANS with x.
tauto.
tauto.
apply H4.
tauto.
apply H5.
assumption.
elim H1.
intros.
apply H2.
elim H0.
intros.
apply H.
split.
intro.
cut
((forall p1 : name -> proc,
btrans p (In x) p1 ->
exists q1 : name -> proc,
btrans q (In x) q1 /\ (forall y : name, StBisim (p1 y) (q1 y))) /\
(forall q1 : name -> proc,
btrans q (In x) q1 ->
exists p1 : name -> proc,
btrans p (In x) p1 /\ (forall y : name, StBisim (p1 y) (q1 y)))).
intro.
cut
((forall p1 : name -> proc,
btrans q (In x) p1 ->
exists q1 : name -> proc,
btrans r (In x) q1 /\ (forall y : name, StBisim (p1 y) (q1 y))) /\
(forall q1 : name -> proc,
btrans r (In x) q1 ->
exists p1 : name -> proc,
btrans q (In x) p1 /\ (forall y : name, StBisim (p1 y) (q1 y)))).
intro.
inversion_clear H.
inversion_clear H2.
split.
intros.
cut
(exists q1 : name -> proc,
btrans q (In x) q1 /\ (forall y : name, StBisim (p1 y) (q1 y))).
intro.
inversion_clear H6.
cut
(exists q1 : name -> proc,
btrans r (In x) q1 /\ (forall y : name, StBisim (x0 y) (q1 y))).
intro.
inversion_clear H6.
exists x1.
split.
tauto.
intro.
apply TRANS with (x0 y).
generalize y.
case H7; trivial.
generalize y.
case H8; trivial.
apply H.
tauto.
apply H3.
assumption.
intros.
cut
(exists p1 : name -> proc,
btrans q (In x) p1 /\ (forall y : name, StBisim (p1 y) (q1 y))).
intro.
inversion_clear H6.
cut
(exists p1 : name -> proc,
btrans p (In x) p1 /\ (forall y : name, StBisim (p1 y) (x0 y))).
intro.
inversion_clear H6.
exists x1.
split.
tauto.
intro.
apply TRANS with (x0 y).
generalize y.
case H8; trivial.
generalize y.
case H7; trivial.
apply H4.
tauto.
apply H5.
assumption.
elim H1.
intros.
elim H3.
intros.
apply H4.
elim H0.
intros.
elim H2.
intros.
apply H3.
intro.
cut
((forall p1 : name -> proc,
btrans p (bOut x) p1 ->
exists q1 : name -> proc,
btrans q (bOut x) q1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y))) /\
(forall q1 : name -> proc,
btrans q (bOut x) q1 ->
exists p1 : name -> proc,
btrans p (bOut x) p1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y)))).
intro.
cut
((forall p1 : name -> proc,
btrans q (bOut x) p1 ->
exists q1 : name -> proc,
btrans r (bOut x) q1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y))) /\
(forall q1 : name -> proc,
btrans r (bOut x) q1 ->
exists p1 : name -> proc,
btrans q (bOut x) p1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y)))).
intro.
inversion_clear H.
inversion_clear H2.
split.
intros.
cut
(exists q1 : name -> proc,
btrans q (bOut x) q1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y))).
intro.
inversion_clear H6.
cut
(exists q1 : name -> proc,
btrans r (bOut x) q1 /\
(forall y : name,
notin y (nu x0) -> notin y (nu q1) -> StBisim (x0 y) (q1 y))).
intro.
inversion_clear H6.
exists x1.
split.
tauto.
intros.
elim (ho_proc_exp x0 y); intros.
inversion_clear H10.
elim
(unsat
(par (nu p1) (par (nu x0) (par (nu x1) (nu (fun w : name => nu (x2 w))))))
(cons y empty)); intros.
inversion_clear H10.
inversion_clear H13.
inversion_clear H15.
inversion_clear H16.
inversion_clear H14.
clear H18.
apply TRANS with (x2 x3 y).
elim
(unsat (par (nu p1) (par (nu (x2 x3)) (nu x0))) (cons x3 (cons y empty)));
intros.
inversion_clear H14.
inversion_clear H18.
inversion_clear H20.
inversion_clear H19.
inversion_clear H22.
clear H23.
apply L6_Light with x4.
assumption. assumption.
change (StBisim ((fun z : name => p1 x4) x3) ((fun z : name => x2 z x4) x3))
in |- *.
apply L6_Light with y.
apply notin_nu.
intros.
inversion H6.
apply H24.
auto.
apply notin_nu.
intros.
inversion H11.
cut (notin y (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin y (x2 z x4)); [ intro | auto ].
assumption.
inversion_clear H7.
rewrite <- H12; apply H23.
assumption.
assumption.
apply notin_nu.
intros.
inversion H10.
apply H24; auto.
apply notin_nu.
intros.
inversion H17.
cut (notin x3 (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin x3 (x2 z x4)); [ intro | auto ].
assumption.
assumption.
apply notin_nu. intros.
inversion H11.
cut (notin y (nu (x2 x3))); [ intro | auto ].
inversion H25.
cut (notin y (x2 x3 z)); [ intro | auto ].
assumption.
elim
(unsat (par (nu x1) (par (nu (x2 x3)) (nu x0))) (cons x3 (cons y empty)));
intros.
inversion_clear H14.
inversion_clear H18.
inversion_clear H20.
inversion_clear H19.
inversion_clear H22.
clear H23.
apply L6_Light with x4.
assumption. assumption.
change (StBisim ((fun z : name => x2 z x4) x3) ((fun z : name => x1 x4) x3))
in |- *.
apply L6_Light with y.
apply notin_nu.
intros.
inversion H11.
cut (notin y (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin y (x2 z x4)); [ intro | auto ].
assumption.
apply notin_nu.
intros.
inversion H9.
apply H24.
auto.
inversion_clear H8.
rewrite <- H12; apply H23.
assumption.
assumption.
apply notin_nu.
intros.
inversion H17.
cut (notin x3 (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin x3 (x2 z x4)); [ intro | auto ].
assumption.
apply notin_nu.
intros.
inversion H15.
apply H24; auto.
apply notin_nu. intros.
inversion H11.
cut (notin y (nu (x2 x3))); [ intro | auto ].
inversion H25.
cut (notin y (x2 x3 z)); [ intro | auto ].
assumption.
assumption.
apply H. tauto.
apply H3. tauto.
intros.
cut
(exists p1 : name -> proc,
btrans q (bOut x) p1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu q1) -> StBisim (p1 y) (q1 y))).
intro.
inversion_clear H6.
cut
(exists p1 : name -> proc,
btrans p (bOut x) p1 /\
(forall y : name,
notin y (nu p1) -> notin y (nu x0) -> StBisim (p1 y) (x0 y))).
intro.
inversion_clear H6.
exists x1.
split.
tauto.
intros.
elim (ho_proc_exp x0 y); intros.
inversion_clear H10.
elim
(unsat
(par (nu x1) (par (nu x0) (par (nu q1) (nu (fun w : name => nu (x2 w))))))
(cons y empty)); intros.
inversion_clear H10.
inversion_clear H13.
inversion_clear H15.
inversion_clear H16.
inversion_clear H14.
clear H18.
apply TRANS with (x2 x3 y).
elim
(unsat (par (nu x1) (par (nu (x2 x3)) (nu x0))) (cons x3 (cons y empty)));
intros.
inversion_clear H14.
inversion_clear H18.
inversion_clear H20.
inversion_clear H19.
inversion_clear H22.
clear H23.
apply L6_Light with x4.
assumption. assumption.
change (StBisim ((fun z : name => x1 x4) x3) ((fun z : name => x2 z x4) x3))
in |- *.
apply L6_Light with y.
apply notin_nu.
intros.
inversion H6.
apply H24.
auto.
apply notin_nu.
intros.
inversion H11.
cut (notin y (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin y (x2 z x4)); [ intro | auto ].
assumption.
inversion_clear H8.
rewrite <- H12; apply H23.
assumption.
assumption.
apply notin_nu.
intros.
inversion H10.
apply H24; auto.
apply notin_nu.
intros.
inversion H17.
cut (notin x3 (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin x3 (x2 z x4)); [ intro | auto ].
assumption.
assumption.
apply notin_nu. intros.
inversion H11.
cut (notin y (nu (x2 x3))); [ intro | auto ].
inversion H25.
cut (notin y (x2 x3 z)); [ intro | auto ].
assumption.
elim
(unsat (par (nu q1) (par (nu (x2 x3)) (nu x0))) (cons x3 (cons y empty)));
intros.
inversion_clear H14.
inversion_clear H18.
inversion_clear H20.
inversion_clear H19.
inversion_clear H22.
clear H23.
apply L6_Light with x4.
assumption. assumption.
change (StBisim ((fun z : name => x2 z x4) x3) ((fun z : name => q1 x4) x3))
in |- *.
apply L6_Light with y.
apply notin_nu.
intros.
inversion H11.
cut (notin y (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin y (x2 z x4)); [ intro | auto ].
assumption.
apply notin_nu.
intros.
inversion H9.
apply H24.
auto.
inversion_clear H7.
rewrite <- H12; apply H23.
assumption.
assumption.
apply notin_nu.
intros.
inversion H17.
cut (notin x3 (nu (x2 z))); [ intro | auto ].
inversion H25.
cut (notin x3 (x2 z x4)); [ intro | auto ].
assumption.
apply notin_nu.
intros.
inversion H15.
apply H24; auto.
apply notin_nu. intros.
inversion H11.
cut (notin y (nu (x2 x3))); [ intro | auto ].
inversion H25.
cut (notin y (x2 x3 z)); [ intro | auto ].
assumption.
assumption.
apply H4. tauto.
apply H5. tauto.
elim H1.
intros.
elim H3.
intros.
apply H5.
elim H0.
intros.
elim H2.
intros.
apply H4.
Qed.
Lemma TAU_S :
forall p q : proc, StBisim p q -> StBisim (tau_pref p) (tau_pref q).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion H0; exists q; split; [ apply TAU | rewrite <- H3 ]; assumption.
inversion H0; exists p; split; [ apply TAU | rewrite <- H3 ]; assumption.
inversion_clear H0.
inversion_clear H0.
inversion_clear H0.
inversion_clear H0.
Qed.
Lemma SUM_S : forall p q r : proc, StBisim p q -> StBisim (sum p r) (sum q r).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion H0.
inversion H.
inversion_clear H6.
elim (H9 a); intros.
elim (H6 p1 H5); intros.
exists x; split; [ apply fSUM1; tauto | tauto ].
exists p1; split; [ apply fSUM2; tauto | apply REF ].
inversion H0.
inversion H.
inversion_clear H6.
elim (H9 a); intros.
elim (H11 q1 H5); intros.
exists x; split; [ apply fSUM1; tauto | tauto ].
exists q1; split; [ apply fSUM2; tauto | apply REF ].
inversion H0.
inversion H.
inversion_clear H6.
inversion_clear H10.
elim (H6 x); intros.
elim (H10 p1 H5); intros.
exists x0; split; [ apply bSUM1; tauto | intuition ].
exists p1; split; [ apply bSUM2; tauto | intro; apply REF ].
inversion H0.
inversion H.
inversion_clear H6.
inversion_clear H10.
elim (H6 x); intros.
elim (H12 q1 H5); intros.
exists x0; split; [ apply bSUM1; tauto | intuition ].
exists q1; split; [ apply bSUM2; tauto | intro; apply REF ].
inversion H0.
inversion H.
inversion_clear H6.
inversion_clear H10.
elim (H11 x); intros.
elim (H10 p1 H5); intros.
exists x0; split; [ apply bSUM1; tauto | intuition ].
exists p1; split; [ apply bSUM2; tauto | intros; apply REF ].
inversion H0.
inversion H.
inversion_clear H6.
inversion_clear H10.
elim (H11 x); intros.
elim (H12 q1 H5); intros.
exists x0; split; [ apply bSUM1; tauto | intuition ].
exists q1; split; [ apply bSUM2; tauto | intros; apply REF ].
Qed.
Lemma NU_S :
forall p q : name -> proc,
(forall x : name, notin x (nu p) -> notin x (nu q) -> StBisim (p x) (q x)) ->
StBisim (nu p) (nu q).
Proof.
cofix; intros; apply sb; do 3 try (split; intros).
inversion H0.
generalize H2.
generalize H0.
elim a.
intros.
elim (unsat (par (nu p) (par (nu q) (nu p2))) l); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
cut (StBisim (p x) (q x)); [ intro | auto ].
inversion_clear H10.
inversion_clear H12.
elim (H10 tau); intros.
cut (ftrans (p x) tau (p2 x)); [ intro | apply H6; auto ].
elim (H12 (p2 x) H15); intros.
inversion_clear H16.
elim (proc_exp x0 x); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (nu x1); split.
apply fRES with empty; intros; auto.
clear H22 H23.
change (ftrans (q y) ((fun _ : name => tau) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
apply NU_S; intros.
apply L6_Light with x; auto.
apply f_act_notin_tau.
intros.
elim (unsat (par (nu p) (par (nu q) (nu p2))) (cons n (cons n0 l))); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
inversion_clear H9.
inversion_clear H12.
cut (StBisim (p x) (q x)); [ intro | auto ].
inversion_clear H12.
inversion_clear H14.
elim (H12 (Out n n0)); intros.
cut (ftrans (p x) (Out n n0) (p2 x)); [ intro | apply H6; auto ].
elim (H14 (p2 x) H17); intros.
inversion_clear H18.
elim (proc_exp x0 x); intros.
inversion_clear H18.
rewrite H22 in H19.
rewrite H22 in H20.
exists (nu x1); split.
apply fRES with empty; intros; auto.
change (ftrans (q y) ((fun _ : name => Out n n0) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
clear H24.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H25.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
apply NU_S; intros.
apply L6_Light with x; auto.
apply f_act_notin_Out; auto.
inversion H0.
generalize H2.
generalize H0.
elim a.
intros.
elim (unsat (par (nu p) (par (nu q) (nu p2))) l); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
cut (StBisim (p x) (q x)); [ intro | auto ].
inversion_clear H10.
inversion_clear H12.
elim (H10 tau); intros.
cut (ftrans (q x) tau (p2 x)); [ intro | apply H6; auto ].
elim (H14 (p2 x) H15); intros.
inversion_clear H16.
elim (proc_exp x0 x); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (nu x1); split.
apply fRES with empty; intros; auto.
change (ftrans (p y) ((fun _ : name => tau) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
apply NU_S; intros.
apply L6_Light with x; auto.
apply f_act_notin_tau.
intros.
elim (unsat (par (nu p) (par (nu q) (nu p2))) (cons n (cons n0 l))); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
inversion_clear H9.
inversion_clear H12.
cut (StBisim (p x) (q x)); [ intro | auto ].
inversion_clear H12.
inversion_clear H14.
elim (H12 (Out n n0)); intros.
cut (ftrans (q x) (Out n n0) (p2 x)); [ intro | apply H6; auto ].
elim (H16 (p2 x) H17); intros.
inversion_clear H18.
elim (proc_exp x0 x); intros.
inversion_clear H18.
rewrite H22 in H19.
rewrite H22 in H20.
exists (nu x1); split.
apply fRES with empty; intros; auto.
clear H24.
change (ftrans (p y) ((fun _ : name => Out n n0) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H25.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
apply NU_S; intros.
apply L6_Light with x; auto.
apply f_act_notin_Out; auto.
inversion H0.
elim
(unsat (par (nu p) (par (nu q) (nu (fun z : name => nu (p2 z))))) (cons x l));
intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x0) (q x0)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
inversion_clear H12.
elim (H11 x); intros.
cut (btrans (p x0) (In x) (p2 x0)); [ intro | apply H2; auto ].
elim (H12 (p2 x0) H15); intros.
inversion_clear H16.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (fun n : name => nu (fun z : name => x2 z n)); split.
apply bRES with empty; intros; auto.
clear H23.
inversion_clear H22.
change (btrans (q y) ((fun _ : name => In x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In.
assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In.
assumption.
intro.
apply NU_S; intros.
elim (LEM_name x0 x3); intros.
rewrite <- H22; auto.
elim (LEM_name x0 y); intros.
rewrite <- H23; auto.
rewrite <- H23 in H16.
rewrite <- H23 in H21.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x3 empty))); intros.
inversion_clear H24.
inversion_clear H25.
inversion_clear H26.
inversion_clear H28.
clear H29.
change
(StBisim ((fun n : name => p2 n x0) x3) ((fun n : name => x2 n x0) x3))
in |- *.
apply L6_Light with x4; auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x4 empty))); intros.
inversion_clear H28.
inversion_clear H29.
inversion_clear H30.
inversion_clear H32.
clear H33.
apply L6_Light with x5; auto.
apply notin_nu; intros.
inversion_clear H28.
cut (notin x5 (nu (p2 x4))); [ intro | auto ].
inversion_clear H28.
auto.
apply notin_nu; intros.
inversion_clear H31.
cut (notin x5 (nu (x2 x4))); [ intro | auto ].
inversion_clear H31.
auto.
change
(StBisim ((fun n : name => p2 n x5) x4) ((fun n : name => x2 n x5) x4))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 x4))); [ intro | auto ].
inversion_clear H9.
auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 x4))); [ intro | auto ].
inversion_clear H19.
auto.
change (StBisim ((fun n : name => p2 n y) x3) ((fun n : name => x2 n y) x3))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply b_act_notin_In; auto.
inversion H0.
elim
(unsat (par (nu p) (par (nu q) (nu (fun z : name => nu (p2 z))))) (cons x l));
intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x0) (q x0)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
inversion_clear H12.
elim (H11 x); intros.
cut (btrans (q x0) (In x) (p2 x0)); [ intro | apply H2; auto ].
elim (H14 (p2 x0) H15); intros.
inversion_clear H16.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (fun n : name => nu (fun z : name => x2 z n)); split.
apply bRES with empty; intros; auto.
clear H23.
inversion_clear H22.
change (btrans (p y) ((fun _ : name => In x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In.
assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In.
assumption.
intro.
apply NU_S; intros.
elim (LEM_name x0 x3); intros.
rewrite <- H22; auto.
elim (LEM_name x0 y); intros.
rewrite <- H23; auto.
rewrite <- H23 in H16.
rewrite <- H23 in H21.
elim
(unsat
(par (nu (fun z : name => nu (x2 z))) (nu (fun z : name => nu (p2 z))))
(cons x0 (cons x3 l))); intros.
inversion_clear H24.
inversion_clear H25.
inversion_clear H26.
inversion_clear H28.
change
(StBisim ((fun n : name => x2 n x0) x3) ((fun n : name => p2 n x0) x3))
in |- *.
apply L6_Light with x4; auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H27.
auto.
elim
(unsat
(par (nu (fun z : name => nu (x2 z))) (nu (fun z : name => nu (p2 z))))
(cons x0 (cons x4 l))); intros.
inversion_clear H28.
inversion_clear H30.
inversion_clear H31.
inversion_clear H33.
apply L6_Light with x5; auto.
apply notin_nu; intros.
inversion_clear H28.
cut (notin x5 (nu (x2 x4))); [ intro | auto ].
inversion_clear H28.
auto.
apply notin_nu; intros.
inversion_clear H32.
cut (notin x5 (nu (p2 x4))); [ intro | auto ].
inversion_clear H32.
auto.
change
(StBisim ((fun n : name => x2 n x5) x4) ((fun n : name => p2 n x5) x4))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H27.
auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 x4))); [ intro | auto ].
inversion_clear H19.
auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 x4))); [ intro | auto ].
inversion_clear H9.
auto.
change (StBisim ((fun n : name => x2 n y) x3) ((fun n : name => p2 n y) x3))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply b_act_notin_In; auto.
inversion H0.
elim
(unsat (par (nu p) (par (nu q) (nu (fun z : name => nu (p2 z))))) (cons x l));
intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x0) (q x0)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
inversion_clear H12.
elim (H13 x); intros.
cut (btrans (p x0) (bOut x) (p2 x0)); [ intro | apply H2; auto ].
elim (H12 (p2 x0) H15); intros.
inversion_clear H16.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (fun n : name => nu (fun z : name => x2 z n)); split.
apply bRES with empty; intros; auto.
clear H23.
inversion_clear H22.
change (btrans (q y) ((fun _ : name => bOut x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut.
assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut.
assumption.
intros.
apply NU_S; intros.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x3 (cons y l)))); intros.
inversion_clear H24.
inversion_clear H25.
inversion_clear H26.
inversion_clear H28.
inversion_clear H29.
change (StBisim ((fun n : name => p2 n y) x3) ((fun n : name => x2 n y) x3))
in |- *.
apply L6_Light with x4; auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x4 (cons y l)))); intros.
inversion_clear H29.
inversion_clear H31.
inversion_clear H32.
inversion_clear H34.
inversion_clear H35.
apply L6_Light with x5; auto.
apply notin_nu; intros.
inversion_clear H29.
cut (notin x5 (nu (p2 x4))); [ intro | auto ].
inversion_clear H29.
auto.
apply notin_nu; intros.
inversion_clear H33.
cut (notin x5 (nu (x2 x4))); [ intro | auto ].
inversion_clear H33.
auto.
change
(StBisim ((fun n : name => p2 n x5) x4) ((fun n : name => x2 n x5) x4))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply H18.
apply notin_nu; intros.
inversion_clear H29.
cut (notin x5 (nu (p2 x0))); [ intro | auto ].
inversion_clear H29.
auto.
apply notin_nu; intros.
inversion_clear H33.
cut (notin x5 (nu (x2 x0))); [ intro | auto ].
inversion_clear H33.
auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
apply notin_nu; intros.
inversion_clear H16.
cut (notin y (nu (fun z0 : name => p2 z0 z))); [ intro | auto ].
inversion_clear H16.
auto.
apply notin_nu; intros.
inversion_clear H21.
cut (notin y (nu (fun z0 : name => x2 z0 z))); [ intro | auto ].
inversion_clear H21.
auto.
apply b_act_notin_bOut; assumption.
elim (unsat (par (nu p) (par (nu q) (nu p1))) (cons x l)); intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x1) (q x1)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
elim (H7 (Out x x1)); intros.
cut (ftrans (p x1) (Out x x1) (p1 x1)); [ intro | apply H3; auto ].
elim (H11 (p1 x1) H14); intros.
inversion_clear H15.
elim (proc_exp x2 x1); intros.
inversion_clear H15.
rewrite H19 in H16.
rewrite H19 in H17.
exists x3; split.
apply OPEN with empty; intros; auto.
clear H22.
change (ftrans (q y) ((fun n : name => Out x n) y) (x3 y)) in |- *;
apply FTR_L3 with x1; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out.
assumption.
assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out.
auto.
assumption.
intros.
apply L6_Light with x1; auto.
inversion H0.
elim
(unsat (par (nu p) (par (nu q) (nu (fun z : name => nu (p2 z))))) (cons x l));
intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x0) (q x0)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
inversion_clear H12.
elim (H13 x); intros.
cut (btrans (q x0) (bOut x) (p2 x0)); [ intro | apply H2; auto ].
elim (H14 (p2 x0) H15); intros.
inversion_clear H16.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H16.
rewrite H20 in H17.
rewrite H20 in H18.
exists (fun n : name => nu (fun z : name => x2 z n)); split.
apply bRES with empty; intros; auto.
clear H23.
inversion_clear H22.
change (btrans (p y) ((fun _ : name => bOut x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut.
assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut.
assumption.
intros.
apply NU_S; intros.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x3 (cons y l)))); intros.
inversion_clear H24.
inversion_clear H25.
inversion_clear H26.
inversion_clear H28.
inversion_clear H29.
change (StBisim ((fun n : name => x2 n y) x3) ((fun n : name => p2 n y) x3))
in |- *.
apply L6_Light with x4; auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
elim
(unsat
(par (nu (fun z : name => nu (p2 z))) (nu (fun z : name => nu (x2 z))))
(cons x0 (cons x4 (cons y l)))); intros.
inversion_clear H29.
inversion_clear H31.
inversion_clear H32.
inversion_clear H34.
inversion_clear H35.
apply L6_Light with x5; auto.
apply notin_nu; intros.
inversion_clear H33.
cut (notin x5 (nu (x2 x4))); [ intro | auto ].
inversion_clear H33.
auto.
apply notin_nu; intros.
inversion_clear H29.
cut (notin x5 (nu (p2 x4))); [ intro | auto ].
inversion_clear H29.
auto.
change
(StBisim ((fun n : name => x2 n x5) x4) ((fun n : name => p2 n x5) x4))
in |- *.
apply L6_Light with x0; auto.
apply notin_nu; intros.
inversion_clear H19.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H19.
auto.
apply notin_nu; intros.
inversion_clear H9.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H9.
auto.
apply H18.
apply notin_nu; intros.
inversion_clear H33.
cut (notin x5 (nu (x2 x0))); [ intro | auto ].
inversion_clear H33.
auto.
apply notin_nu; intros.
inversion_clear H29.
cut (notin x5 (nu (p2 x0))); [ intro | auto ].
inversion_clear H29.
auto.
apply notin_nu; intros.
inversion_clear H27.
cut (notin x4 (nu (x2 z))); [ intro | auto ].
inversion_clear H27.
auto.
apply notin_nu; intros.
inversion_clear H24.
cut (notin x4 (nu (p2 z))); [ intro | auto ].
inversion_clear H24.
auto.
apply notin_nu; intros.
inversion_clear H16.
cut (notin y (nu (fun z0 : name => x2 z0 z))); [ intro | auto ].
inversion_clear H16.
auto.
apply notin_nu; intros.
inversion_clear H21.
cut (notin y (nu (fun z0 : name => p2 z0 z))); [ intro | auto ].
inversion_clear H21.
auto.
apply b_act_notin_bOut; assumption.
elim (unsat (par (nu p) (par (nu q) (nu q1))) (cons x l)); intros.
inversion_clear H5.
inversion_clear H6.
inversion_clear H8.
inversion_clear H7.
cut (StBisim (p x1) (q x1)); [ intro | auto ].
inversion_clear H7.
inversion_clear H11.
elim (H7 (Out x x1)); intros.
cut (ftrans (q x1) (Out x x1) (q1 x1)); [ intro | apply H3; auto ].
elim (H13 (q1 x1) H14); intros.
inversion_clear H15.
elim (proc_exp x2 x1); intros.
inversion_clear H15.
rewrite H19 in H16.
rewrite H19 in H17.
exists x3; split.
apply OPEN with empty; intros; auto.
clear H22.
change (ftrans (p y) ((fun n : name => Out x n) y) (x3 y)) in |- *;
apply FTR_L3 with x1; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out.
assumption.
assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out.
auto.
assumption.
intros.
apply L6_Light with x1; auto.
Qed.
Inductive BisPAR_S : proc -> proc -> Prop :=
bispar_s :
forall p q : proc,
StBisim p q -> forall r : proc, BisPAR_S (par p r) (par q r).
Inductive Op_PAR_S (R : proc -> proc -> Prop) : proc -> proc -> Prop :=
op_par_s :
forall p q : name -> proc,
(forall z : name, notin z (nu p) -> notin z (nu q) -> R (p z) (q z)) ->
Op_PAR_S R (nu p) (nu q).
Fixpoint PAR_S_fun (n : nat) : proc -> proc -> Prop :=
match n with
| O => BisPAR_S
| S m => Op_PAR_S (PAR_S_fun m)
end.
Inductive SBPAR_S (p q : proc) : Prop :=
sbpar_s : forall n : nat, PAR_S_fun n p q -> SBPAR_S p q.
Lemma PAR_S_RW :
forall (n : nat) (p q : name -> proc) (x : name),
notin x (nu p) ->
notin x (nu q) ->
PAR_S_fun n (p x) (q x) ->
forall y : name, notin y (nu p) -> notin y (nu q) -> PAR_S_fun n (p y) (q y).
Proof.
intros; elim (LEM_name x y); intro.
rewrite <- H4; assumption.
generalize p q x H H0 y H4 H2 H3 H1; clear H H0 H2 H3 H4 y H1 x p q;
induction n as [| n Hrecn]; intros.
simpl in H1; inversion H1; simpl in |- *.
elim (proc_exp p0 x); elim (proc_exp q0 x); elim (proc_exp r x); intros.
inversion_clear H8; inversion_clear H9; inversion_clear H10.
rewrite H14 in H5; rewrite H13 in H6; rewrite H12 in H5; rewrite H12 in H6;
cut (p = (fun n : name => par (x2 n) (x0 n)));
[ intro | apply proc_ext with x; auto ].
cut (q = (fun n : name => par (x1 n) (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H10; rewrite H15; apply bispar_s.
rewrite H10 in H1; rewrite H15 in H1; inversion_clear H1.
apply L6 with x; auto.
rewrite H10 in H2; inversion_clear H2; apply notin_nu; intros.
cut (notin y (par (x2 z) (x0 z))); [ intro | auto ].
inversion_clear H17; assumption.
rewrite H15 in H3; inversion_clear H3; apply notin_nu; intros.
cut (notin y (par (x1 z) (x0 z))); [ intro | auto ].
inversion_clear H17; assumption.
inversion_clear H8; inversion_clear H11; apply notin_nu; intros;
apply notin_par; auto.
inversion_clear H9; inversion_clear H11; apply notin_nu; intros;
apply notin_par; auto.
simpl in H1; inversion H1; simpl in |- *.
elim (ho_proc_exp p0 x); elim (ho_proc_exp q0 x); intros.
inversion_clear H8; inversion_clear H9.
rewrite H12 in H5; rewrite H11 in H6.
cut (p = (fun n : name => nu (x1 n)));
[ intro | apply proc_ext with x; auto ].
cut (q = (fun n : name => nu (x0 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H9; rewrite H13; apply op_par_s; intros.
elim
(unsat
(par (nu p)
(par (nu q)
(par (nu (fun n : name => nu (x0 n)))
(nu (fun n : name => nu (x1 n))))))
(cons x (cons y (cons z empty)))); intros.
inversion_clear H16.
inversion_clear H17; inversion_clear H18.
inversion_clear H19; inversion_clear H20.
inversion_clear H21; inversion_clear H22.
clear H24.
apply Hrecn with x2; auto.
inversion_clear H23; auto.
inversion_clear H20; auto.
change
(PAR_S_fun n ((fun n : name => x1 n x2) y) ((fun n : name => x0 n x2) y))
in |- *; apply Hrecn with x; auto.
inversion_clear H8; apply notin_nu; intros.
cut (notin x (nu (x1 z0))); [ intro | auto ].
inversion_clear H24; auto.
inversion_clear H10; apply notin_nu; intros.
cut (notin x (nu (x0 z0))); [ intro | auto ].
inversion_clear H24; auto.
apply proc_mono with x; inversion_clear H2.
cut (notin y (p x)); [ rewrite <- H5; intro | auto ].
inversion_clear H2; auto.
apply proc_mono with x; inversion_clear H3.
cut (notin y (q x)); [ rewrite <- H6; intro | auto ].
inversion_clear H3; auto.
rewrite <- H11; rewrite <- H12; apply H7; auto.
inversion_clear H23.
cut (notin x2 (nu (x1 x))); [ intro | auto ]; rewrite H12; assumption.
inversion_clear H20.
cut (notin x2 (nu (x0 x))); [ intro | auto ]; rewrite H11; assumption.
Qed.
Lemma SBPAR_S_TO_SB' : Inclus SBPAR_S (Op_StBisim SBPAR_S).
Proof.
unfold Inclus in |- *; intros.
inversion_clear H.
cut (PAR_S_fun n p1 p2);
[ generalize p1 p2; generalize n; simple induction n0; intros | assumption ].
simpl in H; inversion H.
inversion_clear H1.
inversion_clear H4.
inversion_clear H5.
apply op_sb; split; intros.
elim a; intros; split; intros.
inversion_clear H5.
elim (H1 tau); intros.
elim (H5 p7 H7); intros.
inversion_clear H9.
exists (par x r); split; [ apply fPAR1; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
exists (par q p7); split; [ apply fPAR2; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; rewrite <- H2 in H;
rewrite <- H3 in H; inversion_clear H; assumption.
elim (H4 x); intros.
elim (H5 q1 H7); intros.
inversion_clear H10.
exists (par (x0 y) q2); split; [ apply COM1 with x; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; auto.
elim (H1 (Out x y)); intros.
elim (H5 q1 H7); intros.
inversion_clear H10.
exists (par x0 (q2 y)); split; [ apply COM2 with x; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
elim (H4 x); intros.
elim (H5 q1 H7); intros.
inversion_clear H10.
exists (nu (fun n : name => par (x0 n) (q2 n))); split;
[ apply CLOSE1 with x; assumption | idtac ].
apply sbpar_s with 1; simpl in |- *; apply op_par_s; intros; apply bispar_s;
auto.
elim (H6 x); intros.
elim (H5 q1 H7); intros.
inversion_clear H10.
exists (nu (fun n : name => par (x0 n) (q2 n))); split;
[ apply CLOSE2 with x; assumption | idtac ].
apply sbpar_s with 1; simpl in |- *; apply op_par_s; intros; apply bispar_s;
apply H12; auto.
inversion_clear H10; apply notin_nu; intros.
cut (notin z (par (q1 z0) (q2 z0))); [ intro | auto ].
inversion_clear H15; assumption.
inversion_clear H13; apply notin_nu; intros.
cut (notin z (par (x0 z0) (q2 z0))); [ intro | auto ].
inversion_clear H15; assumption.
inversion_clear H5.
elim (H1 tau); intros.
elim (H8 p6 H7); intros.
inversion_clear H9.
exists (par x r); split; [ apply fPAR1; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
exists (par p p6); split; [ apply fPAR2; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; rewrite <- H2 in H;
rewrite <- H3 in H; inversion_clear H; assumption.
elim (H4 x); intros.
elim (H9 q0 H7); intros.
inversion_clear H10.
exists (par (x0 y) q2); split; [ apply COM1 with x; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; auto.
elim (H1 (Out x y)); intros.
elim (H9 q0 H7); intros.
inversion_clear H10.
exists (par x0 (q2 y)); split; [ apply COM2 with x; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
elim (H4 x); intros.
elim (H9 q0 H7); intros.
inversion_clear H10.
exists (nu (fun n : name => par (x0 n) (q2 n))); split;
[ apply CLOSE1 with x; assumption | idtac ].
apply sbpar_s with 1; simpl in |- *; apply op_par_s; intros; apply bispar_s;
auto.
elim (H6 x); intros.
elim (H9 q0 H7); intros.
inversion_clear H10.
exists (nu (fun n : name => par (x0 n) (q2 n))); split;
[ apply CLOSE2 with x; assumption | idtac ].
apply sbpar_s with 1; simpl in |- *; apply op_par_s; intros; apply bispar_s;
apply H12; auto.
inversion_clear H10; apply notin_nu; intros.
cut (notin z (par (x0 z0) (q2 z0))); [ intro | auto ].
inversion_clear H15; assumption.
inversion_clear H13; apply notin_nu; intros.
cut (notin z (par (q0 z0) (q2 z0))); [ intro | auto ].
inversion_clear H15; assumption.
inversion_clear H5.
elim (H1 (Out n1 n2)); intros.
elim (H5 p7 H7); intros.
inversion_clear H9.
exists (par x r); split; [ apply fPAR1; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
exists (par q p7); split; [ apply fPAR2; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; rewrite <- H2 in H;
rewrite <- H3 in H; inversion_clear H; assumption.
inversion_clear H5.
elim (H1 (Out n1 n2)); intros.
elim (H8 p6 H7); intros.
inversion_clear H9.
exists (par x r); split; [ apply fPAR1; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption.
exists (par p p6); split; [ apply fPAR2; assumption | idtac ].
apply sbpar_s with 0; simpl in |- *; apply bispar_s; rewrite <- H2 in H;
rewrite <- H3 in H; inversion_clear H; assumption.
split; intros.
elim (H4 x); intros; split; intros.
inversion_clear H8.
elim (H5 p7 H9); intros.
inversion_clear H8.
exists (fun n : name => par (x0 n) r); split;
[ apply bPAR1; assumption | idtac ].
intro; apply sbpar_s with 0; simpl in |- *; apply bispar_s; auto.
exists (fun n : name => par q (p7 n)); split;
[ apply bPAR2; assumption | idtac ].
intro; apply sbpar_s with 0; simpl in |- *; apply bispar_s;
rewrite <- H2 in H; rewrite <- H3 in H; inversion_clear H;
assumption.
inversion_clear H8.
elim (H7 p6 H9); intros.
inversion_clear H8.
exists (fun n : name => par (x0 n) r); split;
[ apply bPAR1; assumption | idtac ].
intro; apply sbpar_s with 0; simpl in |- *; apply bispar_s; auto.
exists (fun n : name => par p (p6 n)); split;
[ apply bPAR2; assumption | idtac ].
intro; apply sbpar_s with 0; simpl in |- *; apply bispar_s;
rewrite <- H2 in H; rewrite <- H3 in H; inversion_clear H;
assumption.
elim (H6 x); intros; split; intros.
inversion_clear H8.
elim (H5 p7 H9); intros.
inversion_clear H8.
exists (fun n : name => par (x0 n) r); split;
[ apply bPAR1; assumption | idtac ].
intros; apply sbpar_s with 0; simpl in |- *; apply bispar_s; apply H11; auto.
inversion_clear H8; apply notin_nu; intros.
cut (notin y (par (p7 z) r)); [ intro | auto ].
inversion_clear H14; assumption.
inversion_clear H12; apply notin_nu; intros.
cut (notin y (par (x0 z) r)); [ intro | auto ].
inversion_clear H14; assumption.
exists (fun n : name => par q (p7 n)); split;
[ apply bPAR2; assumption | idtac ].
intros; apply sbpar_s with 0; simpl in |- *; apply bispar_s;
rewrite <- H2 in H; rewrite <- H3 in H; inversion_clear H;
assumption.
inversion_clear H8.
elim (H7 p6 H9); intros.
inversion_clear H8.
exists (fun n : name => par (x0 n) r); split;
[ apply bPAR1; assumption | idtac ].
intros; apply sbpar_s with 0; simpl in |- *; apply bispar_s; apply H11; auto.
inversion_clear H8; apply notin_nu; intros.
cut (notin y (par (x0 z) r)); [ intro | auto ].
inversion_clear H14; assumption.
inversion_clear H12; apply notin_nu; intros.
cut (notin y (par (p6 z) r)); [ intro | auto ].
inversion_clear H14; assumption.
exists (fun n : name => par p (p6 n)); split;
[ apply bPAR2; assumption | idtac ].
intros; apply sbpar_s with 0; simpl in |- *; apply bispar_s;
rewrite <- H2 in H; rewrite <- H3 in H; inversion_clear H;
assumption.
simpl in H1; inversion H1.
apply op_sb; split; intros.
elim a; intros; split; intros.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu p6))) l); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
cut (ftrans (p x) tau (p6 x)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x) (q x)); [ intro | apply H5; auto ].
inversion_clear H12.
inversion_clear H13.
elim (H12 tau); intros.
elim (H13 (p6 x) H10); intros.
inversion_clear H16.
elim (proc_exp x0 x); intros.
inversion_clear H16.
rewrite H20 in H17; rewrite H20 in H18.
exists (nu x1); split; [ apply fRES with l; intros | idtac ].
change (ftrans (q y) ((fun _ : name => tau) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
inversion_clear H18.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
apply PAR_S_RW with x; auto.
apply f_act_notin_tau.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu p5))) l); intros.
inversion_clear H7.
inversion_clear H8.
inversion_clear H10.
cut (ftrans (q x) tau (p5 x)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x) (q x)); [ intro | apply H5; auto ].
inversion_clear H12.
inversion_clear H13.
elim (H12 tau); intros.
elim (H15 (p5 x) H10); intros.
inversion_clear H16.
elim (proc_exp x0 x); intros.
inversion_clear H16.
rewrite H20 in H17; rewrite H20 in H18.
exists (nu x1); split; [ apply fRES with l; intros | idtac ].
change (ftrans (p y) ((fun _ : name => tau) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
inversion_clear H18.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
apply PAR_S_RW with x; auto.
apply f_act_notin_tau.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu p6))) (cons n2 (cons n3 l))); intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (ftrans (p x) (Out n2 n3) (p6 x)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x) (q x)); [ intro | apply H5; auto ].
inversion_clear H14.
inversion_clear H15.
elim (H14 (Out n2 n3)); intros.
elim (H15 (p6 x) H11); intros.
inversion_clear H18.
elim (proc_exp x0 x); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (nu x1); split; [ apply fRES with l; intros | idtac ].
inversion_clear H25.
change (ftrans (q y) ((fun _ : name => Out n2 n3) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H20.
apply sbpar_s with (S n4); simpl in |- *; apply op_par_s; intros.
apply PAR_S_RW with x; auto.
apply f_act_notin_Out; auto.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu p5))) (cons n2 (cons n3 l))); intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (ftrans (q x) (Out n2 n3) (p5 x)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x) (q x)); [ intro | apply H5; auto ].
inversion_clear H14.
inversion_clear H15.
elim (H14 (Out n2 n3)); intros.
elim (H17 (p5 x) H11); intros.
inversion_clear H18.
elim (proc_exp x0 x); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (nu x1); split; [ apply fRES with l; intros | idtac ].
inversion_clear H25.
change (ftrans (p y) ((fun _ : name => Out n2 n3) y) (x1 y)) in |- *;
apply FTR_L3 with x; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H20.
apply sbpar_s with (S n4); simpl in |- *; apply op_par_s; intros.
apply PAR_S_RW with x; auto.
apply f_act_notin_Out; auto.
split; intros.
split; intros.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim
(unsat (par (nu p) (par (nu q) (nu (fun n : name => nu (p6 n))))) (cons x l));
intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (btrans (p x0) (In x) (p6 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
inversion_clear H15.
elim (H14 x); intros.
elim (H15 (p6 x0) H10); intros.
inversion_clear H18.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (fun n : name => nu (fun u : name => x2 u n)); split;
[ apply bRES with l; intros | idtac ].
inversion_clear H24;
change (btrans (q y) ((fun _ : name => In x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
intro; elim (LEM_name x0 y); intro.
rewrite <- H18;
elim
(unsat
(par (nu (fun n : name => nu (p6 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 empty)); intros.
inversion_clear H23.
inversion_clear H24; inversion_clear H25.
clear H27; cut (SBPAR_S (p6 x0 x3) (x2 x0 x3)); [ intro | auto ].
inversion_clear H25.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
elim
(unsat
(par (nu (fun n : name => nu (p6 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 (cons x3 (cons z empty)))); intros.
inversion_clear H29.
inversion_clear H30; inversion_clear H31.
inversion_clear H33.
inversion_clear H34.
clear H35.
cut (PAR_S_fun n2 (p6 x4 x3) (x2 x4 x3));
[ intro
| change
(PAR_S_fun n2 ((fun n : name => p6 n x3) x4)
((fun n : name => x2 n x3) x4)) in |- *; apply PAR_S_RW with x0;
auto ].
change
(PAR_S_fun n2 ((fun n : name => p6 n x0) z) ((fun n : name => x2 n x0) z))
in |- *; apply PAR_S_RW with x4; auto.
inversion_clear H29; apply notin_nu; intros.
cut (notin x4 (nu (p6 z0))); [ intro | auto ].
inversion_clear H36; auto.
inversion_clear H32; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H36; auto.
apply PAR_S_RW with x3; auto.
inversion_clear H23; auto.
inversion_clear H26; auto.
inversion_clear H12; auto.
inversion_clear H21; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p6 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H29; apply notin_nu; intros.
cut (notin x4 (nu (p6 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H32; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H35; auto.
cut (SBPAR_S (p6 x0 y) (x2 x0 y)); [ intro | auto ].
inversion_clear H23.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
change
(PAR_S_fun n2 ((fun n : name => p6 n y) z) ((fun n : name => x2 n y) z))
in |- *; apply PAR_S_RW with x0; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p6 z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H27; auto.
apply b_act_notin_In; auto.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim
(unsat (par (nu p) (par (nu q) (nu (fun n : name => nu (p5 n))))) (cons x l));
intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (btrans (q x0) (In x) (p5 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
inversion_clear H15.
elim (H14 x); intros.
elim (H17 (p5 x0) H10); intros.
inversion_clear H18.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (fun n : name => nu (fun u : name => x2 u n)); split;
[ apply bRES with l; intros | idtac ].
inversion_clear H24;
change (btrans (p y) ((fun _ : name => In x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
intro; elim (LEM_name x0 y); intro.
rewrite <- H18;
elim
(unsat
(par (nu (fun n : name => nu (p5 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 empty)); intros.
inversion_clear H23.
inversion_clear H24; inversion_clear H25.
clear H27; cut (SBPAR_S (x2 x0 x3) (p5 x0 x3)); [ intro | auto ].
inversion_clear H25.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
elim
(unsat
(par (nu (fun n : name => nu (p5 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 (cons x3 (cons z empty)))); intros.
inversion_clear H29.
inversion_clear H30; inversion_clear H31.
inversion_clear H33.
inversion_clear H34.
clear H35.
cut (PAR_S_fun n2 (x2 x4 x3) (p5 x4 x3));
[ intro
| change
(PAR_S_fun n2 ((fun n : name => x2 n x3) x4)
((fun n : name => p5 n x3) x4)) in |- *; apply PAR_S_RW with x0;
auto ].
change
(PAR_S_fun n2 ((fun n : name => x2 n x0) z) ((fun n : name => p5 n x0) z))
in |- *; apply PAR_S_RW with x4; auto.
inversion_clear H32; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H36; auto.
inversion_clear H29; apply notin_nu; intros.
cut (notin x4 (nu (p5 z0))); [ intro | auto ].
inversion_clear H36; auto.
apply PAR_S_RW with x3; auto.
inversion_clear H26; auto.
inversion_clear H23; auto.
inversion_clear H21; auto.
inversion_clear H12; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p5 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H32; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H35; auto.
inversion_clear H29; apply notin_nu; intros.
cut (notin x4 (nu (p5 z0))); [ intro | auto ].
inversion_clear H35; auto.
cut (SBPAR_S (x2 x0 y) (p5 x0 y)); [ intro | auto ].
inversion_clear H23.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
change
(PAR_S_fun n2 ((fun n : name => x2 n y) z) ((fun n : name => p5 n y) z))
in |- *; apply PAR_S_RW with x0; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p5 z0))); [ intro | auto ].
inversion_clear H27; auto.
apply b_act_notin_In; auto.
split; intros.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim
(unsat (par (nu p) (par (nu q) (nu (fun n : name => nu (p6 n))))) (cons x l));
intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (btrans (p x0) (bOut x) (p6 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
inversion_clear H15.
elim (H16 x); intros.
elim (H15 (p6 x0) H10); intros.
inversion_clear H18.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (fun n : name => nu (fun u : name => x2 u n)); split;
[ apply bRES with l; intros | idtac ].
inversion_clear H24;
change (btrans (q y) ((fun _ : name => bOut x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
intros; elim (LEM_name x0 y); intro.
rewrite <- H24;
elim
(unsat
(par (nu (fun n : name => nu (p6 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 empty)); intros.
inversion_clear H25.
inversion_clear H26; inversion_clear H27.
clear H29; cut (SBPAR_S (p6 x0 x3) (x2 x0 x3)); [ intro | apply H20; auto ].
inversion_clear H27.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
elim
(unsat
(par (nu (fun n : name => nu (p6 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 (cons x3 (cons z empty)))); intros.
inversion_clear H31.
inversion_clear H32; inversion_clear H33.
inversion_clear H35.
inversion_clear H36.
clear H37.
cut (PAR_S_fun n2 (p6 x4 x3) (x2 x4 x3));
[ intro
| change
(PAR_S_fun n2 ((fun n : name => p6 n x3) x4)
((fun n : name => x2 n x3) x4)) in |- *; apply PAR_S_RW with x0;
auto ].
change
(PAR_S_fun n2 ((fun n : name => p6 n x0) z) ((fun n : name => x2 n x0) z))
in |- *; apply PAR_S_RW with x4; auto.
inversion_clear H31; apply notin_nu; intros.
cut (notin x4 (nu (p6 z0))); [ intro | auto ].
inversion_clear H38; auto.
inversion_clear H34; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H38; auto.
apply PAR_S_RW with x3; auto.
inversion_clear H25; auto.
inversion_clear H28; auto.
inversion_clear H12; auto.
inversion_clear H21; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p6 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H31; apply notin_nu; intros.
cut (notin x4 (nu (p6 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H34; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H25; auto.
inversion_clear H28; auto.
cut (SBPAR_S (p6 x0 y) (x2 x0 y)); [ intro | apply H20; auto ].
inversion_clear H25.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
change
(PAR_S_fun n2 ((fun n : name => p6 n y) z) ((fun n : name => x2 n y) z))
in |- *; apply PAR_S_RW with x0; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p6 z0))); [ intro | auto ].
inversion_clear H29; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H29; auto.
inversion_clear H18; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p6 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H23; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => x2 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
apply b_act_notin_bOut; auto.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu p4))) (cons x l)); intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (ftrans (p x0) (Out x x0) (p4 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
elim (H13 (Out x x0)); intros.
elim (H14 (p4 x0) H10); intros.
inversion_clear H17.
elim (proc_exp x1 x0); intros.
inversion_clear H17.
rewrite H21 in H18; rewrite H21 in H19.
exists x2; split; [ apply OPEN with l; intros | idtac ].
change (ftrans (q y) (Out x y) (x2 y)) in |- *; apply FTR_L3 with x0; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; inversion_clear H19.
apply sbpar_s with n2; apply PAR_S_RW with x0; auto.
inversion_clear H5.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim
(unsat (par (nu p) (par (nu q) (nu (fun n : name => nu (p5 n))))) (cons x l));
intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (btrans (q x0) (bOut x) (p5 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
inversion_clear H15.
elim (H16 x); intros.
elim (H17 (p5 x0) H10); intros.
inversion_clear H18.
elim (ho_proc_exp x1 x0); intros.
inversion_clear H18.
rewrite H22 in H19; rewrite H22 in H20.
exists (fun n : name => nu (fun u : name => x2 u n)); split;
[ apply bRES with l; intros | idtac ].
inversion_clear H24;
change (btrans (p y) ((fun _ : name => bOut x) y) (x2 y)) in |- *;
apply BTR_L3 with x0; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
intros; elim (LEM_name x0 y); intro.
rewrite <- H24;
elim
(unsat
(par (nu (fun n : name => nu (p5 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 empty)); intros.
inversion_clear H25.
inversion_clear H26; inversion_clear H27.
clear H29; cut (SBPAR_S (x2 x0 x3) (p5 x0 x3)); [ intro | apply H20; auto ].
inversion_clear H27.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
elim
(unsat
(par (nu (fun n : name => nu (p5 n))) (nu (fun n : name => nu (x2 n))))
(cons x0 (cons x3 (cons z empty)))); intros.
inversion_clear H31.
inversion_clear H32; inversion_clear H33.
inversion_clear H35.
inversion_clear H36.
clear H37.
cut (PAR_S_fun n2 (x2 x4 x3) (p5 x4 x3));
[ intro
| change
(PAR_S_fun n2 ((fun n : name => x2 n x3) x4)
((fun n : name => p5 n x3) x4)) in |- *; apply PAR_S_RW with x0;
auto ].
change
(PAR_S_fun n2 ((fun n : name => x2 n x0) z) ((fun n : name => p5 n x0) z))
in |- *; apply PAR_S_RW with x4; auto.
inversion_clear H34; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H38; auto.
inversion_clear H31; apply notin_nu; intros.
cut (notin x4 (nu (p5 z0))); [ intro | auto ].
inversion_clear H38; auto.
apply PAR_S_RW with x3; auto.
inversion_clear H28; auto.
inversion_clear H25; auto.
inversion_clear H21; auto.
inversion_clear H12; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p5 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H34; apply notin_nu; intros.
cut (notin x4 (nu (x2 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H31; apply notin_nu; intros.
cut (notin x4 (nu (p5 z0))); [ intro | auto ].
inversion_clear H37; auto.
inversion_clear H28; auto.
inversion_clear H25; auto.
cut (SBPAR_S (x2 x0 y) (p5 x0 y)); [ intro | apply H20; auto ].
inversion_clear H25.
apply sbpar_s with (S n2); simpl in |- *; apply op_par_s; intros.
change
(PAR_S_fun n2 ((fun n : name => x2 n y) z) ((fun n : name => p5 n y) z))
in |- *; apply PAR_S_RW with x0; auto.
inversion_clear H21; apply notin_nu; intros.
cut (notin x0 (nu (x2 z0))); [ intro | auto ].
inversion_clear H29; auto.
inversion_clear H12; apply notin_nu; intros.
cut (notin x0 (nu (p5 z0))); [ intro | auto ].
inversion_clear H29; auto.
inversion_clear H18; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => x2 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H23; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p5 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
apply b_act_notin_bOut; auto.
cut
(forall x : name,
notin x (nu p) -> notin x (nu q) -> Op_StBisim SBPAR_S (p x) (q x));
[ intro | auto ].
elim (unsat (par (nu p) (par (nu q) (nu q1))) (cons x l)); intros.
inversion_clear H7.
inversion_clear H8; inversion_clear H9.
inversion_clear H10.
cut (ftrans (q x0) (Out x x0) (q1 x0)); [ intro | apply H6; auto ].
cut (Op_StBisim SBPAR_S (p x0) (q x0)); [ intro | apply H5; auto ].
inversion_clear H13.
inversion_clear H14.
elim (H13 (Out x x0)); intros.
elim (H16 (q1 x0) H10); intros.
inversion_clear H17.
elim (proc_exp x1 x0); intros.
inversion_clear H17.
rewrite H21 in H18; rewrite H21 in H19.
exists x2; split; [ apply OPEN with l; intros | idtac ].
change (ftrans (p y) (Out x y) (x2 y)) in |- *; apply FTR_L3 with x0; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; inversion_clear H19.
apply sbpar_s with n2; apply PAR_S_RW with x0; auto.
Qed.
Lemma PAR_S : forall p q r : proc, StBisim p q -> StBisim (par p r) (par q r).
Proof.
intros; apply Completeness; apply Co_Ind with SBPAR_S;
[ exact SBPAR_S_TO_SB'
| apply sbpar_s with 0; simpl in |- *; apply bispar_s; assumption ].
Qed.
Lemma MATCH_S :
forall p q : proc,
StBisim p q -> forall x y : name, StBisim (match_ x y p) (match_ x y q).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion H0.
inversion H.
inversion_clear H7.
elim (H10 a); intros.
elim (H7 p1 H6); intros.
exists x1; split; [ apply fMATCH; tauto | tauto ].
inversion H0.
inversion H.
inversion_clear H7.
elim (H10 a); intros.
elim (H12 q1 H6); intros.
exists x1; split; [ apply fMATCH; tauto | tauto ].
inversion H0.
inversion H.
inversion_clear H7.
inversion_clear H11.
elim (H7 x0); intros.
elim (H11 p1 H6); intros.
inversion_clear H14.
exists x2; split; [ apply bMATCH; assumption | intro; auto ].
inversion H0.
inversion H.
inversion_clear H7.
inversion_clear H11.
elim (H7 x0); intros.
elim (H13 q1 H6); intros.
inversion_clear H14.
exists x2; split; [ apply bMATCH; assumption | intro; auto ].
inversion H0.
inversion H.
inversion_clear H7.
inversion_clear H11.
elim (H12 x0); intros.
elim (H11 p1 H6); intros.
inversion_clear H14.
exists x2; split; [ apply bMATCH; assumption | intros; auto ].
inversion H0.
inversion H.
inversion_clear H7.
inversion_clear H11.
elim (H12 x0); intros.
elim (H13 q1 H6); intros.
inversion_clear H14.
exists x2; split; [ apply bMATCH; assumption | intros; auto ].
Qed.
Lemma MISMATCH_S :
forall p q : proc,
StBisim p q -> forall x y : name, StBisim (mismatch x y p) (mismatch x y q).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion H0.
inversion H.
inversion_clear H8.
elim (H11 a); intros.
elim (H8 p1 H7); intros.
exists x1; split; [ apply fMISMATCH; tauto | tauto ].
inversion H0.
inversion H.
inversion_clear H8.
elim (H11 a); intros.
elim (H13 q1 H7); intros.
exists x1; split; [ apply fMISMATCH; tauto | tauto ].
inversion H0.
inversion H.
inversion_clear H8.
inversion_clear H12.
elim (H8 x0); intros.
elim (H12 p1 H7); intros.
inversion_clear H15.
exists x2; split; [ apply bMISMATCH; assumption | intro; auto ].
inversion H0.
inversion H.
inversion_clear H8.
inversion_clear H12.
elim (H8 x0); intros.
elim (H14 q1 H7); intros.
inversion_clear H15.
exists x2; split; [ apply bMISMATCH; assumption | intro; auto ].
inversion H0.
inversion H.
inversion_clear H8.
inversion_clear H12.
elim (H13 x0); intros.
elim (H12 p1 H7); intros.
inversion_clear H15.
exists x2; split; [ apply bMISMATCH; assumption | intros; auto ].
inversion H0.
inversion H.
inversion_clear H8.
inversion_clear H12.
elim (H13 x0); intros.
elim (H14 q1 H7); intros.
inversion_clear H15.
exists x2; split; [ apply bMISMATCH; assumption | intros; auto ].
Qed.
Lemma IN_S :
forall (p' q' : name -> proc) (x y : name),
notin y (nu p') ->
notin y (nu q') ->
(forall z : name,
isin z (nu p') \/ isin z (nu q') \/ z = y -> StBisim (p' z) (q' z)) ->
StBisim (in_pref x p') (in_pref x q').
Proof.
intros; apply sb; do 3 try (split; intros).
inversion_clear H2.
inversion_clear H2.
inversion H2.
rewrite <- H3 in H2; rewrite <- H5 in H2; rewrite <- H6 in H2.
exists q'; split.
apply IN.
rewrite <- H3; intro.
elim (LEM_OC (par (nu p') (par (nu q') (out_pref y y nil))) y0); intro.
inversion_clear H7;
[ apply H1; left; assumption
| inversion_clear H8;
[ apply H1; right; left; assumption
| inversion H7;
[ inversion_clear H9
| apply H1; right; right; trivial
| apply H1; right; right; trivial ] ] ].
inversion_clear H7.
inversion_clear H9.
inversion_clear H10.
clear H11 H12.
apply L6_Light with y; auto.
inversion H2.
rewrite <- H3 in H2; rewrite <- H5 in H2; rewrite <- H6 in H2.
exists p'; split.
apply IN.
rewrite <- H3; intro.
elim (LEM_OC (par (nu p') (par (nu q') (out_pref y y nil))) y0); intro.
inversion_clear H7;
[ apply H1; left; assumption
| inversion_clear H8;
[ apply H1; right; left; assumption
| inversion H7;
[ inversion_clear H9
| apply H1; right; right; trivial
| apply H1; right; right; trivial ] ] ].
inversion_clear H7.
inversion_clear H9.
inversion_clear H10.
clear H11 H12.
apply L6_Light with y; auto.
inversion_clear H2.
inversion_clear H2.
Qed.
Lemma OUT_S :
forall p q : proc,
StBisim p q -> forall x y : name, StBisim (out_pref x y p) (out_pref x y q).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion H0.
exists q; split; [ apply OUT | rewrite <- H5; assumption ].
inversion H0.
exists p; split; [ apply OUT | rewrite <- H5; assumption ].
inversion_clear H0.
inversion_clear H0.
inversion_clear H0.
inversion_clear H0.
Qed.
Lemma ID_SUM : forall p : proc, StBisim (sum p nil) p.
Proof.
intro; apply sb; do 3 try (split; intros).
inversion_clear H.
exists p1; split; [ assumption | apply REF ].
inversion_clear H0.
exists q1; split; [ apply fSUM1; assumption | apply REF ].
inversion_clear H.
exists p1; split; [ assumption | intro; apply REF ].
inversion_clear H0.
exists q1; split; [ apply bSUM1; assumption | intro; apply REF ].
inversion_clear H.
exists p1; split; [ assumption | intros; apply REF ].
inversion_clear H0.
exists q1; split; [ apply bSUM1; assumption | intros; apply REF ].
Qed.
Lemma IDEM_SUM : forall p : proc, StBisim (sum p p) p.
Proof.
intro; apply sb; do 3 try (split; intros).
inversion_clear H.
exists p1; split; [ assumption | apply REF ].
exists p1; split; [ assumption | apply REF ].
exists q1; split; [ apply fSUM1; assumption | apply REF ].
inversion_clear H.
exists p1; split; [ assumption | intro; apply REF ].
exists p1; split; [ assumption | intro; apply REF ].
exists q1; split; [ apply bSUM1; assumption | intro; apply REF ].
inversion_clear H.
exists p1; split; [ assumption | intros; apply REF ].
exists p1; split; [ assumption | intros; apply REF ].
exists q1; split; [ apply bSUM1; assumption | intros; apply REF ].
Qed.
Lemma COMM_SUM : forall p q : proc, StBisim (sum p q) (sum q p).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion_clear H.
exists p1; split; [ apply fSUM2; assumption | apply REF ].
exists p1; split; [ apply fSUM1; assumption | apply REF ].
inversion_clear H.
exists q1; split; [ apply fSUM2; assumption | apply REF ].
exists q1; split; [ apply fSUM1; assumption | apply REF ].
inversion_clear H.
exists p1; split; [ apply bSUM2; assumption | intro; apply REF ].
exists p1; split; [ apply bSUM1; assumption | intro; apply REF ].
inversion_clear H.
exists q1; split; [ apply bSUM2; assumption | intro; apply REF ].
exists q1; split; [ apply bSUM1; assumption | intro; apply REF ].
inversion_clear H.
exists p1; split; [ apply bSUM2; assumption | intros; apply REF ].
exists p1; split; [ apply bSUM1; assumption | intros; apply REF ].
inversion_clear H.
exists q1; split; [ apply bSUM2; assumption | intros; apply REF ].
exists q1; split; [ apply bSUM1; assumption | intros; apply REF ].
Qed.
Lemma ASS_SUM :
forall p q r : proc, StBisim (sum p (sum q r)) (sum (sum p q) r).
Proof.
intros; apply sb; do 3 try (split; intros).
inversion_clear H.
exists p1; split; [ apply fSUM1; apply fSUM1; assumption | apply REF ].
inversion_clear H0.
exists p1; split; [ apply fSUM1; apply fSUM2; assumption | apply REF ].
exists p1; split; [ apply fSUM2; assumption | apply REF ].
inversion_clear H.
inversion_clear H0.
exists q1; split; [ apply fSUM1; assumption | apply REF ].
exists q1; split; [ apply fSUM2; apply fSUM1; assumption | apply REF ].
exists q1; split; [ apply fSUM2; apply fSUM2; assumption | apply REF ].
inversion_clear H.
exists p1; split; [ apply bSUM1; apply bSUM1; assumption | intro; apply REF ].
inversion_clear H0.
exists p1; split; [ apply bSUM1; apply bSUM2; assumption | intro; apply REF ].
exists p1; split; [ apply bSUM2; assumption | intro; apply REF ].
inversion_clear H.
inversion_clear H0.
exists q1; split; [ apply bSUM1; assumption | intro; apply REF ].
exists q1; split; [ apply bSUM2; apply bSUM1; assumption | intro; apply REF ].
exists q1; split; [ apply bSUM2; apply bSUM2; assumption | intro; apply REF ].
inversion_clear H.
exists p1; split;
[ apply bSUM1; apply bSUM1; assumption | intros; apply REF ].
inversion_clear H0.
exists p1; split;
[ apply bSUM1; apply bSUM2; assumption | intros; apply REF ].
exists p1; split; [ apply bSUM2; assumption | intros; apply REF ].
inversion_clear H.
inversion_clear H0.
exists q1; split; [ apply bSUM1; assumption | intros; apply REF ].
exists q1; split;
[ apply bSUM2; apply bSUM1; assumption | intros; apply REF ].
exists q1; split;
[ apply bSUM2; apply bSUM2; assumption | intros; apply REF ].
Qed.
Lemma BANG_UNF : forall p : proc, StBisim (bang p) (par p (bang p)).
Proof.
intro; apply sb; do 3 try (split; intros).
exists p1; split; [ inversion_clear H; assumption | apply REF ].
exists q1; split; [ apply fBANG; assumption | apply REF ].
exists p1; split; [ inversion_clear H; assumption | intro; apply REF ].
exists q1; split; [ apply bBANG; assumption | intro; apply REF ].
exists p1; split; [ inversion_clear H; assumption | intros; apply REF ].
exists q1; split; [ apply bBANG; assumption | intros; apply REF ].
Qed.
Lemma NU_NIL : StBisim (nu (fun x : name => nil)) nil.
Proof.
apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim (unsat (par (nu (fun _ : name => nil)) (nu p2)) l); intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans nil tau (p2 x)); [ intro | apply H0; auto ].
inversion_clear H1.
apply f_act_notin_tau.
inversion_clear H.
elim (unsat (par (nu (fun _ : name => nil)) (nu p2)) (cons n (cons n0 l)));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H4.
cut (ftrans nil (Out n n0) (p2 x)); [ intro | apply H0; auto ].
inversion_clear H4.
apply f_act_notin_Out; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat (par (nu (fun _ : name => nil)) (nu (fun z : name => nu (p2 z))))
(cons x l)); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans nil (In x) (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
apply b_act_notin_In; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat (par (nu (fun _ : name => nil)) (nu (fun z : name => nu (p2 z))))
(cons x l)); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans nil (bOut x) (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
apply b_act_notin_bOut; auto.
elim (unsat (par (nu (fun _ : name => nil)) (nu p1)) (cons x l)); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (ftrans nil (Out x x0) (p1 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
inversion_clear H.
Qed.
Lemma NU_NIL1 :
forall (p : proc) (x : name),
StBisim (nu (fun y : name => out_pref y x p)) nil.
Proof.
intros; apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim (unsat (par (nu (fun y0 : name => out_pref y0 x p)) (nu p2)) l); intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (out_pref x0 x p) tau (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H1.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun y0 : name => out_pref y0 x p)) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H4.
cut (ftrans (out_pref x0 x p) (Out n n0) (p2 x0)); [ intro | apply H0; auto ].
inversion H4.
absurd (x0 = n); auto.
apply f_act_notin_Out; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => out_pref y0 x p))
(nu (fun z : name => nu (p2 z)))) (cons x0 l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (out_pref x1 x p) (In x0) (p2 x1)); [ intro | apply H0; auto ].
inversion_clear H2.
apply b_act_notin_In; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => out_pref y0 x p))
(nu (fun z : name => nu (p2 z)))) (cons x0 l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (out_pref x1 x p) (bOut x0) (p2 x1)); [ intro | apply H0; auto ].
inversion_clear H2.
apply b_act_notin_bOut; auto.
elim
(unsat (par (nu (fun y0 : name => out_pref y0 x p)) (nu p1)) (cons x0 l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (ftrans (out_pref x1 x p) (Out x0 x1) (p1 x1));
[ intro | apply H0; auto ].
inversion H2.
absurd (x1 = x0); auto.
inversion_clear H.
Qed.
Lemma NU_NIL2 :
forall p : name -> proc, StBisim (nu (fun y : name => in_pref y p)) nil.
Proof.
intros; apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim (unsat (par (nu (fun y0 : name => in_pref y0 p)) (nu p2)) l); intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (in_pref x p) tau (p2 x)); [ intro | apply H0; auto ].
inversion_clear H1.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun y0 : name => in_pref y0 p)) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H4.
cut (ftrans (in_pref x p) (Out n n0) (p2 x)); [ intro | apply H0; auto ].
inversion H4.
apply f_act_notin_Out; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => in_pref y0 p))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (in_pref x0 p) (In x) (p2 x0)); [ intro | apply H0; auto ].
inversion H2.
absurd (x0 = x); auto.
apply b_act_notin_In; auto.
inversion_clear H.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => in_pref y0 p))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (in_pref x0 p) (bOut x) (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
apply b_act_notin_bOut; auto.
elim (unsat (par (nu (fun y0 : name => in_pref y0 p)) (nu p1)) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (ftrans (in_pref x0 p) (Out x x0) (p1 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
inversion_clear H.
Qed.
Lemma NU_COMM :
forall p : name -> name -> proc,
StBisim (nu (fun y : name => nu (fun z : name => p y z)))
(nu (fun z : name => nu (fun y : name => p y z))).
Proof.
cofix; intro; apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim
(unsat (par (nu (fun y0 : name => nu (fun z : name => p y0 z))) (nu p2)) l);
intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (nu (fun z : name => p x z)) tau (p2 x));
[ intro | apply H0; auto ].
inversion H1.
elim (unsat (par (nu (fun z : name => p x z)) (nu p3)) l0); intros.
inversion_clear H8.
inversion_clear H9.
cut (ftrans (p x x0) tau (p3 x0)); [ intro | apply H7; auto ].
elim (ho_proc_exp p3 x); intros.
inversion_clear H12.
exists (nu (fun z : name => nu (fun y : name => x1 y z))); split.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H16.
inversion_clear H19.
clear H17 H20.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H20.
inversion_clear H23.
clear H21 H24.
change
(ftrans ((fun n : name => p n y) y0) ((fun _ : name => tau) y0)
((fun n : name => x1 n y) y0)) in |- *; apply FTR_L3 with x;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H23; auto.
inversion_clear H13; apply notin_nu; intros.
cut (notin x (nu (x1 z))); [ intro | auto ].
inversion_clear H23; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
change (ftrans (p x y) ((fun _ : name => tau) y) (x1 x y)) in |- *;
apply FTR_L3 with x0; auto.
inversion_clear H8; apply notin_nu; intros; auto.
rewrite <- H14; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
rewrite <- H14; assumption.
inversion_clear H12; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H23; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x1 y0 z))); [ intro | auto ].
inversion_clear H23; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
rewrite H14 in H5; cut (p2 = (fun n : name => nu (x1 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H12;
cut
(nu (fun n : name => nu (x1 n)) =
nu (fun n : name => nu (fun u : name => x1 n u)));
[ intro | apply ETA_EQ2 ].
rewrite H15; apply NU_COMM.
apply f_act_notin_tau.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun y0 : name => nu (fun z : name => p y0 z))) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
inversion_clear H4.
cut (ftrans (nu (fun z : name => p x z)) (Out n n0) (p2 x));
[ intro | apply H0; auto ].
inversion H4.
elim (unsat (par (nu (fun z : name => p x z)) (nu p3)) (cons n (cons n0 l0)));
intros.
inversion_clear H10.
inversion_clear H11; inversion_clear H12.
inversion_clear H14.
cut (ftrans (p x x0) (Out n n0) (p3 x0)); [ intro | apply H9; auto ].
elim (ho_proc_exp p3 x); intros.
inversion_clear H16.
exists (nu (fun z : name => nu (fun y : name => x1 y z))); split.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H20; inversion_clear H21.
inversion_clear H23.
clear H25.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H26; inversion_clear H27.
inversion_clear H29.
clear H31.
change
(ftrans ((fun n : name => p n y) y0) ((fun _ : name => Out n n0) y0)
((fun n : name => x1 n y) y0)) in |- *; apply FTR_L3 with x;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H31; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin x (nu (x1 z))); [ intro | auto ].
inversion_clear H31; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change (ftrans (p x y) ((fun _ : name => Out n n0) y) (x1 x y)) in |- *;
apply FTR_L3 with x0; auto.
inversion_clear H10; apply notin_nu; intros; auto.
rewrite <- H18; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite <- H18; assumption.
inversion_clear H16; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H31; auto.
inversion_clear H19; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x1 y0 z))); [ intro | auto ].
inversion_clear H31; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite H18 in H7; cut (p2 = (fun n : name => nu (x1 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H16;
cut
(nu (fun n : name => nu (x1 n)) =
nu (fun n : name => nu (fun u : name => x1 n u)));
[ intro | apply ETA_EQ2 ].
rewrite H19; apply NU_COMM.
apply f_act_notin_Out; auto.
apply f_act_notin_Out; auto.
generalize H; clear H; elim a; intros.
inversion_clear H.
elim
(unsat (par (nu (fun z : name => nu (fun y0 : name => p y0 z))) (nu p2)) l);
intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (nu (fun y0 : name => p y0 x)) tau (p2 x));
[ intro | apply H0; auto ].
inversion H1.
elim (unsat (par (nu (fun y0 : name => p y0 x)) (nu p0)) l0); intros.
inversion_clear H8.
inversion_clear H9.
cut (ftrans (p x0 x) tau (p0 x0)); [ intro | apply H7; auto ].
elim (ho_proc_exp p0 x); intros.
inversion_clear H12.
exists (nu (fun y : name => nu (fun z : name => x1 z y))); split.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H16.
inversion_clear H19.
clear H17 H20.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H20.
inversion_clear H23.
clear H21 H24.
change
(ftrans (p y y0) ((fun _ : name => tau) y0) ((fun n : name => x1 n y) y0))
in |- *; apply FTR_L3 with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H23; auto.
inversion_clear H13; apply notin_nu; intros.
cut (notin x (nu (x1 z))); [ intro | auto ].
inversion_clear H23; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
change
(ftrans ((fun n : name => p n x) y) ((fun _ : name => tau) y) (x1 x y))
in |- *; apply FTR_L3 with x0; auto.
rewrite <- H14; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
rewrite <- H14; assumption.
inversion_clear H12; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H23; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => x1 z0 z))); [ intro | auto ].
inversion_clear H23; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
inversion_clear H17; apply notin_nu; intros; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
rewrite H14 in H5; cut (p2 = (fun n : name => nu (x1 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H12;
cut
(nu (fun n : name => nu (x1 n)) =
nu (fun n : name => nu (fun u : name => x1 n u)));
[ intro | apply ETA_EQ2 ].
rewrite H15;
change
(StBisim
(nu
(fun y : name => nu (fun z : name => (fun u v : name => x1 v u) y z)))
(nu
(fun n : name =>
nu (fun u : name => (fun u' v : name => x1 v u') u n))))
in |- *; apply NU_COMM.
apply f_act_notin_tau.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun z : name => nu (fun y0 : name => p y0 z))) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
inversion_clear H4.
cut (ftrans (nu (fun y0 : name => p y0 x)) (Out n n0) (p2 x));
[ intro | apply H0; auto ].
inversion H4.
elim
(unsat (par (nu (fun y0 : name => p y0 x)) (nu p0)) (cons n (cons n0 l0)));
intros.
inversion_clear H10.
inversion_clear H11; inversion_clear H12.
inversion_clear H14.
cut (ftrans (p x0 x) (Out n n0) (p0 x0)); [ intro | apply H9; auto ].
elim (ho_proc_exp p0 x); intros.
inversion_clear H16.
exists (nu (fun y : name => nu (fun z : name => x1 z y))); split.
apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H20; inversion_clear H21.
inversion_clear H23.
clear H25; apply fRES with (cons x (cons x0 empty)); intros.
inversion_clear H26; inversion_clear H27.
inversion_clear H29.
clear H31;
change
(ftrans (p y y0) ((fun _ : name => Out n n0) y0)
((fun n : name => x1 n y) y0)) in |- *; apply FTR_L3 with x;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (nu (fun z0 : name => p z0 z))); [ intro | auto ].
inversion_clear H31; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin x (nu (x1 z))); [ intro | auto ].
inversion_clear H31; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change
(ftrans ((fun n : name => p n x) y) ((fun _ : name => Out n n0) y) (x1 x y))
in |- *; apply FTR_L3 with x0; auto.
rewrite <- H18; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite <- H18; assumption.
inversion_clear H16; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H31; auto.
inversion_clear H19; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => x1 z0 z))); [ intro | auto ].
inversion_clear H31; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H23; apply notin_nu; intros; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite H18 in H7; cut (p2 = (fun n : name => nu (x1 n)));
[ intro | apply proc_ext with x; auto ].
rewrite H16;
cut
(nu (fun n : name => nu (x1 n)) =
nu (fun n : name => nu (fun u : name => x1 n u)));
[ intro | apply ETA_EQ2 ].
rewrite H19;
change
(StBisim
(nu
(fun y : name => nu (fun z : name => (fun u v : name => x1 v u) y z)))
(nu
(fun n : name =>
nu (fun u : name => (fun u' v : name => x1 v u') u n))))
in |- *; apply NU_COMM.
apply f_act_notin_Out; auto.
apply f_act_notin_Out; auto.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => nu (fun z : name => p y0 z)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (btrans (nu (fun z : name => p x0 z)) (In x) (p2 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat (par (nu (fun z : name => p x0 z)) (nu (fun z : name => nu (p3 z))))
(cons x l0)); intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (btrans (p x0 x1) (In x) (p3 x1)); [ intro | apply H8; auto ].
elim (ho2_proc_exp p3 x0); intros.
inversion_clear H14.
exists (fun n : name => nu (fun z : name => nu (fun y : name => x2 y z n)));
split.
change
(btrans (nu (fun z : name => nu (fun y : name => p y z)))
(In x)
(fun n : name =>
nu
(fun z : name =>
(fun u v : name => nu (fun y : name => x2 y u v)) z n)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H18; inversion_clear H19.
inversion_clear H21.
clear H22;
change
(btrans (nu (fun y0 : name => p y0 y)) (In x)
(fun v : name => nu (fun y0 : name => (fun n : name => x2 n y) y0 v)))
in |- *; apply bRES with (cons x (cons x0 empty));
intros.
inversion_clear H23; inversion_clear H24.
inversion_clear H26.
clear H27;
change
(btrans ((fun n : name => p n y) y0) ((fun _ : name => In x) y0)
((fun n : name => x2 n y) y0)) in |- *; apply BTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin x0 (nu (x2 z y))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
change (btrans (p x0 y) ((fun _ : name => In x) y) (x2 x0 y)) in |- *;
apply BTR_L3 with x1; auto.
inversion_clear H9; apply notin_nu; intros; auto.
rewrite <- H16; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
rewrite <- H16; assumption.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin y (nu (fun v : name => nu (fun y0 : name => x2 y0 z v))));
[ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x2 y0 z z0))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
rewrite H16 in H6;
cut ((fun n y : name => nu (fun z : name => x2 n z y)) = p2);
[ intro | apply ho_proc_ext with x0; auto ].
rewrite <- H14; intro;
change
(StBisim
(nu
(fun z : name =>
nu (fun z0 : name => (fun u v : name => x2 u v y) z z0)))
(nu
(fun z : name =>
nu (fun y0 : name => (fun u v : name => x2 u v y) y0 z))))
in |- *; apply NU_COMM.
inversion_clear H15; do 3 (apply notin_nu; intros).
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H19.
cut (notin x0 (nu (x2 z z1))); [ intro | auto ].
inversion_clear H19; auto.
apply b_act_notin_In; auto.
apply b_act_notin_In; auto.
inversion_clear H.
elim
(unsat
(par (nu (fun z : name => nu (fun y0 : name => p y0 z)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (btrans (nu (fun y0 : name => p y0 x0)) (In x) (p2 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat
(par (nu (fun y0 : name => p y0 x0)) (nu (fun z : name => nu (p0 z))))
(cons x l0)); intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (btrans (p x1 x0) (In x) (p0 x1)); [ intro | apply H8; auto ].
elim (ho2_proc_exp p0 x0); intros.
inversion_clear H14;
exists (fun n : name => nu (fun z : name => nu (fun y : name => x2 y z n)));
split.
change
(btrans (nu (fun z : name => nu (fun y : name => p z y)))
(In x)
(fun n : name =>
nu
(fun z : name =>
(fun u v : name => nu (fun y : name => x2 y u v)) z n)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H18; inversion_clear H19.
inversion_clear H21.
clear H22;
change
(btrans (nu (fun y0 : name => p y y0)) (In x)
(fun v : name => nu (fun y0 : name => (fun n : name => x2 n y) y0 v)))
in |- *; apply bRES with (cons x (cons x0 empty));
intros.
inversion_clear H23; inversion_clear H24.
inversion_clear H26.
clear H27;
change
(btrans (p y y0) ((fun _ : name => In x) y0) ((fun n : name => x2 n y) y0))
in |- *; apply BTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin x0 (nu (x2 z y))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
change
(btrans ((fun n : name => p n x0) y) ((fun _ : name => In x) y) (x2 x0 y))
in |- *; apply BTR_L3 with x1; auto.
rewrite <- H16; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
rewrite <- H16; assumption.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun y0 : name => p z y0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin y (nu (fun v : name => nu (fun y0 : name => x2 y0 z v))));
[ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x2 y0 z z0))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
inversion_clear H21; apply notin_nu; intros; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
rewrite H16 in H6;
cut (p2 = (fun n y : name => nu (fun z : name => x2 n z y)));
[ intro | apply ho_proc_ext with x0; auto ].
rewrite H14; intro;
change
(StBisim
(nu
(fun z : name =>
nu (fun y0 : name => (fun u v : name => x2 v u y) z y0)))
(nu
(fun z : name =>
nu (fun z0 : name => (fun u v : name => x2 v u y) z0 z))))
in |- *; apply NU_COMM.
inversion_clear H15; do 3 (apply notin_nu; intros).
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H19.
cut (notin x0 (nu (x2 z z1))); [ intro | auto ].
inversion_clear H19; auto.
apply b_act_notin_In; auto.
apply b_act_notin_In; auto.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => nu (fun z : name => p y0 z)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (btrans (nu (fun z : name => p x0 z)) (bOut x) (p2 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat (par (nu (fun z : name => p x0 z)) (nu (fun z : name => nu (p3 z))))
(cons x l0)); intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (btrans (p x0 x1) (bOut x) (p3 x1)); [ intro | apply H8; auto ].
elim (ho2_proc_exp p3 x0); intros.
inversion_clear H14;
exists (fun n : name => nu (fun z : name => nu (fun y : name => x2 y z n)));
split.
change
(btrans (nu (fun z : name => nu (fun y : name => p y z)))
(bOut x)
(fun n : name =>
nu
(fun z : name =>
(fun u v : name => nu (fun y : name => x2 y u v)) z n)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H18; inversion_clear H19.
inversion_clear H21.
clear H22;
change
(btrans (nu (fun y0 : name => p y0 y)) (bOut x)
(fun v : name => nu (fun y0 : name => (fun n : name => x2 n y) y0 v)))
in |- *; apply bRES with (cons x (cons x0 empty));
intros.
inversion_clear H23.
inversion_clear H24.
inversion_clear H26.
clear H27;
change
(btrans ((fun n : name => p n y) y0) ((fun _ : name => bOut x) y0)
((fun n : name => x2 n y) y0)) in |- *; apply BTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin x0 (nu (x2 z y))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
change (btrans (p x0 y) ((fun _ : name => bOut x) y) (x2 x0 y)) in |- *;
apply BTR_L3 with x1; auto.
inversion_clear H9; apply notin_nu; intros; auto.
rewrite <- H16; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
rewrite <- H16; assumption.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin y (nu (fun v : name => nu (fun y0 : name => x2 y0 z v))));
[ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x2 y0 z z0))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
rewrite H16 in H6;
cut (p2 = (fun n y : name => nu (fun z : name => x2 n z y)));
[ intro | apply ho_proc_ext with x0; auto ].
rewrite H14; intros;
change
(StBisim
(nu
(fun z : name =>
nu (fun z0 : name => (fun u v : name => x2 u v y) z z0)))
(nu
(fun z : name =>
nu (fun y0 : name => (fun u v : name => x2 u v y) y0 z))))
in |- *; apply NU_COMM.
inversion_clear H15; do 3 (apply notin_nu; intros).
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H19.
cut (notin x0 (nu (x2 z z1))); [ intro | auto ].
inversion_clear H19; auto.
apply b_act_notin_bOut; auto.
elim (unsat (par (nu (fun z : name => p x0 z)) (nu (p2 x0))) (cons x l0));
intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (ftrans (p x0 x2) (Out x x2) (p2 x0 x2)); [ intro | apply H7; auto ].
exists (fun n : name => nu (fun z : name => p2 z n)); split.
apply OPEN with (cons x (cons x0 empty)); intros.
inversion_clear H17.
inversion_clear H19.
clear H20; apply fRES with (cons x0 (cons x1 empty)); intros.
inversion_clear H21; inversion_clear H22.
inversion_clear H24.
clear H26;
change
(ftrans ((fun n : name => p n y) y0) ((fun _ : name => Out x y) y0)
((fun n : name => p2 n y) y0)) in |- *; apply FTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H3; apply notin_nu; intros.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H26; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change (ftrans (p x0 y) (Out x y) (p2 x0 y)) in |- *; apply FTR_L3 with x2;
auto.
inversion_clear H9; apply notin_nu; intros; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p2 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; apply REF.
apply b_act_notin_bOut; auto.
elim
(unsat (par (nu (fun y0 : name => nu (fun z : name => p y0 z))) (nu p1))
(cons x l)); intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (ftrans (nu (fun z : name => p x0 z)) (Out x x0) (p1 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat (par (nu (fun z : name => p x0 z)) (nu p2)) (cons x (cons x0 l0)));
intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
inversion_clear H13.
cut (ftrans (p x0 x1) (Out x x0) (p2 x1)); [ intro | apply H8; auto ].
elim (ho_proc_exp p2 x0); intros.
inversion_clear H15; exists (fun y : name => nu (fun z : name => x2 y z));
split.
change
(btrans (nu (fun z : name => nu (fun y : name => p y z)))
(bOut x)
(fun y : name => nu (fun z : name => (fun u n : name => x2 n u) z y)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H19; inversion_clear H20.
inversion_clear H22.
clear H23; apply OPEN with (cons x0 empty); intros.
inversion_clear H25.
clear H27;
change
(ftrans ((fun n : name => p n y) y0) (Out x y0)
((fun n : name => x2 n y) y0)) in |- *; apply FTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H16; apply notin_nu; intros.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H27; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change (ftrans (p x0 y) ((fun _ : name => Out x x0) y) (x2 x0 y)) in |- *;
apply FTR_L3 with x1; auto.
inversion_clear H9; apply notin_nu; intros; auto.
rewrite <- H17; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite <- H17; assumption.
inversion_clear H15; apply notin_nu; intros;
cut (notin y (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H18; apply notin_nu; intros.
cut (notin y (nu (fun n : name => x2 n z))); [ intro | auto ].
inversion_clear H27; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite H17 in H6; cut (p1 = (fun n : name => nu (x2 n)));
[ intro | apply proc_ext with x0; auto ].
rewrite H15; intros; cut (nu (x2 y) = nu (fun n : name => x2 y n));
[ intro | apply ETA_EQ ]; rewrite H20; apply REF.
apply f_act_notin_Out; auto.
inversion_clear H.
elim
(unsat
(par (nu (fun z : name => nu (fun y0 : name => p y0 z)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (btrans (nu (fun y0 : name => p y0 x0)) (bOut x) (p2 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat
(par (nu (fun y0 : name => p y0 x0)) (nu (fun z : name => nu (p0 z))))
(cons x l0)); intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (btrans (p x1 x0) (bOut x) (p0 x1)); [ intro | apply H8; auto ].
elim (ho2_proc_exp p0 x0); intros.
inversion_clear H14;
exists (fun n : name => nu (fun z : name => nu (fun y : name => x2 y z n)));
split.
change
(btrans (nu (fun y : name => nu (fun z : name => p y z)))
(bOut x)
(fun n : name =>
nu
(fun z : name =>
(fun u v : name => nu (fun y : name => x2 y u v)) z n)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H18; inversion_clear H19.
inversion_clear H21.
clear H22;
change
(btrans (nu (fun z : name => p y z)) (bOut x)
(fun v : name => nu (fun y0 : name => (fun n : name => x2 n y) y0 v)))
in |- *; apply bRES with (cons x (cons x0 empty));
intros.
inversion_clear H23; inversion_clear H24.
inversion_clear H26.
clear H27;
change
(btrans (p y y0) ((fun _ : name => bOut x) y0)
((fun n : name => x2 n y) y0)) in |- *; apply BTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin x0 (nu (x2 z y))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
change
(btrans ((fun n : name => p n x0) y) ((fun _ : name => bOut x) y) (x2 x0 y))
in |- *; apply BTR_L3 with x1; auto.
rewrite <- H16; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
rewrite <- H16; assumption.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H17; apply notin_nu; intros.
cut (notin y (nu (fun v : name => nu (fun y0 : name => x2 y0 z v))));
[ intro | auto ].
inversion_clear H27; apply notin_nu; intros.
cut (notin y (nu (fun y0 : name => x2 y0 z z0))); [ intro | auto ].
inversion_clear H29; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
inversion_clear H21; apply notin_nu; intros; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
rewrite H16 in H6;
cut (p2 = (fun n y : name => nu (fun z : name => x2 n z y)));
[ intro | apply ho_proc_ext with x0; auto ].
rewrite H14; intros;
change
(StBisim
(nu
(fun z : name =>
nu (fun y0 : name => (fun u v : name => x2 v u y) z y0)))
(nu
(fun y0 : name =>
nu (fun z : name => (fun u v : name => x2 v u y) z y0))))
in |- *; apply NU_COMM.
inversion_clear H15; do 3 (apply notin_nu; intros).
cut (notin x0 (nu (fun z0 : name => nu (x2 z z0)))); [ intro | auto ].
inversion_clear H19; cut (notin x0 (nu (x2 z z1))); [ intro | auto ].
inversion_clear H19; auto.
apply b_act_notin_bOut; auto.
elim (unsat (par (nu (fun y0 : name => p y0 x0)) (nu (p2 x0))) (cons x l0));
intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
cut (ftrans (p x2 x0) (Out x x2) (p2 x0 x2)); [ intro | apply H7; auto ].
exists (fun n : name => nu (fun z : name => p2 z n)); split.
apply OPEN with (cons x (cons x0 empty)); intros.
inversion_clear H17.
inversion_clear H19.
clear H20; apply fRES with (cons x0 (cons x1 empty)); intros.
inversion_clear H21; inversion_clear H22.
inversion_clear H24.
clear H26;
change
(ftrans (p y y0) ((fun n : name => Out x y) y0)
((fun n : name => p2 n y) y0)) in |- *; apply FTR_L3 with x0;
auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H3; apply notin_nu; intros.
cut (notin x0 (nu (p2 z))); [ intro | auto ].
inversion_clear H26; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change (ftrans ((fun n : name => p n x0) y) (Out x y) (p2 x0 y)) in |- *;
apply FTR_L3 with x2; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H14; apply notin_nu; intros;
cut (notin y (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H26; auto.
inversion_clear H15; apply notin_nu; intros.
cut (notin y (nu (fun z0 : name => p2 z0 z))); [ intro | auto ].
inversion_clear H26; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H19; apply notin_nu; intros; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; apply REF.
apply b_act_notin_bOut; auto.
elim
(unsat (par (nu (fun z : name => nu (fun y0 : name => p y0 z))) (nu q1))
(cons x l)); intros.
inversion_clear H.
inversion_clear H1; inversion_clear H2.
cut (ftrans (nu (fun y0 : name => p y0 x0)) (Out x x0) (q1 x0));
[ intro | apply H0; auto ].
inversion H2.
elim
(unsat (par (nu (fun y0 : name => p y0 x0)) (nu p2)) (cons x (cons x0 l0)));
intros.
inversion_clear H9.
inversion_clear H10; inversion_clear H11.
inversion_clear H13.
cut (ftrans (p x1 x0) (Out x x0) (p2 x1)); [ intro | apply H8; auto ].
elim (ho_proc_exp p2 x0); intros.
inversion_clear H15; exists (fun y : name => nu (fun z : name => x2 y z));
split.
change
(btrans (nu (fun y : name => nu (fun z : name => p y z)))
(bOut x)
(fun y : name => nu (fun z : name => (fun u n : name => x2 n u) z y)))
in |- *; apply bRES with (cons x0 (cons x1 empty));
intros.
inversion_clear H19; inversion_clear H20.
inversion_clear H22.
clear H23; apply OPEN with (cons x0 empty); intros.
inversion_clear H25.
clear H27;
change (ftrans (p y y0) (Out x y0) ((fun n : name => x2 n y) y0)) in |- *;
apply FTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (nu (fun y0 : name => p y0 z))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H16; apply notin_nu; intros.
cut (notin x0 (nu (x2 z))); [ intro | auto ].
inversion_clear H27; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
change
(ftrans ((fun n : name => p n x0) y) ((fun _ : name => Out x x0) y)
(x2 x0 y)) in |- *; apply FTR_L3 with x1; auto.
rewrite <- H17; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite <- H17; assumption.
inversion_clear H15; apply notin_nu; intros;
cut (notin y (nu (fun z0 : name => p z z0))); [ intro | auto ].
inversion_clear H27; auto.
inversion_clear H18; apply notin_nu; intros.
cut (notin y (nu (fun n : name => x2 n z))); [ intro | auto ].
inversion_clear H27; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
inversion_clear H22; apply notin_nu; intros; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
rewrite H17 in H6; cut (q1 = (fun n : name => nu (x2 n)));
[ intro | apply proc_ext with x0; auto ].
rewrite H15; intros; cut (nu (x2 y) = nu (fun n : name => x2 y n));
[ intro | apply ETA_EQ ]; rewrite H20; apply REF.
apply f_act_notin_Out; auto.
Qed.
Lemma NU_SUM :
forall p q : name -> proc,
StBisim (nu (fun y : name => sum (p y) (q y))) (sum (nu p) (nu q)).
Proof.
intros; apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim (unsat (par (nu (fun y0 : name => sum (p y0) (q y0))) (nu p2)) l);
intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (sum (p x) (q x)) tau (p2 x)); [ intro | apply H0; auto ].
inversion_clear H1.
exists (nu p2); split.
apply fSUM1; apply fRES with l; intros.
change (ftrans (p y) ((fun _ : name => tau) y) (p2 y)) in |- *;
apply FTR_L3 with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (sum (p z) (q z))); [ intro | auto ].
inversion_clear H9; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
apply REF.
exists (nu p2); split.
apply fSUM2; apply fRES with l; intros.
change (ftrans (q y) ((fun _ : name => tau) y) (p2 y)) in |- *;
apply FTR_L3 with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (sum (p z) (q z))); [ intro | auto ].
inversion_clear H9; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_tau.
apply REF.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun y0 : name => sum (p y0) (q y0))) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H4.
cut (ftrans (sum (p x) (q x)) (Out n n0) (p2 x)); [ intro | apply H0; auto ].
inversion_clear H4.
exists (nu p2); split.
apply fSUM1; apply fRES with l; intros.
inversion_clear H9.
change (ftrans (p y) ((fun _ : name => Out n n0) y) (p2 y)) in |- *;
apply FTR_L3 with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (sum (p z) (q z))); [ intro | auto ].
inversion_clear H12; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
apply REF.
exists (nu p2); split.
apply fSUM2; apply fRES with l; intros.
inversion_clear H9.
change (ftrans (q y) ((fun _ : name => Out n n0) y) (p2 y)) in |- *;
apply FTR_L3 with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (sum (p z) (q z))); [ intro | auto ].
inversion_clear H12; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
apply REF.
apply f_act_notin_Out; auto.
generalize H; clear H; elim a; intros.
inversion_clear H.
exists q1; split.
inversion_clear H0.
apply fRES with l; intros.
clear H3; apply fSUM1; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H4; assumption.
apply f_act_notin_tau.
apply REF.
exists q1; split.
inversion_clear H0.
apply fRES with l; intros.
clear H3; apply fSUM2; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H4; assumption.
apply f_act_notin_tau.
apply REF.
inversion_clear H.
exists q1; split.
inversion_clear H0.
apply fRES with l; intros.
inversion_clear H3; apply fSUM1; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H6; assumption.
apply f_act_notin_Out; auto.
apply REF.
exists q1; split.
inversion_clear H0.
apply fRES with l; intros.
inversion_clear H3; apply fSUM2; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H6; assumption.
apply f_act_notin_Out; auto.
apply REF.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => sum (p y0) (q y0)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (sum (p x0) (q x0)) (In x) (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
exists (fun u : name => nu (fun v : name => p2 v u)); split.
apply bSUM1; apply bRES with l; intros.
inversion_clear H7.
change (btrans (p y) ((fun _ : name => In x) y) (p2 y)) in |- *;
apply BTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
intro; apply REF.
exists (fun u : name => nu (fun v : name => p2 v u)); split.
apply bSUM2; apply bRES with l; intros.
inversion_clear H7.
change (btrans (q y) ((fun _ : name => In x) y) (p2 y)) in |- *;
apply BTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_In; auto.
intro; apply REF.
apply b_act_notin_In; auto.
inversion_clear H.
exists q1; split.
inversion_clear H0.
apply bRES with l; intros.
apply bSUM1; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
intro; apply REF.
exists q1; split.
inversion_clear H0.
apply bRES with l; intros.
apply bSUM2; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
intro; apply REF.
inversion_clear H.
elim
(unsat
(par (nu (fun y0 : name => sum (p y0) (q y0)))
(nu (fun z : name => nu (p2 z)))) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (btrans (sum (p x0) (q x0)) (bOut x) (p2 x0)); [ intro | apply H0; auto ].
inversion_clear H2.
exists (fun u : name => nu (fun v : name => p2 v u)); split.
apply bSUM1; apply bRES with l; intros.
inversion_clear H7.
change (btrans (p y) ((fun _ : name => bOut x) y) (p2 y)) in |- *;
apply BTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
intros; apply REF.
exists (fun u : name => nu (fun v : name => p2 v u)); split.
apply bSUM2; apply bRES with l; intros.
inversion_clear H7.
change (btrans (q y) ((fun _ : name => bOut x) y) (p2 y)) in |- *;
apply BTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
unfold b_act_notin_ho in |- *; intros; apply b_act_notin_bOut; auto.
intros; apply REF.
apply b_act_notin_bOut; auto.
elim
(unsat (par (nu (fun y0 : name => sum (p y0) (q y0))) (nu p1)) (cons x l));
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
cut (ftrans (sum (p x0) (q x0)) (Out x x0) (p1 x0));
[ intro | apply H0; auto ].
inversion_clear H2.
exists p1; split.
apply bSUM1; apply OPEN with l; intros.
change (ftrans (p y) (Out x y) (p1 y)) in |- *; apply FTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; apply REF.
exists p1; split.
apply bSUM2; apply OPEN with l; intros.
change (ftrans (q y) (Out x y) (p1 y)) in |- *; apply FTR_L3 with x0; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x0 (sum (p z) (q z))); [ intro | auto ].
inversion_clear H10; assumption.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
unfold f_act_notin_ho in |- *; intros; apply f_act_notin_Out; auto.
intros; apply REF.
inversion_clear H.
exists q1; split.
inversion_clear H0.
apply bRES with l; intros.
apply bSUM1; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
apply OPEN with l; intros.
apply fSUM1; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
intros; apply REF.
exists q1; split.
inversion_clear H0.
apply bRES with l; intros.
apply bSUM2; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
apply OPEN with l; intros.
apply fSUM2; apply H; auto.
inversion_clear H0; apply notin_nu; intros.
cut (notin y (sum (p z) (q z))); [ intro | auto ].
inversion_clear H5; assumption.
intros; apply REF.
Qed.
Lemma NU_TAU_PREF :
forall p : name -> proc,
StBisim (nu (fun x : name => tau_pref (p x))) (tau_pref (nu p)).
Proof.
intros; apply sb; do 3 try (split; intros).
generalize H; clear H; elim a; intros.
inversion_clear H.
elim (unsat (par (nu (fun x : name => tau_pref (p x))) (nu p2)) l); intros.
inversion_clear H.
inversion_clear H1.
cut (ftrans (tau_pref (p x)) tau (p2 x)); [ intro | apply H0; auto ].
inversion H1.
exists (nu p); split.
apply TAU.
apply NU_S; intros.
apply L6_Light with x; auto.
inversion_clear H; apply notin_nu; intros.
cut (notin x (tau_pref (p z))); [ intro | auto ].
inversion_clear H9; assumption.
rewrite H4; apply REF.
apply f_act_notin_tau.
inversion_clear H.
elim
(unsat (par (nu (fun x : name => tau_pref (p x))) (nu p2))
(cons n (cons n0 l))); intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H4.
cut (ftrans (tau_pref (p x)) (Out n n0) (p2 x)); [ intro | apply H0; auto ].
inversion_clear H4.
apply f_act_notin_Out; auto.
inversion H.
exists (nu p); split.
apply fRES with empty; intros.
clear H5 H6.
apply TAU.
apply REF.
inversion_clear H.
elim
(unsat
(par (nu (fun x0 : name => tau_pref (p x0)))
(