def EqCheckingAbstractInterpretation.Trace.alphaNonempty {Action : Type u} (S : Trace Action → Prop) : Prop

Property abstraction to non-emptiness on trace sets.

Equations

• EqCheckingAbstractInterpretation.Trace.alphaNonempty S = ∃ (tr : EqCheckingAbstractInterpretation.Trace.Trace Action), S tr

def EqCheckingAbstractInterpretation.Trace.gammaNonempty {Action : Type u} (a : Prop) : Trace Action → Prop

Property concretization from non-emptiness back to a trace set.

Equations

• EqCheckingAbstractInterpretation.Trace.gammaNonempty a x✝ = a

def EqCheckingAbstractInterpretation.Trace.alphaDiffSys {Action : Type u} {Name : Type v} (ρc : DiffSys Action Name) : CCS.CCS Action Name → CCS.ProcSet Action Name → Prop

Pointwise lifting of alphaNonempty to difference systems.

Equations

• EqCheckingAbstractInterpretation.Trace.alphaDiffSys ρc p Q = EqCheckingAbstractInterpretation.Trace.alphaNonempty (ρc p Q)

def EqCheckingAbstractInterpretation.Trace.gammaDiffSys {Action : Type u} {Name : Type v} (ρa : CCS.CCS Action Name → CCS.ProcSet Action Name → Prop) : DiffSys Action Name

Pointwise lifting of gammaNonempty to difference systems.

Equations

• EqCheckingAbstractInterpretation.Trace.gammaDiffSys ρa p Q tr = EqCheckingAbstractInterpretation.Trace.gammaNonempty (ρa p Q) tr

def EqCheckingAbstractInterpretation.Trace.DTrSharp {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρa : CCS.CCS Action Name → CCS.ProcSet Action Name → Prop) : CCS.CCS Action Name → CCS.ProcSet Action Name → Prop

Abstract transformer for the non-emptiness property, defined explicitly by cases matching the paper's @def-trace-abstract-interpretation:

• yield the marker if Q = ∅;
• otherwise propagate markers through action-successors. This coincides with α ∘ DTr ∘ γ (see DTrSharp_eq_alpha_comp_DTr_comp_gamma).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.AbsDiffSys (Action : Type u) (Name : Type v) : Type (max v u)

Abstract difference systems for the non-emptiness abstraction.

Equations

• EqCheckingAbstractInterpretation.Trace.AbsDiffSys Action Name = (EqCheckingAbstractInterpretation.CCS.CCS Action Name → EqCheckingAbstractInterpretation.CCS.ProcSet Action Name → Prop)

def EqCheckingAbstractInterpretation.Trace.lfpDTrSharp {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) : AbsDiffSys Action Name

Least fixpoint of DTrSharp, defined as intersection of all pre-fixpoints.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.AbstractDiff {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) : AbsDiffSys Action Name

Abstract trace difference from the paper, defined as lfp(DTrSharp).

Equations

• EqCheckingAbstractInterpretation.Trace.AbstractDiff ρ = EqCheckingAbstractInterpretation.Trace.lfpDTrSharp ρ

def EqCheckingAbstractInterpretation.Trace.MarkerFailsPreorder {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : Prop

Marker-based failure of trace preorder against a singleton right-hand process.

Equations

• EqCheckingAbstractInterpretation.Trace.MarkerFailsPreorder ρ p q = EqCheckingAbstractInterpretation.Trace.AbstractDiff ρ p {q}

theorem EqCheckingAbstractInterpretation.Trace.lfpDTrSharp_prefixpoint {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : DTrSharp ρ (lfpDTrSharp ρ) p Q → lfpDTrSharp ρ p Q

lfpDTrSharp is a pre-fixpoint of DTrSharp.

theorem EqCheckingAbstractInterpretation.Trace.abstractDiff_empty {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) : AbstractDiff ρ p ∅