fact: Definition star_build x n (sx: SMX x -> SMX x) (sn: SMX n -> SMX n) (M: SMX (x+n)): SMX (x+n) := let a := mx_sub00 M in let b := mx_sub01 M in let c := mx_sub10 M in let d := mx_sub11 M in let e := sn d in let be:= b*e in let ec:= e*c in let f := sx (a + be*c) in let fbe := f*be in let ecf := ec*f in mx_blocks f fbe ecf (e + ecf*be).
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)