Logs of a prime event structure

Choice points are minimal conflicts.

def logged {L : Type u_1} (es : PES L) (e : es.Event) : Prop

An event is logged if it is in minimal conflict with some event.

Equations

• logged es e = ∃ (e' : es.Event), es.minimalConflict e e'

def log {L : Type u_1} (es : PES L) (c : Conf es) : Set es.Event

The log of c: its events in minimal conflict with something outside c.

Equations

• log es c = {e : es.Event | e ∈ ↑c ∧ ∃ e' ∉ ↑c, es.minimalConflict e e'}

theorem Log.log_subset {L : Type u_1} (es : PES L) {c : Conf es} : log es c ⊆ ↑c

The log is contained in the configuration.

theorem Log.log_logged {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} (h : e ∈ log es c) : logged es e

Events in the log are logged.

theorem Log.log_mem_iff {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} : e ∈ log es c ↔ e ∈ ↑c ∧ ∃ e' ∉ ↑c, es.minimalConflict e e'

theorem Log.logged_iff {L : Type u_1} (es : PES L) {e : es.Event} : logged es e ↔ ∃ (e' : es.Event), es.minimalConflict e e'

theorem Log.logged_symm {L : Type u_1} (es : PES L) {e e' : es.Event} (h : es.minimalConflict e e') : logged es e'

Minimal conflict is symmetric, so its partner is logged too.

theorem Log.log_has_conflict_outside {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} (he : e ∈ log es c) : ∃ e' ∉ ↑c, es.minimalConflict e e'

@[reducible, inline]

abbrev PES.compatibleWithLog {L : Type u_1} (es : PES L) (σ : Computations es.toFamily) (l : Set es.Event) : Prop

Compatibility with a log, for the conflict relation of es.

Equations

• es.compatibleWithLog σ l = Log.compatibleWithLog es.toFamily es.conflict σ l

def PES.compatibleWithConfigLog {L : Type u_1} (es : PES L) (c : Conf es) (σ : Computations es.toFamily) : Prop

A computation compatible with the log of a configuration.

Equations

• es.compatibleWithConfigLog c σ = es.compatibleWithLog σ (log es c)

def PES.CompatibleWithConfigLog {L : Type u_1} (es : PES L) (c : Conf es) : Type

Computations compatible with the log of a configuration.

Equations

• es.CompatibleWithConfigLog c = Log.CompatibleComputations es.toFamily es.conflict (log es c)

def PES.labelLog {L : Type u_1} (es : PES L) (c : Conf es) : Set L

The label image of the log of a configuration.

Equations

• es.labelLog c = Log.labelLog es.toFamily (log es c)

theorem PES.label_mem_labelLog {L : Type u_1} (es : PES L) {c : Conf es} {e : es.Event} (h : e ∈ log es c) : es.label e ∈ es.labelLog c