proposition: Lemma mx_blocks_star: forall x n (a: MX x x) (b: MX x n) (c: MX n x) (d: MX n n), let e := d# in let be:= b*e in let ec:= e*c in let f := (a + be*c)# in let fbe := f*be in let ecf := ec*f in (mx_blocks a b c d)# == mx_blocks f fbe ecf (e + ecf*be).
proof: Proof. intros. rewrite mx_blocks_star'. unfold mx_star_block, star_build. repeat match goal with |- context[star_rec ?M] => change (star_rec M) with (M#) end. Opaque equal. apply mx_blocks_compat; auto 9 using mx_block_00, mx_block_01, mx_block_10, mx_block_11 with compat. Transparent equal. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)