proposition: Lemma eval_select_block m x y z: forall (U: KMX x m) (A M: KMX m m) B C (D: KMX y y) (V: KMX m z), A+B*D#*C == M -> mx_blocks (x:=0) 0 0 U 0 * (mx_blocks A B C D)# * mx_blocks (y:=0) 0 V 0 0 == U * M# * V.
proof: Proof. intros. rewrite mx_blocks_star. rewrite 2 mx_blocks_dot. rewrite mx_blocks_degenerate_11. rewrite H. 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)