proposition: Theorem valid i j: belong i A -> belong j A -> equiv A i j = None -> eval (change_initial A i) == eval (change_initial A j).
proof: Proof. intros Hi Hj H'. unfold equiv in H'. case_eq (loop A (Datatypes.S size) nil DS.empty i j); intros R HR; rewrite HR in H'. apply (eval_change_initial Hi Hj HR). discriminate. 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)