fact: CoInductive isTrace : Stream S -> Prop := | isTraceTick : forall (x : Stream S) (s : S), inv (inc s tick) -> isTrace (inc s tick ^ x) -> isTrace (s ^ inc s tick ^ x) | isTraceDisc : forall (x : Stream S) (s1 s2 : S) (l : Label), tr s1 l s2 -> inv s2 -> isTrace (s2 ^ x) -> isTrace (s1 ^ s2 ^ x).
imports: Streams time_clocks