proposition: Theorem Kozen94: forall a b, decide_kleene a b = None <-> a == b.
proof: Proof. unfold decide_kleene. intros a b. case_eq (DKA_CheckLabels.same_labels (clean a) (clean b)); simpl; intros Hm. rewrite translate_correct. rewrite DKA_Merge.correct; try apply X_to_DFA_bounded. setoid_rewrite X_to_DFA_correct. setoid_rewrite <- RegExp.Clean.correct. reflexivity. apply DKA_DFA_Equiv.correct. apply X_to_DFA_labels, Hm. split; intro H. discriminate H. exfalso. apply DKA_CheckLabels.complete in Hm. tauto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)