proposition: Theorem correct: forall A B, bounded A -> bounded B -> max_label A = max_label B -> (compare_DFAs equiv A B = None <-> eval A == eval B).
proof: Proof. unfold compare_DFAs. intros A B HA HB H. rewrite <- (eval_left B HA). rewrite <- (eval_right HB H). apply equiv_correct. apply merge_bounded; assumption. simpl. apply below_max_pi0. eapply bounded_initial, HA. simpl. apply below_max_pi1. eapply bounded_initial, HB. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions)