inductive EqCheckingAbstractInterpretation.CCS.CCS (Action : Type u) (Name : Type v) : Type (max u v)

CCS processes: action prefix, nondeterministic choice, deadlock 0, and recursive variables.

• prefix {Action : Type u} {Name : Type v} : Action → CCS Action Name → CCS Action Name
• choice {Action : Type u} {Name : Type v} : CCS Action Name → CCS Action Name → CCS Action Name
• zero {Action : Type u} {Name : Type v} : CCS Action Name
• var {Action : Type u} {Name : Type v} : Name → CCS Action Name

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.CCS.Env (Action : Type u) (Name : Type v) : Type (max v u)

A recursive process environment maps each name to its defining CCS term.

Equations

• EqCheckingAbstractInterpretation.CCS.Env Action Name = (Name → EqCheckingAbstractInterpretation.CCS.CCS Action Name)

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.CCS.ProcSet (Action : Type u) (Name : Type v) : Type (max v u)

Equations

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

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.CCS.instSingletonCCSProcSet {Action : Type u} {Name : Type v} : Singleton (CCS Action Name) (ProcSet Action Name)

Equations

• EqCheckingAbstractInterpretation.CCS.instSingletonCCSProcSet = { singleton := fun (q r : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => r = q }

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.CCS.instEmptyCollectionProcSet {Action : Type u} {Name : Type v} : EmptyCollection (ProcSet Action Name)

Equations

• EqCheckingAbstractInterpretation.CCS.instEmptyCollectionProcSet = { emptyCollection := fun (x : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => False }

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.CCS.instSingletonCCSForallProp {Action : Type u} {Name : Type v} : Singleton (CCS Action Name) (CCS Action Name → Prop)

Equations

• EqCheckingAbstractInterpretation.CCS.instSingletonCCSForallProp = { singleton := fun (q r : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => r = q }

@[implicit_reducible]

instance EqCheckingAbstractInterpretation.CCS.instEmptyCollectionForallCCSProp {Action : Type u} {Name : Type v} : EmptyCollection (CCS Action Name → Prop)

Equations

• EqCheckingAbstractInterpretation.CCS.instEmptyCollectionForallCCSProp = { emptyCollection := fun (x : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => False }

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

One-step labeled transition relation derived from the CCS structural rules and the recursive environment.

• prefix {Action : Type u} {Name : Type v} {ρ : Env Action Name} {a : Action} {p : CCS Action Name} : Deriv ρ (CCS.prefix a p) a p
• choice_left {Action : Type u} {Name : Type v} {ρ : Env Action Name} {p q : CCS Action Name} {a : Action} {p' : CCS Action Name} : Deriv ρ p a p' → Deriv ρ (p.choice q) a p'
• choice_right {Action : Type u} {Name : Type v} {ρ : Env Action Name} {p q : CCS Action Name} {a : Action} {q' : CCS Action Name} : Deriv ρ q a q' → Deriv ρ (p.choice q) a q'
• var {Action : Type u} {Name : Type v} {ρ : Env Action Name} {X : Name} {a : Action} {p' : CCS Action Name} : Deriv ρ (ρ X) a p' → Deriv ρ (CCS.var X) a p'

def EqCheckingAbstractInterpretation.CCS.DerivSet {Action : Type u} {Name : Type v} (ρ : Env Action Name) (p : CCS Action Name) (a : Action) : CCS Action Name → Prop

The set of a-successors of a single process p.

Equations

• EqCheckingAbstractInterpretation.CCS.DerivSet ρ p a p' = EqCheckingAbstractInterpretation.CCS.Deriv ρ p a p'

def EqCheckingAbstractInterpretation.CCS.DerivSetOf {Action : Type u} {Name : Type v} (ρ : Env Action Name) (P : CCS Action Name → Prop) (a : Action) : CCS Action Name → Prop

The lifted derivative: the set of a-successors of any process in P.

Equations

• EqCheckingAbstractInterpretation.CCS.DerivSetOf ρ P a p' = ∃ (p : EqCheckingAbstractInterpretation.CCS.CCS Action Name), P p ∧ EqCheckingAbstractInterpretation.CCS.Deriv ρ p a p'

def EqCheckingAbstractInterpretation.CCS.Enabled {Action : Type u} {Name : Type v} (ρ : Env Action Name) (p : CCS Action Name) : Action → Prop

The set of actions immediately enabled at process p.

Equations

• EqCheckingAbstractInterpretation.CCS.Enabled ρ p a = ∃ (p' : EqCheckingAbstractInterpretation.CCS.CCS Action Name), EqCheckingAbstractInterpretation.CCS.Deriv ρ p a p'