proposition: Lemma store_size_bound: forall s, invariant s -> (nat_of_state s%s <= power size)%nat.
proof: Proof. intros s Hs. rewrite <- (i_table_size Hs). rewrite <- cardinal_domain. apply card_pset. intros p Hp. rewrite domain_spec in Hp. rewrite id_num. destruct Hp. eapply Hs. eassumption. 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)