proposition: Lemma correctness_cycle : forall (b : bool) (s : Stream A) (p : Process) (d : Discourse Channel Act), p = SENDING b s || ACK b -> Equity p d -> InTrace (tl s) p d.
proof: Proof. cofix. intros b s p d H E. unfold InTrace in |- *. apply palways. apply (Evt45 b s p). assumption. auto. intros q ss1 H2. apply (correctness_cycle (negb b) (tl s) q ss1). apply (Unique45 b s p d q ss1). assumption. auto. apply (StillHappens Channel Act Trans A OneDel (Evt Channel Act Trans Precondition) (hd (tl s)) p d q ss1). assumption. assumption. Defined.
imports: ABP.ABP.TRACES.Hypotheses Evt Unique