fact: CoInductive Trace (A:automaton) : states A -> LList (actions A) -> Prop := | empty_trace : forall q:states A, deadlock A q -> Trace A q LNil | lcons_trace : forall (q q':states A) (a:actions A) (l:LList (actions A)), In q' (transitions A q a) -> Trace A q' l -> Trace A q (LCons a l).
imports: Arith List RelationClasses