proposition: Theorem Evt45 : forall (b : bool) (s : Stream A) (p : Process) (ss : Discourse Channel Act), Equity p ss -> p = SENDING b s || ACK b \/ p = SENDING b s || ACKING b -> Evt Channel Act Trans (OneDel (hd (tl s))) p ss.
proof: Proof. intros b s p ss H. generalize H. elim (Evt_from_Equity p ss H). intros q c w ss0 p0 T H1 HypInd EqH whichisp0. apply (notyet _ _ Trans (OneDel (hd (tl s))) q). assumption. intros q0 T0 H0. case whichisp0; clear whichisp0; intro whichisp0. rewrite whichisp0 in T0. case (State4 b s c w q0). assumption. intros state4. case state4. intros whichisc whichisq0. apply HypInd. rewrite whichisp0; assumption. unfold Precondition in |- *. red in |- *. intro. apply H2. rewrite whichisp0. apply exep4. assumption. apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. auto. intros state4. case state4. intro state4p; case state4p; intros whichisc whichisq0. apply (Evt1 (negb b) (tl s) q0 ss0). apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. rewrite negb_elim. assumption. intros state4p. case state4p. intros whichiswc whichisq0. apply HypInd. rewrite whichisp0; assumption. unfold Precondition in |- *. red in |- *. intro. apply H2. rewrite whichisp0. apply exep5. assumption. apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. auto. rewrite whichisp0 in T0. case (State5 b s c w q0). assumption. intros state5; case state5; intros whichisc whichisq0. apply HypInd. rewrite whichisp0; assumption. unfold Precondition in |- *. red in |- *. intro. apply H2. rewrite whichisp0. apply exep6. apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. auto. intros state5; case state5; intros whichisc whichisq0. apply HypInd. rewrite whichisp0; assumption. unfold Precondition in |- *. red in |- *. intro. apply H2. rewrite whichisp0. apply exep6. apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. auto. Defined.
imports: ABP.ABP.TRACES.Lemmas