proposition: Lemma counter_exemple_equiv: forall b w, equiv A i j = Some (b,w) -> DFA_language (change_initial A (select b i j)) w /\ ~ DFA_language (change_initial A (select b j i)) w.
proof: Proof. intros b w. unfold equiv. case_eq (loop A (Datatypes.S (size A)) nil DS.empty i j). intros; discriminate. intros [b' w'] H H'. injection H'; intros; subst. clear H'. apply (@counter_exemple_loop b w _ nil) in H. assumption. intro. simpl. tauto. 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) ATBR(DKA_StateSetSets) ATBR(Utils_WF) Coq(Relations) Coq(List)