proposition: Lemma commute_build: forall a i f A, bounded A -> belong i A -> belong f A -> Algebraic.build a (nat_of_state i) (nat_of_state f) (preNFA_to_preMAUT A) [=0=] preNFA_to_preMAUT (build a i f A).
proof: Proof. induction a; intros s t A HA Hs Ht; simpl. apply commute_add_one; auto. reflexivity. rewrite <- IHa1 by auto. rewrite <- IHa2 by auto. rewrite <- commute_incr by auto. reflexivity. rewrite <- IHa1 by auto. rewrite <- IHa2 by auto. reflexivity. rewrite <- commute_add_one by auto. rewrite <- IHa by auto. rewrite <- commute_add_one by auto. rewrite <- commute_incr by auto. reflexivity. apply commute_add_var; auto. 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)