fact: Record extends (s s': Store): Prop := { e_invariant :> invariant s'; e_table: forall p i, StateSetMap.MapsTo p i s%t -> StateSetMap.MapsTo p i s'%t; e_next: s%s <= s'%s }.
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)