proposition: Lemma commute_add_one: forall i f A, bounded A -> belong i A -> belong f A -> Algebraic.add_one (nat_of_state i) (nat_of_state f) (preNFA_to_preMAUT A) [=0=] preNFA_to_preMAUT (add_one i f A).
proof: Proof. Opaque add_one. intros i f [sA epsA deltaA mlA]. constructor. mx_intros s t Hs Ht. simpl in *. fold_regex. rewrite plus_com, plus_assoc. apply plus_compat; trivial. rewrite epsilonbrel_add_one. case (epsilonbrel (mk sA epsA deltaA mlA) (state_of_nat s) (state_of_nat t)); simpl; nat_analyse; simpl; fold_regex; auto with algebra; num_analyse; simpl; fold_regex; auto with algebra; num_lia_false. Transparent add_one. 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)