proposition: Lemma commute_add_var: forall n i f A, bounded A -> belong i A -> belong f A -> Algebraic.add_var (nat_of_state i) (nat_of_state f) n (preNFA_to_preMAUT A) [=0=] preNFA_to_preMAUT (add_var i f n A).
proof: Proof. intros n i f A HA Hi Hf. rewrite (psurj A) at 2. simpl. constructor. mx_intros s t Hs Ht. simpl in *. fold_regex. rewrite <- plus_assoc. apply plus_compat; trivial. fold (add_var i f n (mk (size A) (epsilonmap A) (deltamap A) (max_label A))). rewrite labelling_add_var. rewrite (@labelling_crop (Nat.max (Datatypes.S (nat_of_num n)) (max_label A))); auto with arith. setoid_rewrite eqb_eq_nat_bool. setoid_rewrite id_nat. unfold labelling. num_simpl. nat_analyse; simpl; fold_regex; try semiring_reflexivity. num_analyse; simpl; fold_regex; try semiring_reflexivity. elim n0. clear. num_simpl. apply Nat.le_max_l. 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)