fact: CoFixpoint ACKING : bool -> Process := fun b : bool => ACLISTEN Channel Act lnk1 (fun ba : bool * A => let (b1, a) := ba in if eqb b1 (negb b) then OUT (negb b) a else ACK b) with OUT : bool -> A -> Process := fun (b1 : bool) (a : A) => ACTALK Channel Act del a (ACK b1) lnk1 (fun _ : bool * A => OUT b1 a) with ACK : bool -> Process := fun b : bool => ACTALK Channel Act lnk2 b (ACKING b) lnk1 (fun _ : bool * A => ACK b).
imports: Bool Streams ABP.ABP.BISIMULATION.Processes