proposition: Lemma X_to_DFA_labels: forall a b, DKA_CheckLabels.same_labels (clean a) (clean b) = true -> DFA.max_label (X_to_DFA (clean a)) = DFA.max_label (X_to_DFA (clean b)).
proof: Proof. intros. unfold X_to_DFA. rewrite 2 DKA_Determinisation.preserve_max_label. rewrite 2 DKA_Epsilon.preserve_max_label. apply DKA_Construction.same_labels_max_label. apply DKA_CheckLabels.same_labels_ssf. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)