proposition: Lemma state4 : forall (b : bool) (s : Stream A), weak_eq Channel Act Trans Silent (SENDING b s || ACK b) (REPEAT (tl s)).
proof: Proof. cofix. intros. apply w_eq. simple destruct c. simpl in |- *. intros. inversion H using PAR_UinvT. simpl in |- *. intros p3 p5 v H2 H3. inversion H2 using SENDING_UinvTC1 in H3. inversion H3 using ACK_UinvR. exists (REPEAT (tl s)). split; [ apply eps | apply state4 ]. exact I. intros. inversion H1 using ACK_UinvTC1 in H0. intros. rewrite (SENDING_ULoosed b s p3 H0). exists (REPEAT (tl s)). split; [ apply eps | apply state4 ]. exact I. intros. rewrite (ACK_ULoosed b lnk1 p4 H0). exists (REPEAT (tl s)). split; [ apply eps | apply state5 ]. exact I. simpl in |- *. intros. inversion H using PAR_UinvT. intros p3 p5 v H0 H1. inversion H0 using SENDING_UinvT2. intros p3 p5 v H0 H1. inversion H1 using ACK_UinvTC2 in H0. inversion H0 using SENDING_UinvR. exists (REPEAT (tl s)). split. apply eps. exact I. rewrite (eqb_reflx b). pattern b at 2 in |- *. rewrite (negb_intro b). apply (state1 (negb b) (tl s)). intros p3 H0. inversion H0 using SENDING_UinvT2. intros p3 H0. rewrite (ACK_ULoosed b lnk2 p3). exists (REPEAT (tl s)). split; [ apply eps | apply state5 ]. exact I. assumption. simpl in |- *. intros. inversion H using PAR_SinvT. intros p3 p5 v H2. inversion H2 using SENDING_SinvT. intros p3 p5 v H2 H3. inversion H3 using ACK_SinvT. simple destruct c. simpl in |- *. intros. inversion H using REPEAT_UinvTC1. simpl in |- *. intros. inversion H using REPEAT_UinvTC2. simpl in |- *. intros. inversion H using REPEAT_SinvT. exists (SENDING (negb b) (tl s) || ACK (negb b)). split. apply (w_tau_left Channel Act Trans Silent del lnk2 (Clear _ Act lnk2 b) (Clear _ Act del (hd (tl s))) (SENDING b s || ACK b) (SEND (negb b) (tl s) || ACKING b)). exact I. simpl in |- *. apply utpar2. rewrite unfold_SENDING. cut (SEND (negb b) (tl s) = (if eqb b b then SEND (negb b) (tl s) else SEND b s)). intro. pattern (SEND (negb b) (tl s)) at 2 in |- *. rewrite H0. apply (uttalk2 Channel Act lnk2 lnk1 (b, hd s) (fun b1 : bool => if eqb b1 b then SEND (negb b) (tl s) else SEND b s)). rewrite (eqb_reflx b). trivial. rewrite unfold_ACK. apply uttalk1. apply (w_tau_left Channel Act Trans Silent del lnk1 (Clear _ Act lnk1 (negb b, hd (tl s))) (Clear _ Act del (hd (tl s))) (SEND (negb b) (tl s) || ACKING b) (SENDING (negb b) (tl s) || OUT (negb b) (hd (tl s)))). apply I. simpl in |- *. apply utpar1. rewrite unfold_SEND. apply uttalk1. rewrite unfold_ACKING. apply utlisten1. rewrite (eqb_reflx (negb b)). trivial. apply w_single. red in |- *; trivial. simpl in |- *. apply stpar2. rewrite unfold_SENDING. apply sttalk3. discriminate. rewrite unfold_OUT. apply sttalk1. apply state4. Qed.
imports: ABP.ABP.BISIMULATION.Protocol ABP.ABP.BISIMULATION.Hypotheses ABP.ABP.BISIMULATION.Lemmas