Calculus of communicating systems

InductiveFinite CCS processes#✓fully proved

For a type \(A\) of actions, the finite CCS processes over \(A\) are built from the inactive process \(\mathbf{0}\) by action prefix \(a.P\) (an action \(a \in A\) followed by a process \(P\)), nondeterministic choice \(P + Q\), and parallel composition \(P \mid Q\).

inductive Process where
  | nil
  | prefix (action : Action) (continuation : Process)
  | choice (left right : Process)
  | parallel (left right : Process)
  deriving DecidableEq
Used by 17
Used byLifting relations through choice · Choice preserves strong bisimilarity in CCS with communication · Labelled transition system of CCS with communication · Transitions of a parallel composition · Prefix preserves strong bisimilarity in CCS with communication · CCS transition relation with communication · Reflexive closure of a relation on processes · Labelled transition system of finite CCS · Embedding finite CCS into CCS with static operators · Parallel composition is commutative up to strong bisimilarity · Parallel composition preserves strong bisimilarity · Parallel lift of two relations · The inactive process is a left unit for parallel composition · The inactive process is a right unit for parallel composition · Prefix preserves strong bisimilarity · Operational semantics of finite CCS with a synchronization function · Transitions of finite CCS without communication

InductiveOperational semantics of finite CCS with a synchronization function#✓fully proved

Let \(\sigma\) be a partial function that assigns to some pairs of actions \((a, b)\) an action \(\sigma(a, b)\). The transition relation \(P \xrightarrow{a} P'\) on finite CCS processes (built from prefix \(a.P\), choice \(P + Q\) and parallel composition \(P \mid Q\)) determined by \(\sigma\) is the least relation such that \(a.P \xrightarrow{a} P\); if \(P \xrightarrow{a} P'\) then \(P + Q \xrightarrow{a} P'\), \(Q + P \xrightarrow{a} P'\), \(P \mid Q \xrightarrow{a} P' \mid Q\) and \(Q \mid P \xrightarrow{a} Q \mid P'\); and if \(P \xrightarrow{a} P'\), \(Q \xrightarrow{b} Q'\) and \(\sigma(a, b) = c\), then \(P \mid Q \xrightarrow{c} P' \mid Q'\).

