proposition: Corollary ka_leq_dec: forall e f: regex', {e ≦f} + {~(e ≦f)}.
proof: Proof. assert(G: forall e f: regex', let A := dfa [] e in let B := dfa (dfa.vars A) f in dfa.lang A (dfa.u A) ≦ dfa.lang B (dfa.u B) <-> e ≦f). intros e f A B. rewrite <-2nfa.dfa.eval_lang, <-2dfa.reroot_id. rewrite ka_correct_complete_leq. unfold A, B. now rewrite 2eval_dfa. intros. eapply sumbool_iff. apply G. apply dfa.lang_incl_dec. lattice. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation