proposition: Lemma eval_master_theorem i f s t a b c: forall A, belong i A -> belong f A -> belong s A -> belong t A -> eval i f (add c (size A) (size A) (add a s (size A) (add b (size A) t (incr A)))) == eval i f (add (a*c#*b) s t A).
proof: Proof. intros [n M]; cbn; intros Hi Hf Hs Ht. apply mx_to_scal_compat; cbn. change 1%nat with (0+1)%nat. rewrite mx_point_blocks10 by trivial. rewrite mx_point_blocks10 by trivial. rewrite mx_point_blocks01 by trivial. rewrite mx_point_blocks11 by trivial. setoid_rewrite mx_point_blocks01 at 2; trivial. cbn. rewrite 2 Nat.sub_diag. set (U := mx_point 1 n 0 i (1: regex)). set (V := mx_point n 1 f 0 (1: regex)). set (Y := mx_point n 1 s 0 (a: regex)). set (Z := mx_point 1 n 0 t (b: regex)). set (A := mx_point 1 1 0 0 c). set (AS := M + mx_point n n s t (a*c#*b)). rewrite 3 mx_blocks_plus. apply eval_select_block. rewrite !plus_neutral_right, !plus_neutral_left. apply plus_compat; trivial. unfold A, Y, Z. rewrite mx_point_scal. rewrite <- mx_of_scal_star. rewrite <- mx_point_scal. rewrite mx_point_dot by trivial with arith. rewrite mx_point_dot by trivial with arith. apply mx_point_compat. 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)