Least replay sets

Relative to a bounding configuration c, the least subconfiguration of c containing a log l is the union of the histories of the events of l.

def Stable.replaySet {L : Type u_1} (F : ConfFamily L) (c l : Set F.Event) : Set F.Event

The least subconfiguration of c containing l.

Equations

• Stable.replaySet F c l = ⋃ x ∈ l, Stable.hist F c x

theorem Stable.subset_replaySet {L : Type u_1} {F : ConfFamily L} {c l : Set F.Event} : l ⊆ replaySet F c l

theorem Stable.replaySet_subset {L : Type u_1} {F : ConfFamily L} {c l : Set F.Event} (hc : F.Config c) (hlc : l ⊆ c) : replaySet F c l ⊆ c

theorem Stable.replaySet_config {L : Type u_1} {F : ConfFamily L} {c l : Set F.Event} (hc : F.Config c) (hlc : l ⊆ c) (hS : Stable F) (hC : Coherent F) : F.Config (replaySet F c l)

It is a configuration: each history is one by stability, their union by coherence.

theorem Stable.replaySet_least {L : Type u_1} {F : ConfFamily L} {c l m : Set F.Event} (hm : F.Config m) (hmc : m ⊆ c) (hlm : l ⊆ m) : replaySet F c l ⊆ m

It is least among subconfigurations of c containing l.