proposition: Lemma eval_dot i f s t a b: forall A, belong i A -> belong f A -> belong s A -> belong t A -> eval i f (add b (size A) t (add a s (size A) (incr A))) == eval i f (add (a*b) s t A).
proof: Proof. intros [n M]. cbn - [eval]. intros Hi Hf Hs Ht. setoid_replace (a*b: regex) with (a*0#*b)%A using relation RegExp.equal. rewrite add_comm; rewrite <- eval_master_theorem;auto. apply eval_compat. rewrite add_zero. reflexivity. fold_regex. rewrite star_zero. semiring_reflexivity. 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_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)