proposition: Lemma eval_star i f s t a A: belong i A -> belong f A -> belong s A -> belong t A -> eval i f (add a (size A) (size A) (add 1 s (size A) (add 1 (size A) t (incr A)))) == eval i f (add (a#) s t A).
proof: Proof. cbn - [eval]; intros Hi Hf Hs Ht. rewrite eval_master_theorem;auto. apply eval_compat, add_compat'; auto. semiring_reflexivity. 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)