proposition: Lemma X_to_DFA_correct: forall a, DFA.eval (X_to_DFA a) == a.
proof: Proof. intro a. unfold X_to_DFA. rewrite DKA_Determinisation.correct by apply DKA_Epsilon.bounded, DKA_Construction.bounded. rewrite DKA_Epsilon.correct by apply DKA_Construction.bounded. rewrite DKA_Construction.correct. apply StrictStarForm.ssf_correct. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)