fact: Definition decide_kleene a b := let a := clean a in let b := clean b in if negb (DKA_CheckLabels.same_labels a b) then Some DifferentAtomSets else translate_ce (DKA_Merge.compare_DFAs DKA_DFA_Equiv.equiv (X_to_DFA a) (X_to_DFA b)).
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)