Cslib.CCS.Process.RawStep · 22 lines 
inductive RawStep (synchronize : Action → Action → Option Action) :
    Process Action → Action → Process Action → Prop
  | prefix (action : Action) (continuation : Process Action) :
      RawStep synchronize (.prefix action continuation) action continuation
  | choiceLeft {left right next : Process Action} {action : Action}
      (step : RawStep synchronize left action next) :
      RawStep synchronize (.choice left right) action next
  | choiceRight {left right next : Process Action} {action : Action}
      (step : RawStep synchronize right action next) :
      RawStep synchronize (.choice left right) action next
  | parallelLeft {left right next : Process Action} {action : Action}
      (step : RawStep synchronize left action next) :
      RawStep synchronize (.parallel left right) action (.parallel next right)
  | parallelRight {left right next : Process Action} {action : Action}
      (step : RawStep synchronize right action next) :
      RawStep synchronize (.parallel left right) action (.parallel left next)
  | communicate {left right left' right' : Process Action}
      {leftAction rightAction result : Action}
      (leftStep : RawStep synchronize left leftAction left')
      (rightStep : RawStep synchronize right rightAction right')
      (syncs : synchronize leftAction rightAction = some result) :
      RawStep synchronize (.parallel left right) result (.parallel left' right')
Uses 1 · Used by 9
Statement usesFinite CCS processes
Used byChoice preserves strong bisimilarity in CCS with communication · Transitions of a parallel composition · Prefix preserves strong bisimilarity in CCS with communication · CCS transition relation with communication · Parallel composition is commutative up to strong bisimilarity · Parallel composition preserves strong bisimilarity · The inactive process is a left unit for parallel composition · Prefix preserves strong bisimilarity · Transitions of finite CCS without communication

AbbreviationTransitions of finite CCS without communication#✓fully proved

The transition relation \(P \xrightarrow{a} P'\) on finite CCS processes is the operational semantics of finite CCS whose synchronization function is undefined on every pair of actions. Thus prefix and choice move as usual, and a parallel composition \(P \mid Q\) moves only by letting one of \(P\) and \(Q\) move; there are no communication steps.

abbrev Step : Process Action → Action → Process Action → Prop :=
  RawStep (fun _ _ => none)
Uses 2 · Used by 1
Statement usesFinite CCS processes · Operational semantics of finite CCS with a synchronization function
Used byLabelled transition system of finite CCS

DefinitionLabelled transition system of finite CCS#✓fully proved

The labelled transition system whose states are the finite CCS processes, whose labels are the actions, and whose transitions \(P \xrightarrow{a} P'\) are those of the communication-free operational semantics of finite CCS.

def lts : Cslib.LTS (Process Action) Action := ⟨Step⟩
Uses 2 · Used by 1
Statement usesFinite CCS processes · Transitions of finite CCS without communication
Used byPrefix preserves strong bisimilarity

InductiveLifting relations through choice#✓fully proved

Given relations \(R\) and \(S\) on finite CCS processes, write \(P_1 + P_2\) for the nondeterministic choice of \(P_1\) and \(P_2\). The choice lift of \(R\) and \(S\) relates \(P\) to \(Q\) exactly when \(R(P, Q)\) holds, or \(S(P, Q)\) holds, or \(P = P_1 + P_2\) and \(Q = Q_1 + Q_2\) with \(R(P_1, Q_1)\) and \(S(P_2, Q_2)\).

inductive ChoiceLift (leftRel rightRel : Process Action → Process Action → Prop) :
    Process Action → Process Action → Prop
  | left {left₁ left₂} (relation : leftRel left₁ left₂) :
      ChoiceLift leftRel rightRel left₁ left₂
  | right {right₁ right₂} (relation : rightRel right₁ right₂) :
      ChoiceLift leftRel rightRel right₁ right₂
  | choice {left₁ left₂ right₁ right₂}
      (left : leftRel left₁ left₂) (right : rightRel right₁ right₂) :
      ChoiceLift leftRel rightRel (.choice left₁ right₁) (.choice left₂ right₂)
Uses 1
Statement usesFinite CCS processes

TheoremPrefix preserves strong bisimilarity#✓fully proved

For every action \(a\) and all finite CCS processes \(P\) and \(Q\), if \(P\) and \(Q\) are strongly bisimilar in the labelled transition system of finite CCS, then the prefixed processes \(a.P\) and \(a.Q\) are strongly bisimilar there as well.

theorem prefix_congr (action : Action) {left right : Process Action}
    (hcontinuation : (lts (Action := Action)).HomBisimilarity left right) :
    (lts (Action := Action)).HomBisimilarity (.prefix action left) (.prefix action right)
Uses 3
Statement usesFinite CCS processes · Labelled transition system of finite CCS
Proof usesOperational semantics of finite CCS with a synchronization function

DefinitionReflexive closure of a relation on processes#✓fully proved

Given a relation \(E\) on finite CCS processes, its equation closure relates \(P\) to \(Q\) exactly when \(P = Q\) or \(E(P, Q)\); that is, it is the reflexive closure of \(E\).

It is used to prove the algebraic laws of nondeterministic choice up to strong bisimilarity.

def EquationClosure (equation : Process Action → Process Action → Prop) :
    Process Action → Process Action → Prop :=
  fun left right => left = right ∨ equation left right
Uses 1 · Used by 2
Statement usesFinite CCS processes
Used byParallel composition is commutative up to strong bisimilarity · The inactive process is a left unit for parallel composition

InductiveCCS labels#✓fully proved

For a set of names, a CCS label is either the silent action \(\tau\), the input on a name \(a\), or the output on a name \(a\).

inductive Label (Name : Type*) where
  | tau
  | input (name : Name)
  | output (name : Name)
  deriving DecidableEq
Used by 82
Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · Acknowledgement channel of the alternating-bit protocol with data · Transitions of the data-free one-place buffer · Transitions of the one-place buffer of bits · Alternating-bit configuration transitions · Transitions of the alternating-bit protocol with data · Alternating-bit data channel transitions · Data-channel transitions of the alternating-bit protocol with data · Alternating-bit transition system · Transition system of the alternating-bit protocol with data · Alternating-bit receiver transitions · Receiver transitions of the alternating-bit protocol with data · Alternating-bit sender transitions · Sender transitions of the alternating-bit protocol with data · Recursive specification of the data-free alternating-bit protocol · Recursive specification of the alternating-bit protocol with data · Transitions of the lossy acknowledgement channel · The silent closure of the buffer is trivial · Transitions of the two-place buffer · Visible weak steps of the buffer · Transitions of go-back-N configurations · Transitions of the go-back-N data channel · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Transitions of lossy go-back-N configurations · Lossy acknowledgements break the buffer specification · Receiver transitions of lossy go-back-N · Configuration transitions are process transitions in lossy go-back-N · Labelled transition system of go-back-N · Receiver transitions of go-back-N · Sender transitions of go-back-N · Recursive CCS specification of go-back-N · The stuck lossy go-back-N configuration refuses new messages · Actions permitted by a restriction · Choice preserves strong bisimilarity in CCS with communication · Labelled transition system of CCS with communication · Transitions of a parallel composition · Prefix preserves strong bisimilarity in CCS with communication · CCS transition relation with communication · Complementary labels · Constant occurrences of a process · Guardedness under a prefix flag · Renaming constants preserves guardedness · Every process is guarded beneath a prefix · Labelled transition system of a recursive specification · Transition system of CCS with restriction and relabelling · Renaming process constants · Embedding finite CCS into CCS with static operators · Parallel composition is commutative up to strong bisimilarity · Parallel composition preserves strong bisimilarity · Parallel lift of two relations · The inactive process is a left unit for parallel composition · The inactive process is a right unit for parallel composition · Recursive CCS processes · Relabelling an action · Relabelling preserves complementary actions · Relabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity · Static CCS processes · Transitions of recursive CCS · Transitions of static CCS · Synchronization of CCS labels · Visible labels as CCS labels · Boolean restriction test · Backward certificate check · Weak-bisimulation certificate check · Constants listing their transitions realize them · Forward certificate check · Code-level parallel composition · Parallel composition preserves realization · Realization of a code-level transition system · Code-level restriction · Restriction preserves realization · Direct check of the root condition · Certificate checks give rooted observation congruence · Transitions of a sum of prefixes · Sum of prefixes · Certificate checks give weak bisimilarity

DefinitionComplementary labels#✓fully proved

Two CCS labels are complementary when one is the input on a name \(a\) and the other is the output on the same name \(a\), in either order. No other pair of labels is complementary; in particular the silent label \(\tau\) has no complement.

def Complementary : Label Name → Label Name → Prop
  | .input left, .output right => left = right
  | .output left, .input right => left = right
  | _, _ => False
Uses 1 · Used by 11
Statement usesCCS labels
Used byTransitions of a parallel composition · Parallel composition is commutative up to strong bisimilarity · Relabelling preserves complementary actions · Relabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity · Transitions of recursive CCS · Transitions of static CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Transitions of a sum of prefixes

DefinitionSynchronization of CCS labels#✓fully proved

Let the names form a type with decidable equality. For labels \(a\) and \(b\), the synchronization of \(a\) with \(b\) is the silent action \(\tau\) when \(a\) is the input on a name \(n\) and \(b\) is the output on the same name \(n\), or when \(a\) is the output on \(n\) and \(b\) is the input on \(n\). For every other pair of labels, including any pair involving \(\tau\), there is no result.

This partial function supplies the communication rule of the CCS operational semantics.

def synchronize [DecidableEq Name] : Label Name → Label Name → Option (Label Name)
  | .input left, .output right => if left = right then some .tau else none
  | .output left, .input right => if left = right then some .tau else none
  | _, _ => none
Uses 1 · Used by 9
Statement usesCCS labels
Used byChoice preserves strong bisimilarity in CCS with communication · Transitions of a parallel composition · Prefix preserves strong bisimilarity in CCS with communication · CCS transition relation with communication · Parallel composition is commutative up to strong bisimilarity · Parallel composition preserves strong bisimilarity · The inactive process is a left unit for parallel composition · Code-level parallel composition · Parallel composition preserves realization

AbbreviationCCS transition relation with communication#✓fully proved

The transition relation on CCS processes with labels over a set of names given by the raw step relation for the synchronization function under which an input and an output on the same name, in either order, synchronize to the silent label \(\tau\), and no other pair of labels synchronizes.

abbrev CommunicationStep : Process (Label Name) → Label Name → Process (Label Name) → Prop :=
  RawStep Label.synchronize
Uses 4 · Used by 5
Statement usesCCS labels · Synchronization of CCS labels · Finite CCS processes · Operational semantics of finite CCS with a synchronization function
Used byChoice preserves strong bisimilarity in CCS with communication · Labelled transition system of CCS with communication · Transitions of a parallel composition · Parallel composition is commutative up to strong bisimilarity · The inactive process is a left unit for parallel composition

DefinitionLabelled transition system of CCS with communication#✓fully proved

The labelled transition system whose states are CCS processes with labels over a set of names, whose labels are CCS labels over those names, and whose transition relation is the CCS transition relation with communication.

def communicationLTS : Cslib.LTS (Process (Label Name)) (Label Name) :=
  ⟨CommunicationStep⟩
Uses 3 · Used by 6
Statement usesCCS labels · Finite CCS processes · CCS transition relation with communication
Used byChoice preserves strong bisimilarity in CCS with communication · Prefix preserves strong bisimilarity in CCS with communication · Parallel composition is commutative up to strong bisimilarity · Parallel composition preserves strong bisimilarity · The inactive process is a left unit for parallel composition · The inactive process is a right unit for parallel composition

TheoremTransitions of a parallel composition#✓fully proved

For CCS processes \(P\), \(Q\), \(R\) and a CCS label \(a\), the parallel composition \(P \mid Q\) has a transition labelled \(a\) to \(R\) in the CCS transition relation with communication if and only if one of the following holds: \(P\) has a transition labelled \(a\) to some \(P'\) and \(R = P' \mid Q\); or \(Q\) has a transition labelled \(a\) to some \(Q'\) and \(R = P \mid Q'\); or \(a = \tau\) and there are processes \(P'\), \(Q'\) and complementary labels \(b\), \(c\) such that \(P\) has a transition labelled \(b\) to \(P'\), \(Q\) has a transition labelled \(c\) to \(Q'\), and \(R = P' \mid Q'\).

theorem communication_parallel_step_iff {left right next : Process (Label Name)}
    {label : Label Name} :
    CommunicationStep (.parallel left right) label next ↔
      (∃ left', CommunicationStep left label left' ∧ next = .parallel left' right) ∨
      (∃ right', CommunicationStep right label right' ∧ next = .parallel left right') ∨
      (label = .tau ∧ ∃ left' right' leftLabel rightLabel,
        CommunicationStep left leftLabel left' ∧ CommunicationStep right rightLabel right' ∧
        leftLabel.Complementary rightLabel ∧ next = .parallel left' right')
Uses 6
Statement usesCCS labels · Complementary labels · Finite CCS processes · CCS transition relation with communication
Proof usesSynchronization of CCS labels · Operational semantics of finite CCS with a synchronization function

InductiveParallel lift of two relations#✓fully proved

Given two relations \(R\) and \(S\) on CCS processes with labels over a set of names, their parallel lift relates a process \(U\) to a process \(V\) exactly when \(R\) relates \(U\) to \(V\), or \(S\) relates \(U\) to \(V\), or \(U = P_1 \mid Q_1\) and \(V = P_2 \mid Q_2\) where \(R\) relates \(P_1\) to \(P_2\) and \(S\) relates \(Q_1\) to \(Q_2\).

inductive ParallelLift
    (leftRel rightRel : Process (Label Name) → Process (Label Name) → Prop) :
    Process (Label Name) → Process (Label Name) → Prop
  | left {left₁ left₂} (relation : leftRel left₁ left₂) :
      ParallelLift leftRel rightRel left₁ left₂
  | right {right₁ right₂} (relation : rightRel right₁ right₂) :
      ParallelLift leftRel rightRel right₁ right₂
  | parallel {left₁ left₂ right₁ right₂}
      (left : leftRel left₁ left₂) (right : rightRel right₁ right₂) :
      ParallelLift leftRel rightRel (.parallel left₁ right₁) (.parallel left₂ right₂)
Uses 2 · Used by 1
Statement usesCCS labels · Finite CCS processes
Used byParallel composition preserves strong bisimilarity

TheoremParallel composition preserves strong bisimilarity#✓fully proved

For CCS processes \(P_1\), \(P_2\), \(Q_1\), \(Q_2\) with labels over a set of names: if \(P_1\) and \(P_2\) are strongly bisimilar and \(Q_1\) and \(Q_2\) are strongly bisimilar in the labelled transition system of CCS with communication, then the parallel compositions \(P_1 \mid Q_1\) and \(P_2 \mid Q_2\) are strongly bisimilar there.

theorem parallel_congr {left₁ left₂ right₁ right₂ : Process (Label Name)}
    (hleft : (communicationLTS (Name := Name)).HomBisimilarity left₁ left₂)
    (hright : (communicationLTS (Name := Name)).HomBisimilarity right₁ right₂) :
    (communicationLTS (Name := Name)).HomBisimilarity
      (.parallel left₁ right₁) (.parallel left₂ right₂)
Uses 6
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesSynchronization of CCS labels · Parallel lift of two relations · Operational semantics of finite CCS with a synchronization function

TheoremPrefix preserves strong bisimilarity in CCS with communication#✓fully proved

For every CCS label \(a\) and all CCS processes \(P\) and \(Q\): if \(P\) and \(Q\) are strongly bisimilar in the labelled transition system of CCS with communication, then so are the prefixed processes \(a.P\) and \(a.Q\).

theorem communication_prefix_congr (label : Label Name)
    {left right : Process (Label Name)}
    (hcontinuation : (communicationLTS (Name := Name)).HomBisimilarity left right) :
    (communicationLTS (Name := Name)).HomBisimilarity
      (.prefix label left) (.prefix label right)
Uses 5
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesSynchronization of CCS labels · Operational semantics of finite CCS with a synchronization function

TheoremChoice preserves strong bisimilarity in CCS with communication#✓fully proved

For CCS processes \(P_1\), \(P_2\), \(Q_1\), \(Q_2\) with labels over a set of names: if \(P_1\) and \(P_2\) are strongly bisimilar and \(Q_1\) and \(Q_2\) are strongly bisimilar in the labelled transition system of CCS with communication, then the choices \(P_1 + Q_1\) and \(P_2 + Q_2\) are strongly bisimilar there.

theorem communication_choice_congr {left₁ left₂ right₁ right₂ : Process (Label Name)}
    (hleft : (communicationLTS (Name := Name)).HomBisimilarity left₁ left₂)
    (hright : (communicationLTS (Name := Name)).HomBisimilarity right₁ right₂) :
    (communicationLTS (Name := Name)).HomBisimilarity
      (.choice left₁ right₁) (.choice left₂ right₂)
Uses 6
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesSynchronization of CCS labels · CCS transition relation with communication · Operational semantics of finite CCS with a synchronization function

TheoremParallel composition is commutative up to strong bisimilarity#✓fully proved

For all CCS processes \(P\) and \(Q\) with labels over a set of names, \(P \mid Q\) and \(Q \mid P\) are strongly bisimilar in the labelled transition system of CCS with communication.

theorem parallel_comm (left right : Process (Label Name)) :
    (communicationLTS (Name := Name)).HomBisimilarity
      (.parallel left right) (.parallel right left)
Uses 8 · Used by 1
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesComplementary labels · Synchronization of CCS labels · CCS transition relation with communication · Reflexive closure of a relation on processes · Operational semantics of finite CCS with a synchronization function
Used byThe inactive process is a right unit for parallel composition

TheoremThe inactive process is a left unit for parallel composition#✓fully proved

Let the names form a type with decidable equality. For every CCS process \(P\) over input, output and silent labels on these names, the parallel composition \(0 \mid P\) of the inactive process \(0\) with \(P\) is strongly bisimilar to \(P\) in the communication labelled transition system.

theorem parallel_nil_left (process : Process (Label Name)) :
    (communicationLTS (Name := Name)).HomBisimilarity (.parallel .nil process) process
Uses 7 · Used by 1
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesSynchronization of CCS labels · CCS transition relation with communication · Reflexive closure of a relation on processes · Operational semantics of finite CCS with a synchronization function
Used byThe inactive process is a right unit for parallel composition

TheoremThe inactive process is a right unit for parallel composition#✓fully proved

Let the names form a type with decidable equality. For every CCS process \(P\) over input, output and silent labels on these names, the parallel composition \(P \mid 0\) of \(P\) with the inactive process \(0\) is strongly bisimilar to \(P\) in the communication labelled transition system.

theorem parallel_nil_right (process : Process (Label Name)) :
    (communicationLTS (Name := Name)).HomBisimilarity (.parallel process .nil) process
Uses 5
Statement usesCCS labels · Finite CCS processes · Labelled transition system of CCS with communication
Proof usesParallel composition is commutative up to strong bisimilarity · The inactive process is a left unit for parallel composition

InductiveVisible CCS label#✓fully proved

A visible CCS label, excluding the silent action.

inductive VisibleLabel (Name : Type*) where
  | input (name : Name)
  | output (name : Name)
  deriving DecidableEq
Used by 5
Used byApplying a relabelling to a channel name · Complement of a visible label · Relabelling preserves complementary actions · Relabelling · Visible labels as CCS labels

DefinitionComplement of a visible label#✓fully proved

The complement of the input label on a channel \(a\) is the output label on \(a\), and the complement of the output label on \(a\) is the input label on \(a\).

def complement : VisibleLabel Name → VisibleLabel Name
  | .input name => .output name
  | .output name => .input name
Uses 1 · Used by 2
Statement usesVisible CCS label
Used byRelabelling an action · Relabelling preserves complementary actions

DefinitionVisible labels as CCS labels#✓fully proved

The inclusion of visible labels into CCS labels sends the input on a channel \(a\) to the input on \(a\), and the output on \(a\) to the output on \(a\).

def toLabel : VisibleLabel Name → Label Name
  | .input name => .input name
  | .output name => .output name
Uses 2 · Used by 2
Statement usesCCS labels · Visible CCS label
Used byRelabelling an action · Relabelling preserves complementary actions

StructureRelabelling#✓fully proved

A finite CCS relabelling over channel names is a finite list of entries \((a, \ell)\), each pairing a channel name \(a\) with a visible label \(\ell\), that is, an input or an output on some channel. The entry \((a, \ell)\) gives \(\ell\) as the image of the input on \(a\); the image of the output on \(a\) is then the complement of \(\ell\). The first entry with name \(a\) is used, and a name occurring in no entry is mapped to itself.

structure Relabelling (Name : Type*) where
  entries : List (Name × VisibleLabel Name)
  deriving DecidableEq
Uses 1 · Used by 19
Statement usesVisible CCS label
Used byApplying a relabelling to a channel name · Constant occurrences of a process · Guardedness under a prefix flag · Renaming constants preserves guardedness · Every process is guarded beneath a prefix · Renaming process constants · Recursive CCS processes · Relabelling an action · Relabelling preserves complementary actions · Relabelling preserves strong bisimilarity · Closure of a relation under one relabelling · Restriction preserves strong bisimilarity · Static CCS processes · Transitions of recursive CCS · Transitions of static CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Transitions of a sum of prefixes

DefinitionApplying a relabelling to a channel name#✓fully proved

Let \(f\) be a finite relabelling whose table lists the entries \((a_1, \ell_1), \dots, (a_k, \ell_k)\), where each \(a_i\) is a channel name and each \(\ell_i\) a visible label. The image of a channel name \(a\) under \(f\) is \(\ell_i\) for the first index \(i\) with \(a_i = a\), and the input label on \(a\) when no entry has name \(a\).

def apply (rename : Relabelling Name) (name : Name) : VisibleLabel Name :=
  applyEntries rename.entries name
Uses 2 · Used by 2
Statement usesRelabelling · Visible CCS label
Used byRelabelling an action · Relabelling preserves complementary actions

InductiveStatic CCS processes#✓fully proved

Finite CCS processes with the static operators, over a type of channel names, are built from the inactive process \(0\) by the prefix \(\alpha.P\) of a CCS action \(\alpha\) (silent, an input or an output) and a process \(P\), the choice \(P + Q\), the parallel composition \(P \mid Q\), the restriction \(P \setminus L\) of \(P\) by a finite list \(L\) of names, and the relabelling \(P[f]\) of \(P\) by a finite relabelling \(f\).

Unlike function-valued operators, finite lists and tables preserve decidable equality of processes and cannot express relabellings that alter the silent action \(\tau\) or fail to preserve complementary visible actions.

inductive StaticProcess (Name : Type*) where
  | nil
  | prefix (action : Label Name) (continuation : StaticProcess Name)
  | choice (left right : StaticProcess Name)
  | parallel (left right : StaticProcess Name)
  | restriction (blocked : List Name) (process : StaticProcess Name)
  | relabelling (rename : Relabelling Name) (process : StaticProcess Name)
  deriving DecidableEq
Uses 2 · Used by 7
Statement usesCCS labels · Relabelling
Used byTransition system of CCS with restriction and relabelling · Embedding finite CCS into CCS with static operators · Relabelling preserves strong bisimilarity · Closure of a relation under one relabelling · Restriction preserves strong bisimilarity · Lifting a relation through a restriction · Transitions of static CCS

DefinitionEmbedding finite CCS into CCS with static operators#✓fully proved

Each finite CCS process over CCS labels is sent to the process with static operators of the same shape: the inactive process goes to the inactive process, the prefix of an action \(\alpha\) to a process \(P\) goes to the prefix of \(\alpha\) to the image of \(P\), and a choice or a parallel composition of \(P\) and \(Q\) goes to the choice or the parallel composition of the images of \(P\) and \(Q\).

def ofProcess : Process (Label Name) → StaticProcess Name
  | .nil => .nil
  | .prefix action continuation => .prefix action (ofProcess continuation)
  | .choice left right => .choice (ofProcess left) (ofProcess right)
  | .parallel left right => .parallel (ofProcess left) (ofProcess right)
Uses 3
Statement usesCCS labels · Finite CCS processes · Static CCS processes

DefinitionRelabelling an action#✓fully proved

For a relabelling \(f\), the silent action \(\tau\) is relabelled to \(\tau\), an input on a channel \(a\) is relabelled to the image of \(a\) under \(f\), and an output on \(a\) is relabelled to the complement of the image of \(a\) under \(f\), each viewed as a CCS label.

def relabelAction (rename : Relabelling Name) : Label Name → Label Name
  | .tau => .tau
  | .input name => (rename.apply name).toLabel
  | .output name => (rename.apply name).complement.toLabel
Uses 5 · Used by 9
Statement usesCCS labels · Relabelling · Applying a relabelling to a channel name · Complement of a visible label · Visible labels as CCS labels
Used byRelabelling preserves complementary actions · Relabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity · Transitions of recursive CCS · Transitions of static CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Transitions of a sum of prefixes

TheoremRelabelling preserves complementary actions#✓fully proved

For every relabelling \(f\) and all CCS labels \(\alpha\) and \(\beta\), if \(\alpha\) and \(\beta\) are complementary, then the actions obtained by relabelling \(\alpha\) and \(\beta\) with \(f\) are complementary.

theorem relabelAction_complementary {left right : Label Name}
    (h : left.Complementary right) (rename : Relabelling Name) :
    (relabelAction rename left).Complementary (relabelAction rename right)
Uses 8
Statement usesCCS labels · Complementary labels · Relabelling · Relabelling an action
Proof usesApplying a relabelling to a channel name · Visible CCS label · Complement of a visible label · Visible labels as CCS labels

DefinitionActions permitted by a restriction#✓fully proved

Given a finite list \(L\) of blocked channel names, the silent action \(\tau\) is always permitted, and an input or an output on a channel \(a\) is permitted exactly when \(a \notin L\).

def Allowed (blocked : List Name) : Label Name → Prop
  | .tau => True
  | .input name => name ∉ blocked
  | .output name => name ∉ blocked
Uses 1 · Used by 8
Statement usesCCS labels
Used byRelabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity · Transitions of recursive CCS · Transitions of static CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Transitions of a sum of prefixes

InductiveTransitions of static CCS#✓fully proved

The labelled transition relation \(P \xrightarrow{\alpha} P'\) on static CCS processes, with actions \(\alpha\) the CCS labels (silent \(\tau\), inputs and outputs), is the least relation closed under the following rules, where \(\alpha.P\) is the prefix, \(P + Q\) the choice, \(P \mid Q\) the parallel composition, \(P \setminus L\) the restriction of \(P\) by a finite list \(L\) of channel names, and \(P[f]\) the relabelling of \(P\) by a finite relabelling \(f\). The prefix has the transition \(\alpha.P \xrightarrow{\alpha} P\). If \(P \xrightarrow{\alpha} P'\), then \(P + Q \xrightarrow{\alpha} P'\), \(Q + P \xrightarrow{\alpha} P'\), \(P \mid Q \xrightarrow{\alpha} P' \mid Q\) and \(Q \mid P \xrightarrow{\alpha} Q \mid P'\). If \(P \xrightarrow{\alpha} P'\) and \(Q \xrightarrow{\beta} Q'\) where \(\alpha\) and \(\beta\) are complementary (an input and an output on the same channel), then \(P \mid Q \xrightarrow{\tau} P' \mid Q'\). If \(P \xrightarrow{\alpha} P'\) and \(\alpha\) is \(\tau\) or its channel is not in \(L\), then \(P \setminus L \xrightarrow{\alpha} P' \setminus L\). If \(P \xrightarrow{\alpha} P'\), then \(P[f] \xrightarrow{f(\alpha)} P'[f]\), where \(f(\tau) = \tau\), an input on a channel \(a\) is sent to the visible label \(f(a)\) that \(f\) assigns to \(a\), and an output on \(a\) is sent to the complement of \(f(a)\).

Cslib.CCS.StaticProcess.Step · 20 lines 
inductive Step : StaticProcess Name → Label Name → StaticProcess Name → Prop
  | prefix (action) (continuation) : Step (.prefix action continuation) action continuation
  | choiceLeft {left right next action} (step : Step left action next) :
      Step (.choice left right) action next
  | choiceRight {left right next action} (step : Step right action next) :
      Step (.choice left right) action next
  | parallelLeft {left right next action} (step : Step left action next) :
      Step (.parallel left right) action (.parallel next right)
  | parallelRight {left right next action} (step : Step right action next) :
      Step (.parallel left right) action (.parallel left next)
  | communicate {left right left' right' leftAction rightAction}
      (leftStep : Step left leftAction left') (rightStep : Step right rightAction right')
      (complementary : leftAction.Complementary rightAction) :
      Step (.parallel left right) .tau (.parallel left' right')
  | restrict {blocked process next action}
      (step : Step process action next) (allowed : Allowed blocked action) :
      Step (.restriction blocked process) action (.restriction blocked next)
  | relabel {rename process next action} (step : Step process action next) :
      Step (.relabelling rename process) (relabelAction rename action)
        (.relabelling rename next)
Uses 6 · Used by 3
Statement usesCCS labels · Complementary labels · Relabelling · Static CCS processes · Actions permitted by a restriction · Relabelling an action
Used byTransition system of CCS with restriction and relabelling · Relabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity

DefinitionTransition system of CCS with restriction and relabelling#✓fully proved

The labelled transition system of finite CCS with static operators has the finite CCS processes with restriction and relabelling as states and the CCS labels as labels, and its transitions are the steps of the structural operational semantics of these processes.

def lts : Cslib.LTS (StaticProcess Name) (Label Name) := ⟨Step⟩
Uses 3 · Used by 2
Statement usesCCS labels · Static CCS processes · Transitions of static CCS
Used byRelabelling preserves strong bisimilarity · Restriction preserves strong bisimilarity

InductiveLifting a relation through a restriction#✓fully proved

Given a finite list \(L\) of channel names and a relation \(R\) on static CCS processes, the lifted relation relates \(P\) to \(Q\) exactly when either \(R\) relates \(P\) to \(Q\), or \(P = P' \setminus L\) and \(Q = Q' \setminus L\) for some processes \(P'\) and \(Q'\) that \(R\) relates.

inductive RestrictionLift (blocked : List Name)
    (relation : StaticProcess Name → StaticProcess Name → Prop) :
    StaticProcess Name → StaticProcess Name → Prop
  | base {left right} (related : relation left right) : RestrictionLift blocked relation left right
  | restriction {left right} (related : relation left right) :
      RestrictionLift blocked relation (.restriction blocked left) (.restriction blocked right)
Uses 1 · Used by 1
Statement usesStatic CCS processes
Used byRestriction preserves strong bisimilarity

TheoremRestriction preserves strong bisimilarity#✓fully proved

For every finite list \(L\) of channel names and all static CCS processes \(P\) and \(Q\), if \(P\) and \(Q\) are strongly bisimilar in the labelled transition system of finite CCS with static operators, then so are the restricted processes \(P \setminus L\) and \(Q \setminus L\).

theorem restriction_congr (blocked : List Name) {left right : StaticProcess Name}
    (h : lts.HomBisimilarity left right) :
    lts.HomBisimilarity (.restriction blocked left) (.restriction blocked right)
Uses 9
Statement usesCCS labels · Static CCS processes · Transition system of CCS with restriction and relabelling
Proof usesComplementary labels · Relabelling · Actions permitted by a restriction · Lifting a relation through a restriction · Transitions of static CCS · Relabelling an action

InductiveClosure of a relation under one relabelling#✓fully proved

Given a relabelling \(f\) and a relation \(R\) on finite CCS processes with static operators, the lifted relation is the least relation that relates \(P\) to \(Q\) and relates the relabelling of \(P\) by \(f\) to the relabelling of \(Q\) by \(f\) whenever \(R\) relates \(P\) to \(Q\).

inductive RelabellingLift (rename : Relabelling Name)
    (relation : StaticProcess Name → StaticProcess Name → Prop) :
    StaticProcess Name → StaticProcess Name → Prop
  | base {left right} (related : relation left right) : RelabellingLift rename relation left right
  | relabelling {left right} (related : relation left right) :
      RelabellingLift rename relation (.relabelling rename left) (.relabelling rename right)
Uses 2 · Used by 1
Statement usesRelabelling · Static CCS processes
Used byRelabelling preserves strong bisimilarity

TheoremRelabelling preserves strong bisimilarity#✓fully proved

For every relabelling \(f\) and all finite CCS processes \(P\) and \(Q\) with static operators, if \(P\) and \(Q\) are strongly bisimilar in the labelled transition system of finite CCS with static operators, then the relabellings of \(P\) and of \(Q\) by \(f\) are strongly bisimilar there.

theorem relabelling_congr (rename : Relabelling Name) {left right : StaticProcess Name}
    (h : lts.HomBisimilarity left right) :
    lts.HomBisimilarity (.relabelling rename left) (.relabelling rename right)
Uses 9
Statement usesCCS labels · Relabelling · Static CCS processes · Transition system of CCS with restriction and relabelling
Proof usesComplementary labels · Actions permitted by a restriction · Closure of a relation under one relabelling · Transitions of static CCS · Relabelling an action

InductiveRecursive CCS processes#✓fully proved

Given a set of names and a set of process constants, the recursive CCS processes are generated by the following constructors: the inactive process \(\mathbf{0}\); a process constant \(A\); a prefix \(\alpha.P\) for a CCS label \(\alpha\) and a process \(P\); a choice \(P + Q\); a parallel composition \(P \mid Q\); a restriction \(P \setminus L\) for a finite list \(L\) of names; and a relabelling \(P[f]\) for a CCS relabelling \(f\).

inductive Process (Name Constant : Type*) where
  | nil
  | constant (name : Constant)
  | prefix (action : Label Name) (continuation : Process Name Constant)
  | choice (left right : Process Name Constant)
  | parallel (left right : Process Name Constant)
  | restriction (blocked : List Name) (process : Process Name Constant)
  | relabelling (rename : Relabelling Name) (process : Process Name Constant)
  deriving DecidableEq
Uses 2 · Used by 49
Statement usesCCS labels · Relabelling
Used byThe data-free alternating-bit protocol · The alternating-bit protocol with data · The alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · The data-free one-place buffer · The empty one-place buffer of bits · The data-free one-place buffer in a given state · The one-place buffer of bits with given content · Alternating-bit transition system · Transition system of the alternating-bit protocol with data · Recursive specification of the data-free alternating-bit protocol · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol in a configuration · The alternating-bit protocol with data in a configuration · The empty two-place buffer · The two-place buffer process · The silent closure of the buffer is trivial · Visible weak steps of the buffer · The go-back-N protocol · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Go-back-N with a lossy acknowledgement channel · Lossy acknowledgements break the buffer specification · Configuration transitions are process transitions in lossy go-back-N · The lossy go-back-N process in a configuration · Labelled transition system of go-back-N · Recursive CCS specification of go-back-N · The stuck lossy go-back-N configuration refuses new messages · Go-back-N protocol process in a configuration · Constant occurrences of a process · Constants of a process · Guarded process · Guardedness under a prefix flag · Renaming constants preserves guardedness · Every process is guarded beneath a prefix · Labelled transition system of a recursive specification · Renaming process constants · Recursive CCS specification · Transitions of recursive CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Realization of a code-level transition system · Restriction preserves realization · Certificate checks give rooted observation congruence · Transitions of a sum of prefixes · Sum of prefixes · Certificate checks give weak bisimilarity

AbbreviationRecursive CCS specification#✓fully proved

Given a type of channel names and a type of process constants, a recursive specification assigns to each process constant \(A\) a defining body: a CCS process expression over those names, which may itself mention process constants (including \(A\)).

abbrev Specification (Name Constant : Type*) := Constant → Process Name Constant
Uses 1 · Used by 13
Statement usesRecursive CCS processes
Used byRecursive specification of the data-free alternating-bit protocol · Recursive specification of the alternating-bit protocol with data · Recursive CCS specification of go-back-N · Guarded recursive specification · Labelled transition system of a recursive specification · Transitions of recursive CCS · Constants listing their transitions realize them · Parallel composition preserves realization · Realization of a code-level transition system · Restriction preserves realization · Certificate checks give rooted observation congruence · Transitions of a sum of prefixes · Certificate checks give weak bisimilarity

InductiveTransitions of recursive CCS#✓fully proved

Let the channel names have decidable equality and let \(\Delta\) be a recursive specification, assigning to each process constant \(A\) its defining body \(\Delta(A)\). The labelled transition relation \(P \xrightarrow{\alpha} P'\) relative to \(\Delta\) on recursive CCS processes, with actions \(\alpha\) the CCS labels (silent \(\tau\), inputs and outputs), is the least relation closed under the following rules, where \(\alpha.P\) is the prefix, \(P + Q\) the choice, \(P \mid Q\) the parallel composition, \(P \setminus L\) the restriction of \(P\) by a finite list \(L\) of channel names, and \(P[f]\) the relabelling of \(P\) by a finite relabelling \(f\). If \(\Delta(A) \xrightarrow{\alpha} P'\), then \(A \xrightarrow{\alpha} P'\). The prefix has the transition \(\alpha.P \xrightarrow{\alpha} P\). If \(P \xrightarrow{\alpha} P'\), then \(P + Q \xrightarrow{\alpha} P'\), \(Q + P \xrightarrow{\alpha} P'\), \(P \mid Q \xrightarrow{\alpha} P' \mid Q\) and \(Q \mid P \xrightarrow{\alpha} Q \mid P'\). If \(P \xrightarrow{\alpha} P'\) and \(Q \xrightarrow{\beta} Q'\) where \(\alpha\) and \(\beta\) are complementary (an input and an output on the same channel), then \(P \mid Q \xrightarrow{\tau} P' \mid Q'\). If \(P \xrightarrow{\alpha} P'\) and \(\alpha\) is \(\tau\) or its channel is not in \(L\), then \(P \setminus L \xrightarrow{\alpha} P' \setminus L\). If \(P \xrightarrow{\alpha} P'\), then \(P[f] \xrightarrow{f(\alpha)} P'[f]\), where \(f(\tau) = \tau\), an input on a channel \(a\) is sent to the visible label \(f(a)\) that \(f\) assigns to \(a\), and an output on \(a\) is sent to the complement of \(f(a)\).

Cslib.CCS.Recursive.Process.Step · 33 lines 
inductive Step (specification : Specification Name Constant) :
    Process Name Constant → Label Name → Process Name Constant → Prop
  | unfold {constant action next}
      (step : Step specification (specification constant) action next) :
      Step specification (.constant constant) action next
  | prefix (action) (continuation) :
      Step specification (.prefix action continuation) action continuation
  | choiceLeft {left right action next}
      (step : Step specification left action next) :
      Step specification (.choice left right) action next
  | choiceRight {left right action next}
      (step : Step specification right action next) :
      Step specification (.choice left right) action next
  | parallelLeft {left right action next}
      (step : Step specification left action next) :
      Step specification (.parallel left right) action (.parallel next right)
  | parallelRight {left right action next}
      (step : Step specification right action next) :
      Step specification (.parallel left right) action (.parallel left next)
  | communicate {left right left' right' leftAction rightAction}
      (leftStep : Step specification left leftAction left')
      (rightStep : Step specification right rightAction right')
      (complementary : leftAction.Complementary rightAction) :
      Step specification (.parallel left right) .tau (.parallel left' right')
  | restrict {blocked process action next}
      (step : Step specification process action next)
      (allowed : StaticProcess.Allowed blocked action) :
      Step specification (.restriction blocked process) action
        (.restriction blocked next)
  | relabel {rename process action next}
      (step : Step specification process action next) :
      Step specification (.relabelling rename process)
        (StaticProcess.relabelAction rename action) (.relabelling rename next)
Uses 7 · Used by 13
Statement usesCCS labels · Complementary labels · Recursive CCS processes · Recursive CCS specification · Relabelling · Actions permitted by a restriction · Relabelling an action
Used byThe silent closure of the buffer is trivial · Visible weak steps of the buffer · Lossy acknowledgements break the buffer specification · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages · Labelled transition system of a recursive specification · Constants listing their transitions realize them · Parallel composition preserves realization · Realization of a code-level transition system · Restriction preserves realization · Certificate checks give rooted observation congruence · Transitions of a sum of prefixes · Certificate checks give weak bisimilarity

DefinitionLabelled transition system of a recursive specification#✓fully proved

Assuming equality of names is decidable, for a recursive specification \(\Delta\) the labelled transition system generated by \(\Delta\) has the recursive CCS processes as states and the CCS labels as labels, and its transitions \(P \xrightarrow{\alpha} P'\) are exactly the steps of the structural operational semantics relative to \(\Delta\).

def lts (specification : Specification Name Constant) :
    Cslib.LTS (Process Name Constant) (Label Name) :=
  ⟨Step specification⟩
Uses 4 · Used by 5
Statement usesCCS labels · Recursive CCS processes · Transitions of recursive CCS · Recursive CCS specification
Used byAlternating-bit transition system · Transition system of the alternating-bit protocol with data · Labelled transition system of go-back-N · Certificate checks give rooted observation congruence · Certificate checks give weak bisimilarity

DefinitionGuardedness under a prefix flag#✓fully proved

For a Boolean flag \(b\), recording whether an action prefix has already been crossed, guardedness of a recursive CCS process under \(b\) is defined recursively: the inactive process \(\mathbf{0}\) is guarded under \(b\); a constant \(A\) is guarded under \(b\) exactly when \(b\) is true; a prefix \(\alpha.Q\) is guarded under \(b\) when \(Q\) is guarded under true; a choice \(Q + R\) or a parallel composition \(Q \mid R\) is guarded under \(b\) when both \(Q\) and \(R\) are; and a restriction \(Q \setminus L\) or a relabelling \(Q[f]\) is guarded under \(b\) when \(Q\) is.

Thus under the flag false a process is guarded exactly when every constant occurrence lies beneath an action prefix. Static operators and parallel/choice contexts do not themselves guard recursion.

def GuardedUnder (beneathPrefix : Bool) : Process Name Constant → Prop
  | .nil => True
  | .constant _ => beneathPrefix = true
  | .prefix _ continuation => GuardedUnder true continuation
  | .choice left right | .parallel left right =>
      GuardedUnder beneathPrefix left ∧ GuardedUnder beneathPrefix right
  | .restriction _ process | .relabelling _ process =>
      GuardedUnder beneathPrefix process
Uses 3 · Used by 3
Statement usesCCS labels · Recursive CCS processes · Relabelling
Used byGuarded process · Renaming constants preserves guardedness · Every process is guarded beneath a prefix

DefinitionGuarded process#✓fully proved

A recursive CCS process is guarded when all of its constant occurrences lie beneath an action prefix.

def Guarded (process : Process Name Constant) : Prop := GuardedUnder false process
Uses 2 · Used by 1
Statement usesRecursive CCS processes · Guardedness under a prefix flag
Used byGuarded recursive specification

TheoremEvery process is guarded beneath a prefix#✓fully proved

Every recursive CCS process \(P\) is guarded under the flag \(\mathrm{true}\): once an action prefix has been crossed, every constant occurrence counts as guarded.

theorem guardedUnder_true (process : Process Name Constant) : GuardedUnder true process
Uses 4 · Used by 1
Statement usesRecursive CCS processes · Guardedness under a prefix flag
Proof usesCCS labels · Relabelling
Used byRenaming constants preserves guardedness

DefinitionConstant occurrences of a process#✓fully proved

The constant occurrences of a recursive CCS process \(P\) are the list of the process constants occurring in \(P\), from left to right and with repetitions: the inactive process \(\mathbf{0}\) has none; a constant \(A\) has the single occurrence \(A\); a prefix \(\alpha.Q\), a restriction \(Q \setminus L\) and a relabelling \(Q[f]\) have the occurrences of \(Q\); and a choice \(Q + R\) or a parallel composition \(Q \mid R\) has the occurrences of \(Q\) followed by those of \(R\).

def constantOccurrences : Process Name Constant → List Constant
  | .nil => []
  | .constant name => [name]
  | .prefix _ continuation => constantOccurrences continuation
  | .choice left right | .parallel left right =>
      constantOccurrences left ++ constantOccurrences right
  | .restriction _ process | .relabelling _ process => constantOccurrences process
Uses 3 · Used by 1
Statement usesCCS labels · Recursive CCS processes · Relabelling
Used byConstants of a process

DefinitionConstants of a process#✓fully proved

Assuming equality of process constants is decidable, the constants of a recursive CCS process \(P\) are the list obtained from the constant occurrences of \(P\) by removing duplicates, so that every process constant occurring in \(P\) appears in it exactly once.

def constants [DecidableEq Constant] (process : Process Name Constant) : List Constant :=
  (constantOccurrences process).dedup
Uses 2
Statement usesRecursive CCS processes · Constant occurrences of a process

DefinitionRenaming process constants#✓fully proved

Given a map \(\rho\) from one set of process constants to another, renaming the constants of a recursive CCS process \(P\) by \(\rho\) replaces each occurrence of a constant \(A\) by \(\rho(A)\) and leaves \(P\) otherwise unchanged: the inactive process, prefixes, choices, parallel compositions, restrictions and relabellings are kept as they are.

def mapConstants {Other : Type*} (rename : Constant → Other) :
    Process Name Constant → Process Name Other
  | .nil => .nil
  | .constant name => .constant (rename name)
  | .prefix action continuation => .prefix action (mapConstants rename continuation)
  | .choice left right => .choice (mapConstants rename left) (mapConstants rename right)
  | .parallel left right => .parallel (mapConstants rename left) (mapConstants rename right)
  | .restriction blocked process => .restriction blocked (mapConstants rename process)
  | .relabelling relabel process => .relabelling relabel (mapConstants rename process)
Uses 3 · Used by 1
Statement usesCCS labels · Recursive CCS processes · Relabelling
Used byRenaming constants preserves guardedness

TheoremRenaming constants preserves guardedness#✓fully proved

Let \(P\) be a recursive CCS process, let \(\rho\) be a map from its process constants to another set of constants, and let \(P\rho\) be the process obtained from \(P\) by renaming its constants by \(\rho\). Then for each Boolean flag \(b\), \(P\rho\) is guarded under \(b\) if and only if \(P\) is guarded under \(b\).

theorem guardedUnder_mapConstants {Other : Type*} (rename : Constant → Other)
    (beneathPrefix : Bool) (process : Process Name Constant) :
    GuardedUnder beneathPrefix (mapConstants rename process) ↔
      GuardedUnder beneathPrefix process
Uses 6
Statement usesRecursive CCS processes · Guardedness under a prefix flag · Renaming process constants
Proof usesCCS labels · Every process is guarded beneath a prefix · Relabelling

DefinitionGuarded recursive specification#✓fully proved

A recursive specification \(\Delta\), which assigns to each process constant \(A\) a body \(\Delta(A)\), is guarded when for every constant \(A\) the body \(\Delta(A)\) is a guarded process.

def Guarded (specification : Specification Name Constant) : Prop :=
  ∀ constant, Process.Guarded (specification constant)
Uses 2
Statement usesGuarded process · Recursive CCS specification
48 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.