proposition: Lemma Unique45 : forall (b : bool) (s : Stream A) (p : Process) (ss : Discourse Channel Act) (q : Process) (ss1 : Discourse Channel Act), Wittness Channel Act Trans A OneDel (hd (tl s)) q ss1 p ss -> p = SENDING b s || ACK b \/ p = SENDING b s || ACKING b -> q = SENDING (negb b) (tl s) || ACK (negb b).
proof: Proof. intros b s p ss q ss1 H. elim H. intros p0 ss0 c0 w0 q0 T H1 H2 HypInd whichisp0. case whichisp0; clear whichisp0; intro whichisp0. case (State4 b s c0 w0 q0). rewrite whichisp0 in T; assumption. intro state; case state; intros whichc whichq0. apply HypInd. auto. intro state. case state. intro statep1; case statep1; intros whichc whichq0. apply (Unique1 (negb b) (tl s) q0 ss0 q ss1). assumption. rewrite negb_elim; assumption. intro statep2; case statep2; intros whichc whichq0. apply HypInd. auto. case (State5 b s c0 w0 q0). rewrite whichisp0 in T; assumption. intro state; case state; intros whichc whichq0. apply HypInd. auto. intro state; case state; intros whichc whichq0. apply HypInd. auto. intros c0 w0 p0 T H1 whichisp0. case whichisp0; clear whichisp0; intro whichisp0. case (State4 b s c0 w0 q). rewrite whichisp0 in T; assumption. intro state; case state; intros whichc whichq0. absurd (c0 = lnk1). unfold OneDel in H1. dependent rewrite H1. discriminate. assumption. intro statep1; case statep1. intro state; case state; intros whichc whichq0. absurd (c0 = lnk2). unfold OneDel in H1. dependent rewrite H1. discriminate. dependent rewrite whichc. trivial. intro state; case state; intros whichc whichq0. absurd (c0 = lnk2). unfold OneDel in H1. dependent rewrite H1. discriminate. dependent rewrite whichc. trivial. case (State5 b s c0 w0 q). rewrite whichisp0 in T; assumption. intro state; case state; intros whichc whichq0. absurd (c0 = lnk1). unfold OneDel in H1. dependent rewrite H1. discriminate. dependent rewrite whichc. trivial. intro state; case state; intros whichc whichq0. absurd (c0 = lnk1). unfold OneDel in H1. dependent rewrite H1. discriminate. dependent rewrite whichc. trivial. Defined.
imports: ABP.ABP.TRACES.Lemmas