The reversible LTSI of a stable family

Backward steps undo one event. The reverse LPV axioms require stability.

def ConfFamily.esRStep {L : Type u_1} (F : ConfFamily L) : F.Conf → DirLabel L → F.Conf → Prop

Reversible step: forward adds an event, backward removes one.

Equations

• F.esRStep x✝¹ (DirLabel.fwd a) x✝ = F.esStep x✝¹ a x✝
• F.esRStep x✝¹ (DirLabel.bwd a) x✝ = F.esStep x✝ a x✝¹

def ConfFamily.esRIndep {L : Type u_1} (F : ConfFamily L) : F.Conf → DirLabel L → F.Conf → DirLabel L → F.Conf → Prop

Reversible coinitial independence: same direction, distinct events.

Equations

• One or more equations did not get rendered due to their size.
• F.esRIndep x✝² (DirLabel.fwd a) x✝¹ (DirLabel.fwd b) x✝ = F.esIndep x✝² a x✝¹ b x✝
• F.esRIndep x✝² (DirLabel.fwd a) x✝¹ (DirLabel.bwd a_1) x✝ = False
• F.esRIndep x✝² (DirLabel.bwd a) x✝¹ (DirLabel.fwd a_1) x✝ = False

def ConfFamily.toRLTSI {L : Type u_1} (F : ConfFamily L) : RLTSI L

The reversible LTSI of a configuration family.

Equations

• F.toRLTSI = { State := F.Conf, init := F.empty, step := F.esRStep, indep := F.esRIndep, step_rev := ⋯ }

theorem ConfFamily.union_diff_singleton {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e : F.Event} (he : e ∈ c) : c \ {e} ∪ {e} = c

Removing and re-adding a present event leaves a configuration unchanged.

theorem ConfFamily.esRStep_bwd {L : Type u_1} {F : ConfFamily L} {c c' : F.Conf} {a : L} {e : F.Event} (hc : F.Config ↑c') (he : e ∈ ↑c) (hlbl : F.label e = a) (htgt : ↑c' = ↑c \ {e}) : F.esRStep c (DirLabel.bwd a) c'

A backward step is a forward step read the other way.

theorem ConfFamily.config_diff_pair {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} {e₁ e₂ : F.Event} (h₁ : F.Config (c \ {e₁})) (h₂ : F.Config (c \ {e₂})) (hc : F.Config c) : F.Config (c \ {e₁} ∩ (c \ {e₂}))

The closing state of two backward steps.

theorem ConfFamily.inter_diff_union {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e₁ e₂ : F.Event} (he₂ : e₂ ∈ c) (hne : e₁ ≠ e₂) : c \ {e₁} ∩ (c \ {e₂}) ∪ {e₂} = c \ {e₁}

Re-adding one of the two removed events.

theorem ConfFamily.inter_diff_union' {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e₁ e₂ : F.Event} (he₁ : e₁ ∈ c) (hne : e₁ ≠ e₂) : c \ {e₁} ∩ (c \ {e₂}) ∪ {e₁} = c \ {e₂}

Re-adding the other one.

theorem ConfFamily.toRLTSI_LPV {L : Type u_1} {F : ConfFamily L} (hF : Stable F) : F.toRLTSI.LPV

The reversible LTSI of a stable family satisfies the reverse LPV axioms.