inductive EqCheckingAbstractInterpretation.CCS.RunningExample.RunAct : Type

Actions in the running example.

• a : RunAct
• b : RunAct

@[instance_reducible]

instance EqCheckingAbstractInterpretation.CCS.RunningExample.instDecidableEqRunAct : DecidableEq RunAct

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.instDecidableEqRunAct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunAct : Repr RunAct

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunAct = { reprPrec := EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunAct.repr }

def EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunAct.repr : RunAct → ℕ → Std.Format

Equations

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

inductive EqCheckingAbstractInterpretation.CCS.RunningExample.RunName : Type

Process names in the running example.

• PA : RunName
• PB : RunName

@[instance_reducible]

instance EqCheckingAbstractInterpretation.CCS.RunningExample.instDecidableEqRunName : DecidableEq RunName

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.instDecidableEqRunName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunName : Repr RunName

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunName = { reprPrec := EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunName.repr }

def EqCheckingAbstractInterpretation.CCS.RunningExample.instReprRunName.repr : RunName → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.CCS.RunningExample.RunProc : Type

Equations

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

def EqCheckingAbstractInterpretation.CCS.RunningExample.PA : RunProc

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.PA = EqCheckingAbstractInterpretation.CCS.CCS.var EqCheckingAbstractInterpretation.CCS.RunningExample.RunName.PA

def EqCheckingAbstractInterpretation.CCS.RunningExample.PB : RunProc

Equations

• EqCheckingAbstractInterpretation.CCS.RunningExample.PB = EqCheckingAbstractInterpretation.CCS.CCS.var EqCheckingAbstractInterpretation.CCS.RunningExample.RunName.PB

def EqCheckingAbstractInterpretation.CCS.RunningExample.b0 : RunProc

Equations

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

def EqCheckingAbstractInterpretation.CCS.RunningExample.PBb0 : RunProc

Equations

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

def EqCheckingAbstractInterpretation.CCS.RunningExample.runEnv : Env RunAct RunName

PA ↦ a.PA + a.b.0, PB ↦ a.(PB + b.0).

Equations

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

def EqCheckingAbstractInterpretation.CCS.RunningExample.runNext : RunProc → RunAct → List RunProc

The finite transition table induced by runEnv.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.CCS.RunningExample.runNext x✝¹ x✝ = []

def EqCheckingAbstractInterpretation.CCS.RunningExample.runLTS : FiniteLTS RunAct RunProc

The derivative-closed finite fragment induced by runEnv.

Equations

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