proposition: Lemma mx_star_charac: forall n (M: LMX n n), M# == mx_lang_Union (iter M).
proof: Proof. intros. apply leq_antisym. star_left_induction. apply plus_destruct_leq. rewrite <- (leq_mx_lang_Union _ O). reflexivity. mx_intros s t Hs Ht. simpl. fold_langAlg label. apply sum_leq. intros k _ Hk. rewrite lang_leq. intros w [u Hu [v [o Hv] ->]]. exists (Datatypes.S o). simpl. rewrite lang_sum. exists k; auto. exists u; auto. exists v; auto. apply <- mx_lang_Union_spec. intro m. induction m. unfold iter. auto with algebra. change (iter M (Datatypes.S m)) with (M * (iter M m)). rewrite IHm. rewrite <- (star_make_right M) at 2. apply plus_make_right. Qed.
imports: Coq(List) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(Functors) ATBR(MxFunctors) ATBR(DKA_Definitions) ATBR(Model_Languages)