proposition: Lemma counter_exemple_loop: forall b w n v t, bounded_word A v -> loop A n v t (read A (rev v) i) (read A (rev v) j) = inr (b,w) -> DFA_language (change_initial A (select b i j)) w /\ ~ DFA_language (change_initial A (select b j i)) w.
proof: Proof. induction n; intros v tar Hv. intro. discriminate. simpl. case DS.test_and_unify. intros [|] tar'. intro. discriminate. bool_analyse. clear e tar. revert v Hv tar'. generalize (le_n (max_label A)). generalize (max_label A) at 1 3 as a. induction a using num_peano_rec; [setoid_rewrite fold_num_sum_O|setoid_rewrite fold_num_sum_S]; intros Ha v Hv tar; simpl. intro. discriminate. num_simpl. simpl. num_simpl. generalize (IHn (a::v) tar). simpl. rewrite 2 read_app. simpl. case loop. intros tar' _ H. apply IHa in H; auto with arith. intros p H H'. dependent destruction H'. apply H; auto. intros c [->|Hc]; auto with arith. num_lia. clear IHn. intro H'; injection H'; intros; subst; clear H'. StateSetProps.mem_analyse; StateSetProps.mem_analyse; (elim H; reflexivity) || (unfold DFA_language, bounded_word; setoid_rewrite <- In_rev; 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)