proposition: Lemma Evt1 : forall (b : bool) (s : Stream A) (p : Process) (ss : Discourse Channel Act), Equity p ss -> p = SEND b s || ACKING (negb b) -> Evt Channel Act Trans (OneDel (hd 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 s)) q). assumption. intros q0 T0 H0. rewrite whichisp0 in T0. case (State1 b s c w q0). assumption. intro state1; case state1; intros whichisc whichisq0. apply (Evt3 b s q0 ss0). apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. assumption. intros state2. case state2. intros whichiscw whichisq0. apply (Evt2 b s q0 ss0). apply (Always_stable Channel Act Trans (Evt Channel Act Trans Precondition) p0 ss0 c w q0). rewrite whichisp0; assumption. assumption. assumption. Defined.
imports: ABP.ABP.TRACES.Lemmas