@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.Trace (Action : Type u) : Type u

A trace is a finite sequence of actions.

Equations

• EqCheckingAbstractInterpretation.Trace.Trace Action = List Action

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.TraceSet (Action : Type u) : Type u

A trace set is a predicate on traces.

Equations

• EqCheckingAbstractInterpretation.Trace.TraceSet Action = (EqCheckingAbstractInterpretation.Trace.Trace Action → Prop)

inductive EqCheckingAbstractInterpretation.Trace.TraceSem {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) : CCS.CCS Action Name → Trace Action → Prop

• nil {Action : Type u} {Name : Type v} {ρ : CCS.Env Action Name} (p : CCS.CCS Action Name) : TraceSem ρ p []
• cons {Action : Type u} {Name : Type v} {ρ : CCS.Env Action Name} {p p' : CCS.CCS Action Name} {a : Action} {tr : Trace Action} : CCS.Deriv ρ p a p' → TraceSem ρ p' tr → TraceSem ρ p (a :: tr)

def EqCheckingAbstractInterpretation.Trace.traceSetOf {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) : TraceSet Action

Equations

• EqCheckingAbstractInterpretation.Trace.traceSetOf ρ p tr = EqCheckingAbstractInterpretation.Trace.TraceSem ρ p tr

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

Equations

• EqCheckingAbstractInterpretation.Trace.TraceDifference ρ p q tr = (EqCheckingAbstractInterpretation.Trace.traceSetOf ρ p tr ∧ ¬EqCheckingAbstractInterpretation.Trace.traceSetOf ρ q tr)

def EqCheckingAbstractInterpretation.Trace.TraceDifferenceToSet {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) : TraceSet Action

Equations

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

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

Equations

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

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

Equations

• EqCheckingAbstractInterpretation.Trace.TraceEquivalent ρ p q = (EqCheckingAbstractInterpretation.Trace.TracePreorder ρ p q ∧ EqCheckingAbstractInterpretation.Trace.TracePreorder ρ q p)

theorem EqCheckingAbstractInterpretation.Trace.tracePreorder_refl {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) : TracePreorder ρ p p

theorem EqCheckingAbstractInterpretation.Trace.tracePreorder_trans {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p₁ p₂ p₃ : CCS.CCS Action Name) (h₁₂ : TracePreorder ρ p₁ p₂) (h₂₃ : TracePreorder ρ p₂ p₃) : TracePreorder ρ p₁ p₃

theorem EqCheckingAbstractInterpretation.Trace.traceEquivalent_refl {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) : TraceEquivalent ρ p p

theorem EqCheckingAbstractInterpretation.Trace.traceEquivalent_symm {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : TraceEquivalent ρ p q → TraceEquivalent ρ q p

theorem EqCheckingAbstractInterpretation.Trace.traceEquivalent_trans {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p₁ p₂ p₃ : CCS.CCS Action Name) (h₁₂ : TraceEquivalent ρ p₁ p₂) (h₂₃ : TraceEquivalent ρ p₂ p₃) : TraceEquivalent ρ p₁ p₃

theorem EqCheckingAbstractInterpretation.Trace.tracePreorder_iff_noDifference {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : TracePreorder ρ p q ↔ ∀ (tr : Trace Action), ¬TraceDifference ρ p q tr

theorem EqCheckingAbstractInterpretation.Trace.traceDifferenceToSet_singleton {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) (tr : Trace Action) : TraceDifferenceToSet ρ p {q} tr ↔ TraceDifference ρ p q tr