a \longrightarrow_{\mathcal{R}} a'

reaction under the rules \mathcal{R}

Bg.React, Reactive.React, printed a ⟶[R] a'; concrete WRS.React, printed a ⟶[W] a'

from source

a \xrightarrow{L}_{\lambda} a'

labelled transition: the label is a context L, at the set of locations \lambda

WRS.Trans, printed a ─[L, λ]→ a'; without locations (WRS.UTrans, Reactive.Trans), a ─[L]→ a'

from source, unbridged

a \sim b

strong bisimilarity

WRS.Bisim, Reactive.Bisimilar, printed a ∼ b

from source, unbridged

a \approx b

weak bisimilarity

see Logic, below

not audited

g \circ f = h

in a precategory, where composition is partial: g \circ f is defined and equals h

PreCat.Comp, printed g ◦ f ≃ h

from source

f \bumpeq g, A \Bumpeq B

support equivalence and lean-support equivalence of concrete bigraphs

SPreCat.SuppEquiv, printed f ≏ g; Big.LeanEquiv, printed A ≎ B

from source, new

\pi \bullet G

support translation: G with its nodes and edges renamed by the permutation \pi

Big.tr, BigH.tr, LiG.tr

from source, not audited

\mathrm{IPO}(f_0, f_1; h_0, h_1)

the pair (h_0, h_1) is an idem pushout for (f_0, f_1)

PreCat.IsIPO

from source

a \sim^{\mathrm{FPE}} b

bisimilarity in which only the engaged transitions between prime interfaces must be matched

WRS.RelBisim at FPE

from source

A \mid_{\ell} A', G \parallel G'

parallel product of concrete link graphs and of concrete bigraphs, for disjoint supports and inner names (provisional symbol \mid_{\ell}; TR-580 writes \mid)

LiG.par, Big.par, BigH.par

from source

A \doteq B

the same link graph, or bigraph, at faces with the same members (provisional symbol)

LiG.Same, Big.Same

new

\mathrm{merge}_m^X

the concrete merge of m sites into one root, with the names X passed through (provisional symbol)

Big.mergeN

bridged

/_k\, x, \mathrm{cl}_e(X; Y), \mathrm{cl}^m_e(X; Y)

closure of the one name x by the edge k; of the names X by the edges e(x), the names Y passed through; the same on a bigraph of width m (provisional symbols)

LiG.closure1, Big.closure1; LiG.closure; Big.closure, Big.closureW

from source, bridged, new

P \equiv Q

structural congruence of processes (CCS, π)

Locus.CCS.SC, Locus.CCSFull.SC, Pi.SC, printed P ≡ Q

from source, bridged, unbridged

P \to Q

reduction of processes

Locus.CCS.Red, Locus.CCSFull.Red, Pi.Red, printed P ⟶ Q

from source, new

\llbracket P \rrbracket

the bigraph encoding a process (its names and environment are not printed)

CCS.agent, CCSFull.agent, agentπ, printed ⟦P⟧

from source

o \checkmark_F a

the occurrence certificate o passes the checker for the rule family F in the agent a (the simulator)

Occ.check

bridged

a \Rightarrow_F b

reachability by checked steps of the rule family F (Miolingo)

Keys.Reach, D1.Reach, Main.Reach, ReachA

bridged, unbridged, new

a \rightsquigarrow b

a user action (Miolingo): a well-formed request is placed in the agent; it is not a reaction

Miolingo.Act

unbridged, new

a \Rightarrow^{\mathsf u}_F b

reachability by checked steps of the family F and user actions (Miolingo)

Miolingo.ReachU

new

\llbracket d \rrbracket

the library's bigraph built from a checked description d fitting I \to J (the simulator's data); the same brackets as the process encoding, told apart by what is inside

BD.toBigAt, printed ⟦d⟧

bridged