proposition: Lemma invariant_initial_store: invariant initial_store.
proof: Proof. unfold initial_store. constructor; simpl; intros. revert H. StateSetMapProps.map_iff. intuition subst; try reflexivity. intros x Hx. rewrite <- H in Hx. apply (NFA.bounded_initiaux HA Hx). StateSetMapProps.find_tac; StateSetProps.setdec. exists initiaux. replace i with (state_of_nat O). auto with map. change 2%positive with (state_of_nat 1) in H. num_lia. reflexivity. revert H. StateLabelMapProps.map_iff. tauto. 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_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)