proposition: Lemma commute_incr: forall A, bounded A -> Algebraic.incr (preNFA_to_preMAUT A) [=0=] preNFA_to_preMAUT (incr A).
proof: Proof. intros [s ? ? ?] HA. unfold incr, preNFA_to_preMAUT. simpl. replace (nat_of_num(S s)) with (nat_of_state s +1)%nat by (clear;num_lia). constructor. mx_intros i j Hi Hj. simpl. destruct_blocks; trivial; fold_regex; (case_eq (epsilonbrel (mk (S s) epsilonmap0 deltamap0 max_label0) (state_of_nat i) (state_of_nat j)); intro Hij; [apply HA in Hij; cbn in *; exfalso; num_lia | symmetry; rewrite labelling_empty; [ auto with algebra | intros a; apply not_true_eq_false; intro F; apply HA in F; simpl in *; exfalso; num_lia ]]). 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)