proposition: Lemma no_deadlocks : forall q:states A1, ~ deadlock A1 q.
proof: Proof. unfold deadlock in |- *; simple destruct q; intro H. - absurd (transitions A1 q0 a = nil). + cbn in *; discriminate. + auto. - absurd (transitions A1 q1 a = nil). + cbn in *; discriminate. + auto. - absurd (transitions A1 q2 b = nil). + cbn in *; discriminate. + auto. Qed.
imports: Arith List RelationClasses