proposition: Lemma theta_delta': forall a i, a < max_label -> i < size' -> StateSet.eq (theta (delta' d a i)) (delta_set a (theta i)).
proof: Proof. intros a i Ha Hi x. rewrite in_delta_set. unfold delta'. StateLabelMapProps.find_analyse. rename H into Hx. apply invariant_build_store in Hx as [pi Hpi Hix]. rewrite (theta_rho Hix). rewrite in_delta_set. setoid_rewrite <- (theta_rho Hpi). reflexivity. elim H. destruct (proj2 build_store_correct i a) as [di Hdi]; auto. eauto with map. 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)