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

@[instance_reducible]

instance EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS {Action✝ : Type u_1} {Name✝ : Type u_2} [DecidableEq Action✝] [DecidableEq Name✝] : DecidableEq (CCS Action✝ Name✝)

Equations

• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS = EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq

def EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq {Action✝ : Type u_1} {Name✝ : Type u_2} [DecidableEq Action✝] [DecidableEq Name✝] (x✝ x✝¹ : CCS Action✝ Name✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.prefix a a_1) (a_2.choice a_3) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.prefix a a_1) EqCheckingAbstractInterpretation.CCS.CCS.zero = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.prefix a a_1) (EqCheckingAbstractInterpretation.CCS.CCS.var a_2) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (a.choice a_1) (EqCheckingAbstractInterpretation.CCS.CCS.prefix a_2 a_3) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (a.choice a_1) EqCheckingAbstractInterpretation.CCS.CCS.zero = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (a.choice a_1) (EqCheckingAbstractInterpretation.CCS.CCS.var a_2) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq EqCheckingAbstractInterpretation.CCS.CCS.zero (EqCheckingAbstractInterpretation.CCS.CCS.prefix a a_1) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq EqCheckingAbstractInterpretation.CCS.CCS.zero (a.choice a_1) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq EqCheckingAbstractInterpretation.CCS.CCS.zero EqCheckingAbstractInterpretation.CCS.CCS.zero = isTrue ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq EqCheckingAbstractInterpretation.CCS.CCS.zero (EqCheckingAbstractInterpretation.CCS.CCS.var a) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.var a) (EqCheckingAbstractInterpretation.CCS.CCS.prefix a_1 a_2) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.var a) (a_1.choice a_2) = isFalse ⋯
• EqCheckingAbstractInterpretation.CCS.instDecidableEqCCS.decEq (EqCheckingAbstractInterpretation.CCS.CCS.var a) EqCheckingAbstractInterpretation.CCS.CCS.zero = isFalse ⋯

@[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)

@[instance_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 }

@[instance_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 }

@[instance_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 }

@[instance_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'