(1)
For the deterministic automaton functor \(TX = 2 \times X^A\)  with
\(A = \lbrace a,b\rbrace \) , we let \(\mathcal {L} \)  be the set of two binary
modalities \(\langle 0, a.(-), b.(-)\rangle \)  and \(\langle 1, a.(-), b.(-)\rangle \) 
(corresponding to the two Moss liftings of ex:Moss.1). We
interpret expressions in the final \(T\) -coalgebra \(\nu T\)  carried by
all formal languages over \(A\) . Here are a few closed and guarded
expressions and their semantics in \(\nu T\)  (as usual \(|w|_b\)  denotes the
number of \(b\) 's in \(w\) ):
\(\llbracket \nu v. \langle 0, a.v, b.v\rangle  \rrbracket _{} & = \lbrace \emptyset \rbrace  \\\llbracket \nu z. \langle 1, a.z, b.z\rangle  \rrbracket _{} & = \lbrace A^*\rbrace  \\\llbracket \nu x. \langle 1, a.x, b.\nu y. \langle 0, a.y, b.x\rangle \rangle  \rrbracket _{}&= \lbrace \lbrace  w \in A^* \mid |w|_b\ \text{even} \rbrace \rbrace \) 
\(\begin{tikzpicture}[>=Latex,shorten >=1pt,on grid,node distance=2cm,every state/.style={minimumsize=10pt},auto,every node/.style={font=\tiny }]\node [state] (q0) {v};[->] (q0) edge [loop left] node {a,b} ();\end{tikzpicture}\node [state,accepting] (q1) [right=of q0] {z};[->] (q1) edge [loop left] node {a,b} ();\) 
state,accepting] (q2) [right=of q1] x;
state] (q3) [right=of q2] y;
[->] (q2) edge [loop left] node a ()
edge [bend left] node b (q3)
(q3) edge [loop right] node a ()
edge [bend left] node b (q2);
\(Note that the semantics of each of these expressions is a singleton(up to behavioural equivalence); in fact, for an arbitrary\) 
\(-coalgebra \) X\(, the semantics of the above expressions is the setof states accepting the language in the singleton on theright. In~{lem:gfp-is-singleton} further below we prove thatthis holds in general.\)
(2)
Consider \(T = \mathcal {P} _\omega (A \times -)\)  where \(A\)  is a finite set of
labels. A presentation of \(T\)  is given by the signature containing
for each \(n\) -tuple \(\vec{a} = (a_1, \ldots , a_n) \in A^n\)  one \(n\) -ary
operation symbol, and the corresponding natural transformation
\(\tau  ^{\vec{a}}: (-)^n \rightarrow T\)  is defined by
\(\tau  ^{\vec{a}}_X: (x_1, \ldots , x_n) \mapsto \lbrace (a_1,x_1), \ldots ,(a_n,x_n)\rbrace .\) 
The corresponding Moss lifting is \(\lambda  ^{\vec{a}}/n\)  given by
\(\textstyle \lambda  ^{\vec{a}}_X(Y_1, \ldots , Y_n)=\lbrace  Z\in \mathcal {P}_\omega  (A \times X) \mid Z\subseteq \bigcup _{i=1}^n(\lbrace a_i\rbrace \times Y_i) \\\text{and }Z \cap \lbrace a_i\rbrace  \times Y_i\ne \emptyset \text{ for$i=1,\ldots ,n$}\rbrace \) 
(cf. (REF )). Now put
\(\mathcal {L} = \lbrace [\vec{a}]/n \mid \vec{a} \in A^n, n \in \omega \rbrace \)  and
interpret each \([\vec{a}]\)  by \(\lambda  ^{\vec{a}}\) . For example, for
\(A = \lbrace a,b\rbrace \)  the expression \(\nu x. [a]([a,b,a](x,[()],[()]))\) ,
where \([()]\)  is the unique nullary modality in \(\mathcal {L} \) ,
describes the left-hand state in the following labelled transition system
\(\begin{tikzpicture}[shorten >=1pt,on grid,node distance=2cm,every state/.style={minimumsize=10pt},auto,every node/.style={font=\tiny }]\node [state] (q0) {x};\node [state] (q1) [right=of q0] {y};\node [state] (q2) [right=of q1] {z};\node [state] (q3) [below=of q1] {w};\end{tikzpicture}[->] (q0) edge [bend right] node[below] {a} (q1)(q1) edge [bend right] node[above] {a} (q0)edge node {a} (q2)edge node {b} (q3);\) 
\(\item For \) 
= \(\mathcal {D}\)  \( we have the presentation with an \) n\(-aryoperation \)\(\tau \)  p\( for every \) p = (p1, ..., pn)\(with \) i=1n pi = 1\( and corresponding Moss liftings asdescribed in~{ex:Moss}.3. For each such \) p\(, weintroduce a modality \) [p]/n\(\mathcal {L}\)  \(, and interpret itas \)\(\lambda \)  p\(. Now consider the Markov chain (i.e.\ \)\(\mathcal {D}\)  \(-coalgebra)\)\(\begin{tikzpicture}[shorten >=1pt,on grid,node distance=2.5cm,every state/.style={minimumsize=10pt},auto,every node/.style={font=\tiny }]\node [state] (q0) {x};\node [state] (q1) [above right=of q0] {y};\node [state] (q2) [below right=of q1] {z};\end{tikzpicture}[->] (q0) edge [out=210,in=150,loop] node {{2}{3}} ()edge [out=65,in=215] node {{1}{3}} (q1)(q1) edge [out=120,in=60,loop] node {{1}{3}} ()edge [out=245,in=25] node[right] {{1}{6}} (q0)edge node {{1}{2}} (q2)(q2) edge [out=-30,in=30,loop] node[right] {{3}{4}} ()edge node {{1}{4}} (q0);\)
\(The behaviour of the left-hand state is described by the expression\) 
x. [23, 13](x, y.
[16,13,12](x,y, z.
[14,34](x,z))).
\(\) 



The syntax of our expressions is determined purely by the finitary
coalgebraic type functor, more precisely, by a given strongly
expressive set \(\Lambda  \)  of monotone singleton-preserving
predicate lifting. In contrast, existing expression calculi such as
standard regular expressions for deterministic automata or the
coalgebraic expression calculi in [1]}, [2]} use
extra operations (e.g. expressing union or concatenation of
languages). These operations are not dictated by the setting,
viz. an endofunctor on \(\mathbf {Set} \) . Rob Myers' PhD thesis [3]}
explains nicely how such extra operations are obtained naturally in
an expression calculus when one works over an algebraic category
(such as the one of join-semilattices or vector spaces over the
reals, i.e. algebras for the monad \(\mathbb {R} ^{(-)}\) ). We leave the
extension of our expression language to this more general setting
for future work.
Our Kleene theorem requires a number of technical lemmas:
Let \(\lambda /n\)  and \(\lambda ^{\prime }/n^{\prime }\)  be monotone singleton-preserving
predicate liftings for \(T\) . Let \(S\)  be an equivalence relation on a
set \(X\) , let \(A_1,\dots ,A_{n}\) , be
\(S\) -equivalence classes or empty, and let \(B_1,\dots ,B_{n^{\prime }}\)  be \(S\) -closed
subsets of \(X\) . Then the following holds.

\(\lambda  _{X} (A_1,\dots A_n) \subseteq \lambda  _{X}^{\prime }(B_1,\dots B_{n^{\prime }}) \text{ or }\lambda  _{X} (A_1,\dots A_n) \cap \lambda  _{X}^{\prime } (B_1,\dots B_{n^{\prime }}) =\varnothing .\)

If the \(B_1,\ldots ,B_{n^{\prime }}\)  are even \(S\) -equivalence classes or empty, then
\(\lambda  _{X} (A_1,\dots A_n) = \lambda  _{X}^{\prime }(B_1,\dots B_{n^{\prime }}) \text{ or }\lambda  _{X} (A_1,\dots A_n) \cap \lambda  _{X}^{\prime } (B_1,\dots B_{n^{\prime }}) =\varnothing .\) 

[Sketch]
Apply naturality to the quotient map \(q: X \twoheadrightarrow X/S\) .
In the proof of lem:gfp-is-singleton further
below, we will make use of a \(\Lambda  \) -bisimulation. We briefly
recall the essentials of this notion [4]}:
[\(\Lambda  \) -Simulation]
Given a pair of \(T\) -coalgebras \(( X,\xi )\)  and \(( Y,\zeta )\) , a
\(\Lambda  \) -simulation is a relation \(S\subseteq X\times Y\)  such
that for all predicate liftings \(\lambda  \in \Lambda  \)  and
\(X_i\subseteq X\) , \(x\mathbin {S}y\)  implies
\(\xi ( x ) \in \lambda  _X( X_1,\dots , X_n ) \Rightarrow \zeta ( y)\in \lambda  _Y( S[ X_1 ],\dots , S[ X_n ] ).\) 
A \(\Lambda  \) -bisimulation is a \(\Lambda  \) -simulation \(S\)  such that
\(S^\circ  \)  is also a \(\Lambda  \) -simulation. Elements \((x,y) \in X\times Y\) 
are \(\Lambda  \) -bisimilar if there is a \(\Lambda  \) -bisimulation
relating \(x\)  and \(y\) .



\(\Lambda \) -bisimilarity concides with behavioural equivalence.


In fact, for Theoren REF  it is sufficient that
\(\Lambda \)  is separating and the predicate liftings in \(\Lambda \)  are
monotone. It turns out that Theorem REF  is actually a
special case of [5]}, applied to the case
where the lax extension is induced by a separating set of monotone
predicate liftings.
Let \((X,\xi )\)  be a \(T\) -coalgebra, let \(\lambda  _i/k\in \Lambda  \) ,
\(i = 1, \ldots , k\) , and let \((A_1,\dots , A_k)\)  be the greatest fixed
point of the map \(h:(\mathcal {Q} X)^k \rightarrow (\mathcal {Q} X)^k\)  defined
by
\(\begin{pmatrix}X_1 \\\vdots \\X_k\end{pmatrix} \mapsto \begin{pmatrix}\xi ^{-1}[\lambda  _{1,X}(X_1,\dots ,X_k)] \\\vdots \\\xi ^{-1}[\lambda  _{k,X}(X_1,\dots , X_k)]\end{pmatrix}\) 
Then for each \(i\) , all elements of \(A_i\)  are behaviourally
equivalent, and for all \(i\) , \(j\) , either \(A_i\cap A_j=\varnothing \) 
or \(A_i=A_j\) .
(In the above lemma, we restrict to all \(\lambda  _i\)  having
full arity \(k\)  and using their arguments in the given order only in
the interest of readability; this is w.l.o.g. since we can just
reorder arguments and add dummy arguments.)
[Sketch]
Let \(S \subseteq X \times X\)  be the relation
\(S = \lbrace  ( x_1,x_2 )\mid \exists A_i\,.\,x_1\in A_i\wedge x_2\in A_i\rbrace \cup \Delta _X.\) 
Using lem:predicate-liftings-preserve-equivalence-classes
one shows first that \(S\)  is an equivalence relation, which already
takes care of the second part of the claim, and then that \(S\)  is a
\(\Lambda \) -bisimulation. The first claim of the lemma then follows by
Theorem REF .
The final ingredient of our Kleene-type correspondence is
the following adaptation of Bekič's bisection lemma [6]}:

For complete lattices \((X,\le )\) , \((Y,\le )\)  and for every pair of monotone maps
\(f: X\times Y \rightarrow X\)  and \(g: X\times Y \rightarrow Y\) , we have
\(\nu ( x, y ) . ( f( x,y ),g( x,y ) ) = (x_0, y_0)\quad \text{ with }\quad \begin{array}{rl}x_0 &= \nu x.f( x, \nu y . g( x, y ) ) \\y_0 &= \nu y. g( x_0, y ).\end{array}\) 

Although in [6]} this lemma only covers least fixed points
in a slightly different setting, the proof is the same.
For completeness, we provide it in the appendix.
Using lem:bekic we can transform every expression
\(\phi \in \mathcal {E}_0 \)  into a system of flat equations
\((z_1 = \phi _1,\dots , z_k = \phi _k)\)  for some \(k\in \omega \) , i.e.
equations without nested modalities or fixed point operators: This is
done by first ensuring that every fixed point operator uses a
different fixed point variable and then binding every modality that is
not nested directly under a fixed point operator with a new fixed
point operator using a fresh variable. Thus we can rewrite every expression
\(\phi \in \mathcal {E}_0 \)  in the form
\(\phi \equiv \nu z_1 .\, \textit {L} _1 ( z_1, \nu z_2 .\textit {L} _2( \dots ),\dots , \nu z_k .\textit {L} _k( \dots ))\) 
for some modalities \(L_i\in \mathcal {L} \) , \(i = 1, \ldots , k\) . If we
now inductively apply lem:bekic and, for readability,
additionally normalize every modality to have as many arguments as
there are different fixed point variables in such an expression,
introducing dummy arguments where necessary, then we can write
\(\phi \)  as a system
\(\begin{aligned}z_1 &= \textit {L} _1( z_1, z_2, \dots , z_k )\\z_2 &= \textit {L} _2( z_1, z_2, \dots , z_k )\\\vdots &\\z_k &= \textit {L} _n( z_1, z_2, \dots , z_k )\end{aligned}\) 
of flat equations. Given any coalgebra \(C = (X, \xi )\) , the above
system induces an obvious map of the form (REF ) (replacing
\(z_i\)  by \(X_i\)  and \(L_i\)  by \(\lambda  _i= \llbracket L_i \rrbracket _{} \) ), and the first
components of its greatest fixed point is the semantics
\(\llbracket \phi  \rrbracket _{C} \) . The following example shows a concrete case.
[Applying Bekič's bisection lemma]

Consider the expression
\(\phi = \nu x. \textit {L} _1 ( x, \textit {L} _2( x ), \nu y.\textit {L} _3( y, \nu z . \textit {L} _2( z ) ) )\) 
In order to transform it as per the procedure indicated, we first
need to add a fixed point operator with a fresh variable to the
first occurrence of \(\textit {L} _2\) :
\(\phi = \nu x. \textit {L} _1 ( x, \nu w .\textit {L} _2( x ), \nu y.\textit {L} _3( y, \nu z . \textit {L} _2( z ) ) )\) 
Then we can form the equation system for the variables \(x, w, y, z\)
\(x &= \overline{\textit {L}}_1( x, w, y, z ) = \textit {L} _1( x, w, y ) \\w &= \overline{\textit {L}}_2( x, w, y, z ) = \textit {L} _2( x ) \\y &= \overline{\textit {L}}_3( x, w, y, z ) = \textit {L} _3( y, z ) \\z &= \overline{\textit {L}}_4( x, w, y, z ) = \textit {L} _2( z )\) 

where we extend \(\mathcal {L}\)  with additional operators
\(\overline{\textit {L}}_i\)  having dummy arguments, defined as indicated.
The semantics of this equation system in a coalgebra \(C=( X, \xi )\)  is
defined as the greatest fixpoint \(( A_0, A_1, A_2, A_3 )\)  of the map
\(h: \mathcal {Q} ^n X \rightarrow \mathcal {Q} ^n X\)  defined by
\(h:\begin{pmatrix}X_1 \\ X_2 \\ X_3 \\ X_4\end{pmatrix}\mapsto \begin{pmatrix}\xi ^{-1}[\llbracket \textit {L} _1 \rrbracket _{X} ( X_1, X_2, X_3 )] \\\xi ^{-1}[\llbracket \textit {L} _2 \rrbracket _{X} ( X_1 )] \\\xi ^{-1}[\llbracket \textit {L} _1 \rrbracket _{X} ( X_2, X_4 )] \\\xi ^{-1}[\llbracket \textit {L} _2 \rrbracket _{X} ( X_4 )]\end{pmatrix}.\) 
The semantics of \(\phi \)  in \(C\)  is then \(\llbracket \phi  \rrbracket _{C} = A_0\) .
The following two results together establish a Kleene-type
correspondence for the generic expressions of
def:generic-expressions.


Every expression \(\phi \in \mathcal {E}_0 \)  describes exactly one
behavioural equivalence class, which is moreover realized in a
finite coalgebra. Explicitly: there exists a state \(x\)  in a finite
coalgebra such that for every coalgebra \(C\) , \(\llbracket \phi  \rrbracket _{C} \) 
contains precisely the states of \(C\)  that are behaviourally
equivalent to \(x\) .

[Sketch]
By lem:invariance, it suffices to show that any two states
(w.l.o.g. in the same coalgebra, using coproducts) satisfying
\(\phi \)  are bisimilar. Since \(\phi \)  can transformed into a
system (REF ) of flat equations, this follows by
lem:gfp-is-singleton. Realization in a finite coalgebra
follows from the finite model property of the coalgebraic
\(\mu \) -calculus [8]}, and alternatively is shown by
constructing a model from the variables in a flat equation system.
Let \(C=(X, \xi )\)  be a finite \(T\) -coalgebra. For every \(x \in X\) , there
exists an expression \(\phi \in \mathcal {E}_0 \)  such that
\(x \in \llbracket \phi  \rrbracket _{C} \) .


Let \(X = \lbrace x_1, \dots , x_{k}\rbrace \)  and w.l.o.g. \(x = x_1\) . Since
\(\Lambda \)  is strongly expressive, for every \(x_i \in X\)  there is a
modality \(L_i\) , w.l.o.g. with arity \(k\)  and prescribed argument
ordering, such that
\(\lbrace  \xi (x_i) \rbrace  = \llbracket L_i \rrbracket _{X} (\lbrace x_{1}\rbrace , \ldots , \lbrace x_{k}\rbrace ).\) 
That is, the \(\lbrace x_i\rbrace \)  solve the system
\((x_i=L_i(x_1,\dots ,x_k))_{i=1,\dots ,k}\)  of flat fixed point
equations, so for the greatest fixed point \((A_1,\dots ,A_k)\)  of the
system, we have \(x_i\in A_i\)  for every \(i\) , in particular
\(x=x_1\in A_1\) . It now just remains to convert the equation system
into an equivalent single expression in the standard
manner [9]} (incurring exponential blow-up);
then \(x\in \llbracket \phi  \rrbracket _{C} \)  as desired.


Every expression
denotes a behavioural equivalence class of a state in a finite
coalgebra, and conversely every such class is denoted by some
expression.
(1)
For the functor \(TX = 2 \times X^A\)  for \(A = \lbrace a,b\rbrace \)  consider
the coalgebra with carrier \(X = \lbrace x_1, x_2\rbrace \)  and with coalgebra
structure \(\xi : X \rightarrow 2 \times X^A\)  with
\(\xi (x_0) = (1, (a \mapsto x_0, b \mapsto x_1))\)  and
\(\xi (x_1) = (0, (a \mapsto x_1, b \mapsto x_0))\) . Then we clearly
have \(\lbrace \xi (x_1)\rbrace  = \lambda  ^1(\lbrace x_1\rbrace ,\lbrace x_2\rbrace )\)  and
\(\lbrace \xi (x_2)\rbrace  = \lambda  ^1(\lbrace x_2\rbrace ,\lbrace x_1\rbrace )\) . Using the syntax
of ex:expr.1 and following the proof
of thm:kleene-theorem-for-generic-expressions, we obtain
the following expression for the behavioural equivalence
class (i.e. formal language) for \(x_1\) :
\(\nu x_1.\langle 1, a.x_1, b.\nu x_2. \langle 0, a.x_2, b.x_1\rangle \rangle .\) 
Note that this is the same expression (modulo
\(\alpha \) -equivalence) as the third expression
from ex:expr.1.
(2)
For the functor \(\mathcal {P}_\omega  (A \times -)\)  and \(A = \lbrace a,b\rbrace \)  the coalgebra \(C=(\lbrace x,y,z,w\rbrace ,\xi )\)  depicted in
ex:expr.2 satisfies the following equations:
\(\lbrace \xi (x)\rbrace  = \lambda  _C^{(a)}(\lbrace y\rbrace ), \;\lbrace \xi (y)\rbrace  = \lambda  _C^{(a,b,c)}(\lbrace x,w,z\rbrace ), \;\lbrace \xi (w)\rbrace  = \lambda  _C^{()}(), \;\lbrace \xi (w)\rbrace  = \lambda  _C^{()}()\) 
By thm:kleene-theorem-for-generic-expressions \(\lbrace \lbrace x\rbrace ,\lbrace y\rbrace ,\lbrace z\rbrace ,\lbrace w\rbrace \rbrace \) 
solves the following system, reusing the same variable names,
\(x = [a](y), \quad y = [a,b,a](x,w,z),\quad w = [()], \quad z = [()]\) 
which can be transformed as demonstrated in exp:bekbislem to the expression
given in ex:expr.2, describing the behaviour of the state \(x\) .
(3)
For the functor \(T = \mathcal {D} \)  consider the expression from ex:expr.3:
\(\nu x. [{2}{3}, {1}{3}](x, \nu y.[{1}{6},{1}{3},{1}{2}](x,y, \nu z.[{1}{4},{3}{4}](x,z)))\) , which transforms to the system
\(x = [{2}{3}, {1}{3}](x, y), \quad y = [{1}{6},{1}{3},{1}{2}](x,y, z), \quad z = [{1}{4},{3}{4}](x,z).\) 
By thm:generic-expression-describes-exactly-one-bisimulation-class we can
construct a coalgebra \(C =(\lbrace x,y,z\rbrace , \xi )\)  defined by:
\(\lbrace \xi (x)\rbrace  &= \lambda  _X^{({2}{3}, {1}{3})}(\lbrace x\rbrace ,\lbrace y\rbrace )\\\lbrace \xi (y)\rbrace  &=\lambda  _X^{({1}{6},{1}{3},{1}{2})}(\lbrace x\rbrace ,\lbrace y\rbrace ,\lbrace z\rbrace )\\\lbrace \xi (z)\rbrace  &= \lambda  _X^{({1}{4},{3}{4})}(\lbrace x\rbrace ,\lbrace z\rbrace )\) 

which is exactly the coalgebra depicted in ex:expr.3 where \(x\)  is in the
behavioural equivalence class of the above expression.

An alternative approach to defining the semantics of expressions is to
construct a \(T\) -coalgebra structure on the set \(\mathcal {E}_0\)  of closed and
guarded expressions, similarly as in the work of Silva et
al. [1]} and also Myers [3]}. In
thm:coalgebraic-and-modallogic-semantics-coincide below we
show that this new semantics coincides with the previous one.

We define a \(T\) -coalgebra
\(\varepsilon : \mathcal {E}_0 \rightarrow T \mathcal {E}_0 \)  inductively by
\(\varepsilon ( \textit {L} ( \phi _1, \dots , \phi _n ) ) &\in \llbracket L \rrbracket _{} ( \lbrace  \phi _1 \rbrace , \dots , \lbrace  \phi _n \rbrace  )\\\varepsilon ( \nu x.\phi ) & = \varepsilon ( \phi [ \nu x.\phi /x] ). \) 


This is actually a definition of \(\varepsilon \)  because (a)
in (REF ), \(\llbracket L \rrbracket _{} \)  preserves singletons and thus
there is only one element in
\(\llbracket L \rrbracket _{} ( \lbrace  \phi _1 \rbrace , \dots , \lbrace  \phi _n \rbrace  )\) , and (b) for the
inductive part (), one can use the number of
top-level fixed point operators as a termination measure, which
decreases in each step because the fixed points are
guarded.
Now recall that a coalgebra \(\xi : X\rightarrow TX\)  is locally finite if
every \(x\in X\)  is contained in a finite subcoalgebra of \(\xi \) . Locally
finite coalgebras are precisely the (directed) unions of finite
coalgebras (see [12]}). Thus, it follows from
thm:kleene-theorem-for-generic-expressions that for any
\(x\in X\)  in a locally finite coalgebra \(\xi : X\rightarrow TX\) , there exists a
\(\phi \in \mathcal {E}_0 \)  with \(x\in \llbracket \phi  \rrbracket _{X} \) .
Moreoever, \(\mathcal {E}_0 \)  is obviously not finite; however, arguing via
finiteness of the Fischer-Ladner closure [13]} we obtain

The \(T\) -coalgebra \((\mathcal {E}_0,\varepsilon )\)  is locally finite.
The following theorem says that \((\mathcal {E}_0,\varepsilon )\)  serves
as a canonical model of the expression language:
For every closed and guarded expression \(\phi \in \mathcal {E}_0 \)  and every
state \(x\)  in a \(T\) -coalgebra \(C\) , \(x\in \llbracket \phi  \rrbracket _{C} \)  iff \(x\)  is
behaviourally equivalent to \(\phi \)  as a state in
\((\mathcal {E}_0,\varepsilon )\) .
In particular, the above implies that
\(\phi \in \llbracket \phi  \rrbracket _{\mathcal {E}_0} \qquad \text{for all $\phi \in \mathcal {E}_0 $,}\) 
essentially a truth lemma for \(\mathcal {E}_0 \) . For the proof of
Theorem REF , we note:

\(\alpha \) -Equivalent expressions are behaviourally equivalent as
states in \((\mathcal {E}_0,\varepsilon )\) .
[Theorem REF , sketch]
It suffices to prove (REF ): The `if' direction of the
claim then follows from invariance of \(\phi \)  under behavioural
equivalence (lem:invariance), and `only if' is by
Theorem REF .
We generalize (REF ) to expressions \(\phi \)  with free
variables: Whenever \(\sigma \)  is a substitution of the free variables
of \(\phi \)  and \(\kappa  \)  a valuation such that \(\sigma (v)\in \kappa  (v)\)  for
every free variable \(v\)  of \(\phi \) , then
\(\phi \sigma \in \llbracket \phi  \rrbracket _{\mathcal {E}_0}^{\kappa }.\) 
We proceed by induction on \(\phi \) , using Lemma REF  in
the fixpoint case.
To give a concrete example use of the connection between expression
languages and modal fixed point logics afforded by the above
results, we note that we now obtain an alternative handle on
equivalence of expressions that complements the standard approach
via partition refinement: Expressions \(\phi ,\psi \)  are equivalent iff
some state described by \(\phi \)  (obtained, e.g., via the one of the model
constructions in
Theorems REF 
and REF )
satisfies \(\psi \) . Note that the latter is fairly easy to check as
long as the modalities are computationally tractable, since \(\psi \) 
otherwise involves only greatest fixed points. This approach is
similar to reasoning algorithms in the lightweight description logic
\(\mathcal {EL}\)  [14]}, where checking validity of
\(\phi \rightarrow \psi \)  is reduced to model checking \(\psi \)  in a minimal model
of \(\phi \) ; we leave a more detailed analysis to future work.
Conclusion and Further Work
We have defined a generic expression language for behaviours of finite
set coalgebras based on predicate liftings, specifically on a strongly
expressive set of singleton-preserving predicate liftings. There are
mutual conversions between such sets of predicate liftings and functor
presentations, one direction being via the Moss liftings introduced by
Marti and Venema [5]}; we have however demonstrated that
these fail to be mutually inverse in one direction, i.e. in general
not all singleton-preserving predicate liftings are Moss liftings. Our
language is presumably equivalent to the set-based instance of Myer's
expression language [3]}; our alternative presentation is aimed
primarily at showing that expression languages embed naturally into
the coalgebraic \(\mu \) -calculus, generalizing well-known results on the
relational
\(\mu \) -calculus [17]}, [18]}, [19]}, [20]}. The
benefit of this insight is to tighten the connection between
expression languages and specification logics, e.g. it allows for
combining model checking, equivalence checking, and reasoning within a
single formalism. On a more technical note, we show, e.g., that one
can provide an alternative semantics of expressions by defining a
coalgebra structure on expressions, an approach pioneered by Silva et
al. [1]} and used also by Myers [3]}; in the light
of the expressions/logic correspondence, this construction is now seen
as a canonical model construction for a fragment of the coalgebraic
\(\mu \) -calculus, and the core part of the proof that the two semantics
agree becomes just a truth lemma.
An important point for further work is to extend the current setup
from the base category \(\mathbf {Set} \)  to algebraic categories (such as join
semi-lattices or positive convex algebras) in order to generalize our
results to expression calculi involving convenient additional
operations (reflecting the ambient algebraic theory) such as
addition. A closely related point is the connection with coalgebraic
determinization [23]}; it should be interesting to see
whether our ideas can lead to expression calculi for coarser system
equivalences than bisimilarity, such as trace equivalence for
transition systems or distribution bisilimarity for Segala systems.
Such a generalization might be based on our recent approach
to coalgebraic trace semantics via graded monads [24]}.

Omitted Details and Proofs
Proof of lem:pres
REF .: First note that (REF )
is really a definition of \(\tau  _\lambda  \)  because \(\lambda  \)  is
preserves singletons. Moreover, \(\tau  _\lambda  \)  is natural because
for \(f:X\rightarrow Y\)  and \(x_i\in X\) ,
\(\tau  _{\lambda , X}( x_1,\ldots ,x_n ) & \in \lambda  _X( \lbrace  x_1\rbrace ,\ldots ,\lbrace  x_n \rbrace  ) & \\& \subseteq \lambda  _X( f^{-1}[ \lbrace  f(x_1) \rbrace ],\ldots ,f^{-1}[ \lbrace  f(x_n) \rbrace  ] ) &  \\& = (Tf)^{-1}[ \lambda  _Y( \lbrace  f(x_1) \rbrace ,\ldots ,\lbrace  f(x_n)\rbrace  ) ] & \\& = (Tf)^{-1}[ \lbrace  \tau  _{\lambda , Y}( f(x_1),\ldots ,f(x_n) )\rbrace ] & \\\Rightarrow \ &Tf ( \tau  _{\lambda , X} ( x_1,\ldots ,x_n )) =\tau  _{\lambda , Y}( f(x_1),\ldots ,f(x_n) )\) 
REF .: By the previous item, we obtain a
natural transformation
\(\alpha  = [ \tau  _\lambda  ]_{\lambda  \in \Lambda }\) , and
strong expressivity implies that \(\alpha  \)  is componentwise
surjective.
\(\Box \)

Proof of prop:laxdescrpres
Recall that \(\lambda  = \nabla ^L\circ \tau  \mathcal {Q} \)  by definition. Let
\(s_X: X \rightarrow \mathcal {Q} X\)  be the function \(s_X( x ) = \lbrace  x \rbrace \) . Then we have
\(& \lambda  _X( \lbrace x_1\rbrace ,\ldots ,\lbrace x_{n}\rbrace  ) \\& = \lbrace  t\in TX \mid ( t, \tau  _{\mathcal {Q} X}( \lbrace  x_1\rbrace ,\ldots ,\lbrace  x_{n} \rbrace  ) ) \in L(\in _X) \rbrace  \\& = \lbrace  t\in TX \mid ( t, \tau  _{\mathcal {Q} X}( s_X( x_1),\dots ,s_X( x_{n} ) ) ) \in L(\in _X) \rbrace  \\& = \lbrace  t\in TX \mid ( t, Ts_X \circ \tau  _X( x_1,\dots ,x_{n}) ) \in L(\in _X) \rbrace  \\& = \lbrace  t\in TX\mid ( t,\tau  _X( x_1,\dots ,x_{n} ))\in L(\in _X);( Ts_X )^\circ  \rbrace  \\& = \lbrace  t\in TX\mid ( t,\tau  _X( x_1,\dots ,x_{n} ))\in L(\in _X ; s_X^\circ ) \rbrace  \\& = \lbrace  t\in TX\mid ( t,\tau  _X( x_1,\dots ,x_{n} ))\in L(\Delta _X) \rbrace   \\& = \lbrace  \tau  _X( x_1,\dots ,x_{n} ) \rbrace \) 

Proof of prop:moss-strong-expr
Let \(t\in TX\) ; we need to show that
\(\lbrace  t \rbrace  = \lambda  ( \lbrace  x_1 \rbrace ,\dots ,\lbrace  x_n \rbrace  )\)  for some Moss
lifting \(\lambda  \)  and \(x_1, \ldots , x_n\in X\) . Since
\(\alpha : T_\Sigma \rightarrow T\)  from our functor presentation of \(T\)  has
surjective components, there exists some \(\tau /n \in \Sigma \)  such
that \(t = \alpha  _X(x_1, \ldots , x_n) = \tau  _X( x_1,\dots ,x_n )\)  for
some \(x_1, \ldots , x_n\in X\) .
Because \(L\)  is a lax extension, we have
\(Ts_X \subseteq Ls_X \subseteq L(\in _X)\)  for the function
\(s_X : x\mapsto \lbrace  x \rbrace \)  and thus
\((t, Ts_X(t)) = ( t, \tau  _{\mathcal {Q} X}( \lbrace  x_1 \rbrace ,\dots ,\lbrace  x_n \rbrace  )) \in L(\in _X)\) 
since
\(Ts_X(t)= Ts_X(\tau  _X(x_1, \ldots , x_n))= \tau  _{\mathcal {Q} X} (s_X(x_1), \ldots , s_X(x_n))\) .
Thus \(t \in \lambda  ( \lbrace  x_1 \rbrace ,\dots ,\lbrace  x_n \rbrace  )\) 
(see def:Mosslift), and since Moss liftings
preserve singletons, we conclude
\(\lbrace  t \rbrace  = \lambda  ( \lbrace  x_1 \rbrace ,\dots ,\lbrace  x_n \rbrace  )\)  as desired. \(\Box \)

Details for rem:moss-unary
We show that \(\lambda  = \lambda  ^{(\tau  ^\lambda )}\)  for monotone
singleton-preserving unary predicate liftings \(\lambda  \) . Let
\(\lambda /1\)  and \(\lambda ^{\prime }/1\)  be predicate liftings that agree on
singletons. Now for any \(X\)  and \(A \subseteq X\)  consider the
characteristic map \(\chi _A: X \rightarrow 2 = \lbrace \bot , \top \rbrace \) , which satisfies
\(A = \chi _A^{-1}(\top )\) . Then using naturality and the fact that
\(\lambda  _2(\lbrace \top \rbrace ) = \lambda  _2^{\prime }(\lbrace \top \rbrace )\) , we have
\(\lambda  _X(A)& = \lambda  _X(\chi _A^{-1}(\lbrace \top \rbrace ))= (T\chi _A)^{-1}(\lambda  _2(\lbrace \top \rbrace ))\\& = (T\chi _A)^{-1}(\lambda  _2^{\prime }(\lbrace \top \rbrace ))= \lambda  _X^{\prime }(\chi _A^{-1}(\lbrace \top \rbrace ))= \lambda  _X^{\prime }(A).\) 

Now observe that \(\lambda  \)  and \(\lambda  ^{(\tau  ^\lambda )}\)  agree on
singletons, thus they are equal as desired.

Proof of lem:fp-substitution
First we prove that for any expression \(\phi \in \mathcal {E} \)  that does not contain free
variables that are bound in another expression \(\psi \in \mathcal {E} \)  the following holds:
\(\llbracket \psi  \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} = \llbracket \psi [ \phi /z ] \rrbracket _{} ^\kappa  \) 
Induction on \(\psi \) . If \(\psi = x \ne z\)  then
\(\llbracket x \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} = \llbracket x \rrbracket _{} ^\kappa  = \llbracket x[ \phi /z] \rrbracket _{} ^\kappa  \) ; if \(\psi = z\)  then \(\llbracket z \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} =\llbracket \phi  \rrbracket _{} ^\kappa  = \llbracket z[ \phi /z ] \rrbracket _{} ^\kappa  \) ; for \(\psi = \textit {L} (\phi _1,\ldots ,\phi _n )\) :
\(\llbracket \textit {L} ( \psi _1,\ldots ,\psi _n ) \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} = \xi ^{-1}[ \llbracket L \rrbracket _{} ( \llbracket \psi _1 \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]},\ldots ,\llbracket \psi _n \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} ) ]\\\overset{I.H.}{=} \xi ^{-1}\big [ \llbracket L \rrbracket _{} ( \llbracket \psi _1[ \phi /z] \rrbracket _{},\ldots ,\llbracket \psi _n[ \phi /z ] \rrbracket _{} ) \big ] = \llbracket \textit {L} (\psi _1[ \phi /z ],\ldots ,\psi _n[ \phi /z ] ) \rrbracket _{} \\= \llbracket \textit {L} ( \psi _1,\ldots ,\psi _n )[ \phi /z ] \rrbracket _{};\) 
if \(\psi = \nu z.\psi _1\)  then \(\llbracket \nu z.\psi _1 \rrbracket _{} ^{\kappa  [z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]} = \llbracket \nu z.\psi _1 \rrbracket _{} ^\kappa  = \llbracket (\nu z.\psi )[ \phi /z] \rrbracket _{} ^\kappa  \) ; if \(\psi = \nu x.\psi _1\)  with \(x \ne z\)  then:
\(\llbracket \nu x.\psi _1 \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]}= \nu Y.\llbracket \psi _1 \rrbracket _{} ^{\kappa  [ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ][ x\mapsto Y ]}= \nu Y.\llbracket \psi _1 \rrbracket _{} ^{\kappa  [ x\mapsto Y ][ z\mapsto \llbracket \phi  \rrbracket _{} ^\kappa  ]}\\\overset{I.H.}{=} \nu Y.\llbracket \psi _1[ \phi /z ] \rrbracket _{} ^{\kappa  [ x\mapsto Y ]}= \llbracket \nu x.( \psi _1[ \phi /z ] ) \rrbracket _{} ^{\kappa } = \llbracket ( \nu x.\psi _1)[ \phi /z ] \rrbracket _{} ^\kappa  \) 
where the last equation holds because of the assumption that the free variables of \(\phi \) 
are not bound in \(\psi \) .
It follows that
\(\llbracket \nu z.\phi  \rrbracket _{} = \nu Y.\llbracket \phi  \rrbracket _{} ^{[z\mapsto Y]} = \llbracket \phi  \rrbracket _{} ^{[z\mapsto \llbracket \nu z.\phi  \rrbracket _{} ]}\overset{(\ref {eq:substitutionlemma})}{=} \llbracket \phi [ \nu z.\phi / z ] \rrbracket _{}.\) 

Proof of lem:predicate-liftings-preserve-equivalence-classes
Denote by \(q: X \twoheadrightarrow X/S\)  the canonical quotient map, let
\(C_1,\ldots ,C_m \subseteq X\)  be \(S\) -closed, and let \(\lambda /m\)  be monotone
and preserve singletons. Then \(C_i = q^{-1} [ q[C_i]]\)  for
all \(i\) . Therefore, we have for every \(t\in \mathcal {Q} TX\) :
\(t \in \lambda  _{X}(C_1,\dots C_m) =\lambda  _{X}(q^{-1}[q[C_1]],\dots ,q^{-1}[ q [ C_m ] ]) \nonumber \\\Rightarrow t \in ( Tq )^{-1} [\lambda  _{X/S}( q[ C_1 ],\dots ,q[ C_m] )]  \\\Rightarrow Tq(t) \in \lambda  _{X/S}(q[C_1],\dots , q[ C_m]).\nonumber \) 
(1)
If there is some \(t \in \lambda  _{X} (A_1,\dots A_n) \cap \lambda  _{X}^{\prime }(B_1,\dots B_{n^{\prime }})\) , then we show the inclusion. For \(s\in \lambda  _{X} (A_1,\dots A_n)\) , (REF ) provides
\(\lbrace Tq(t), Tq(s)\rbrace  \subseteq \lambda  _{X/S}(q[A_1],\ldots ,q[A_n]).\) 
Every \(A_i\subseteq X\)  is an \(S\) -equivalence class or empty, so \(q[A_i]\) 
is at most a singleton. By monotonicity and singleton preservation of \(\lambda  \) ,
the right-hand side is at most a singleton, and thus \(Tq(t) = Tq(s)\) . Applying
\((\ref {eq:gat})\)  to \(t\)  and \(B_1,\ldots ,B_{n^{\prime }}\) , we have
\(Tq(s) = Tq(t) \in \lambda ^{\prime }(q[B_1],\ldots ,q[B_{n^{\prime }}])\) , and consequently \(s\in \lambda ^{\prime }(B_1,\ldots ,B_{n^{\prime }})\) , again by (REF ).
(2)
In the case where the sets are not disjoint, the equality is
obtained by proving both inclusions using point (1).
\(\Box \)


Proof of lem:gfp-is-singleton
Let \(S \subseteq X \times X\)  be the relation
\(S = \lbrace  ( x_1,x_2 )\mid \exists A_i\,.\,x_1\in A_i\wedge x_2\in A_i\rbrace \cup \Delta _X.\) 
(1) We prove that \(S\)  is an equivalence relation. Let \(\overline{S}\) 
be the equivalence relation generated by \(S\) , and let
\(\overline{A_i}\)  be the \(S\) -closure of \(A_i\) . Then the
\(\overline{A_i}\)  are also \(\overline{S}\) -closed, and we have
\(\overline{S} = \lbrace  ( x_1,x_2 )\mid \exists \overline{A_i}\,.\,x_1\in \overline{A_i}\wedge x_2\in \overline{A_i}\rbrace \cup \Delta _X.\) 
It follows that each \(\overline{A_i}\)  is either empty (if
\(A_i=\emptyset \) ) or else an \(\overline{S}\) -equivalence
class.
Now we show that \(( \overline{A_1},\dots ,\overline{A_k} )\)  is a
post-fixed point of \(h\) : Because \((A_1,\dots , A_n)\)  is a fixed point
and the \(\lambda  _i\)  are monotone, we have
\(A_j = \xi ^{-1} [ \lambda  _{j,X} (A_1,\dots ,A_k)] \subseteq \xi ^{-1} [\lambda  _{j,X} (\overline{A_1},\dots ,\overline{A_k} )]\quad \text{for all $j$}.\) 
We will show that the post-fixed point condition
\(\overline{A_j} \subseteq \xi ^{-1}[ \lambda  _{j,X}(\overline{A_1},\dots , \overline{A_k} )]\) 
holds for all \(j\) . To see this, it suffices by (REF ) and the
definition of \(\overline{A_j}\)  to show that whenever
\(A_l\cap A_p\ne \emptyset \) , then
\(\lambda  _{l,X} (\overline{A_1},\dots ,\overline{A_k} ) = \lambda  _{p,X}(\overline{A_1},\dots , \overline{A_k}).\) 
So let \(x\in A_l\cap A_p\) . Then by (REF ),
\( \xi ( x ) \in \lambda  _{l,X} (\overline{A_1},\dots ,\overline{A_k} ) \cap \lambda  _{p,X}(\overline{A_1},\dots , \overline{A_k})\) ,
and therefore (REF ) follows by
lem:predicate-liftings-preserve-equivalence-classes.2.
Having shown that \((\overline{A_1},\dots ,\overline{A_k})\)  is a
post-fixed point of \(h\) , we obtain that
\(\overline{A_i} \subseteq A_i\)  for all \(i\) , which implies that
\(S = \overline{S}\)  is an equivalence relation. Hence every \(A_i\)  is
either empty or an equivalence class of \(S\) , whence
\(A_i \cap A_j = \emptyset \)  or \(A_i = A_j\)  holds for all \(i, j\)  as
claimed in the second part of the lemma.
(2) Now we prove that \(S\)  is a
\(\Lambda  \) -bisimulation, i.e. \(x \mathbin {S} y\)  and
\(\xi (x) \in \lambda  _X (B_1,\dots ,B_n)\)  implies
\(\xi (y) \in \lambda  _X ( S[B_1], \dots , S[ B_n ])\)  for every
\(\lambda /n\in \Lambda  \)  and \(B_j \subseteq X\) . By
Theorem REF , this implies the first claim of the lemma,
since \(x,y\in A_j\)  implies \(x\,S\,y\)  by construction of \(S\) .
By point (1), \(S\)  is an equivalence relation, so
\(S[B_j] = \overline{B_j} \supseteq B_j\)  is the \(S\) -closure of \(B_j\) ;
and since \(\lambda  \)  is monotone,
\(\xi (x) \in \lambda  _X (\overline{B_1}, \dots ,\overline{B_n})\) . Further, \(x\mathbin {S}y\)  implies that either \(x=y\) , in which
case there is nothing to prove, or there exists \(j\)  such that
\(x,y\in A_j\)  and therefore
\(\xi (x), \xi (y) \in \lambda  _{j,X}(A_1, \dots , A_k).\) 
Because \(\xi ( x )\)  also lies in \(\lambda  _X (\overline{B_1}, \dots ,\overline{B_n}) \) , we obtain
\(\lambda  _{j,X}(A_1, \dots , A_k)\subseteq \lambda  _X (\overline{B_1}, \dots , \overline{B_n})\) 
by lem:predicate-liftings-preserve-equivalence-classes,
and thus \(\xi (y) \in \lambda  _X (S[B_1], \dots , S[ B_n ])\) . \(\Box \)

Proof of lem:bekic
By Tarski, all fixed points exist. \((x_0,y_0)\)  is a fixed point of
\(\langle f,g \rangle : X\times Y\rightarrow X\times Y\) , because
\(y_0 = g(x_0,y_0)\)  and thus also
\(x_0 = f(x_0, \nu y.g(x_0,y)) = f(x_0,g(x_0,y_0)) = f(x_0,y_0).\) 
For any other fixed point \((x^{\prime },y^{\prime })\)  of \(\langle f,g \rangle \) , we have
\(x^{\prime } = f(x^{\prime },y^{\prime }) = f(x^{\prime }, g(x^{\prime },y^{\prime }))\le f(x^{\prime }, \nu y.g(x^{\prime },y)),\) 
so \(x^{\prime } \le x_0\)  and furthermore
\(y^{\prime } = g(x^{\prime },y^{\prime }) \le g(x_0,y^{\prime })\le \nu y.g(x_0,y)\) .\(\Box \)

Proof of thm:generic-expression-describes-exactly-one-bisimulation-class
We first show that \(\phi \)  denotes a single behavioural equivalence
class, i.e. (i) we have invariance under behavioural equivalence
(lem:invariance) and (ii) two states satisfying \(\phi \)  are
bisimilar. In order to prove (ii) we may w.l.o.g. assume that the
two states live in the same coalgebra; indeed, given two coalgebras
\(C\)  and \(D\)  and states \(x\)  in \(C\)  and \(y\)  in \(D\)  satisfyfing \(\phi \) ,
then \(\operatorname{inl}(x), \operatorname{inr}(y)\)  in \(C + D\)  are behaviourally equivalent to
\(x\)  and \(y\) , respectively, thus both satisfy \(\phi \)  by
lem:invariance.
Now let \(C=(X,\xi )\)  be a \(T\) -coalgebra; we need to
show that any two elements of \(\llbracket \phi  \rrbracket _{C} \)  are behaviourally
equivalent. As noted above, we can transform \(\phi \)  into a
system (REF ) of flat equations, and \(\llbracket \phi  \rrbracket _{C} \)  is
the first component of the greatest fixed point of the corresponding
map of the form (REF ). The
claim thus follows by lem:gfp-is-singleton.
It remains to show that there exists a finite coalgebra \(C\)  such
that \(\llbracket \phi  \rrbracket _{C} \ne \emptyset \) . This is immediate from the finite
model property of the coalgebraic \(\mu \) -calculus [8]};
alternatively, avoiding such overkill, it is seen as follows: We
define \(C=(X,\xi )\)  on the set \(X=\lbrace x_1,\dots ,x_k\rbrace \)  of the variables
in the above flat equation system by
\(\xi (x_i)\in \llbracket L_i \rrbracket _{X} (\lbrace x_1\rbrace ,\dots ,\lbrace x_k\rbrace )\)  where
\(\phi _i=L_i(x_1,\dots ,x_k)\) . Then by construction,
\((\lbrace x_1\rbrace ,\dots ,\lbrace x_k\rbrace )\)  is a fixed point of the equation system,
hence contained in the greatest fixed point, which proves the desired
non-emptiness of the greatest fixed point.

Proof of prop:locally-finite
Recall that the Fischer-Ladner closure of a \(\mu \) -calculus formula
is standardly defined as the closure under subformulas, negation,
and fixed point unfolding. In the absence of negation, we adapt the
definition to include only closure under subformulas and fixed point
unfolding. We then, of course, inherit the standard result that the
Fischer-Ladner closure is finite [13]}. Now by construction
of \(\varepsilon \) , the subcoalgebra of \((\mathcal {E}_0,\varepsilon )\)  generated by
\(\phi \in \mathcal {E}_0 \)  contains only states from the
Fisher-Ladner-closure of \(\phi \) , hence is finite. \(\Box \)

Proof of thm:coalgebraic-and-modallogic-semantics-coincide
It suffices to prove the truth lemma (REF ): The `if'
direction of the claim then follows from invariance of \(\phi \)  under
behavioural equivalence (lem:invariance), and `only if' is
by
Theorem REF .
We strengthen (REF ) to a claim on expressions \(\phi \) 
possibly having free variables: Whenever \(\sigma \)  is a substitution
of the free variables of \(\phi \)  and \(\kappa  \)  a valuation such that
\(\sigma (v)\in \kappa  (v)\)  for every free variable \(v\)  of \(\phi \) , then
\(\phi \sigma \in \llbracket \phi  \rrbracket _{\mathcal {E}_0}^{\kappa }.\) 
We prove (REF ) by induction over \(\phi \) . The case
for fixed point variables is just by the assumption on \(\sigma \)  and
\(\kappa  \) . For the modal case, we calculate as follows:
\(L(\phi _1,\dots ,\phi _n)\sigma & = L(\phi _1\sigma ,\dots ,\phi _n\sigma )\\& \in \varepsilon ^{-1}[\llbracket L \rrbracket _{} (\lbrace \phi _1\sigma _1\rbrace ,\dots ,\lbrace \phi _n\sigma \rbrace )& \\& \subseteq \varepsilon ^{-1}[\llbracket L \rrbracket _{} (\llbracket \phi _1 \rrbracket _{\mathcal {E}_0}^{\kappa },\dots ,\llbracket \phi _n \rrbracket _{\mathcal {E}_0}^{\kappa } \rbrace )& \\& = \llbracket L(\phi _1,\dots ,\phi _n) \rrbracket _{\mathcal {E}_0}^{\kappa }. &\) 

Finally, for the fixed point case \(\nu x.\,\phi \) , first note that by
Lemma REF , we can assume that \(x\)  does not occur as a
free variable in \(\sigma (v)\)  for any free variable \(v\) 
of \(\nu x.\,\phi \) . Moreover, since \(x\)  is not free in
\(\nu x.\,\phi \) , \(\sigma \)  does not touch \(x\) . Thus,
\((\nu x.\,\phi )\sigma =\nu x.\,(\phi \sigma )\) . By construction of
\(\varepsilon \) , \(\nu x.\,(\phi \sigma )\)  is, as a state of \(\mathcal {E}_0 \) ,
behaviourally equivalent to \(\phi \sigma [\nu x.\,\phi \sigma /x]\) ,
which by the inductive hypothesis is contained in
\(\llbracket \phi  \rrbracket _{\mathcal {E}_0}^{\kappa ^{\prime }} \)  where \(\kappa ^{\prime }\)  arises from \(\kappa \) 
by assigning to \(x\)  the value
\(\lbrace \nu x.\,\phi \sigma \rbrace =\lbrace (\nu x.\,\phi )\sigma \rbrace \) . This shows that
\(\lbrace (\nu x.\,\phi )\sigma \rbrace \)  is a post-fixed point of the map defining
\(\llbracket \nu x.\,\phi  \rrbracket _{\mathcal {E}_0}^{\kappa } \) , and hence contained in
\(\llbracket \nu x.\,\phi  \rrbracket _{\mathcal {E}_0}^{\kappa } \) , which proves the claim. \(\Box \)

Proof of lem:alpha-eq
Let \(\pi _\alpha :\mathcal {E}_0 \rightarrow \mathcal {E}_0/\alpha \)  denote the quotient map of
\(\mathcal {E}_0 \)  modulo \(\alpha \) -equivalence. Paralleling the definition of
\(\varepsilon \) , we define a \(T\) -coalgebra structure \(\varepsilon _\alpha \)  on
\(\mathcal {E}_0/\alpha \)  by
\(\varepsilon _\alpha ( \pi _\alpha (\textit {L} ( \phi _1, \dots , \phi _n ) )) &\in \llbracket L \rrbracket _{} ( \lbrace  \pi _\alpha (\phi _1) \rbrace , \dots , \lbrace  \pi _\alpha (\phi _n) \rbrace  )\\\varepsilon ( \pi _\alpha (\nu x.\phi ) ) & = \varepsilon ( \pi _\alpha (\phi [ \nu x.\phi /x]) ). \) 

One sees in largely the same way as for \(\varepsilon \)  that this is
actually a definition, noting additionally that \(\alpha \) -equivalent
transformations of a formula \(L(\phi _1,\dots ,\phi _n)\)  necessarily
happen in its arguments \(\phi _i\)  and that the number of top-level
fixed point operators is invariant under \(\alpha \) -equivalence. We
are done once we show that
\(\pi _\alpha :(\mathcal {E}_0,\varepsilon )\rightarrow (\mathcal {E}_0/\alpha ,\varepsilon _\alpha )\)  is
a coalgebra morphism. We proceed by case distinction over the shape
of states \(\phi \in \mathcal {E}_0 \) :
First assume that \(\phi \)  has the form
\(\phi =L(\phi _1,\dots ,\phi _n)\) . We have to show
\(T\pi _\alpha (\varepsilon (L(\phi _1,\dots ,\phi _n)))\in \llbracket L \rrbracket _{} (\lbrace \pi _\alpha (\phi _1)\rbrace ,\dots ,\lbrace \pi _\alpha (\phi _n)\rbrace )\) . By
naturality, this is equivalent to
\(\varepsilon (L(\phi _1,\dots ,\phi _n))\in \llbracket L \rrbracket _{} (\pi _\alpha ^{-1}[\lbrace \pi _\alpha (\phi _1)\rbrace ],\dots ,\pi _\alpha ^{-1}[\lbrace \pi _\alpha (\phi _n)\rbrace ])\) ,
which follows by monotonicity from the fact that
\(\varepsilon (L(\phi _1,\dots ,\phi _n))\in \llbracket L \rrbracket _{} (\lbrace \phi _1\rbrace ,\dots ,\lbrace \phi _n\rbrace )\) 
by definition.
Second, assume that \(\phi \)  has the form \(\phi =\nu x.\psi \) . We
proceed by induction on the number of top-level fixed point
operators in \(\phi \) : We have
\(T\pi _\alpha (\varepsilon (\nu x.\psi )) & =T\pi _\alpha (\varepsilon (\psi [\nu x.\psi /x]))& \\& = \varepsilon _\alpha (\pi _\alpha (\psi [\nu x.\psi /x]))& \\& \varepsilon _\alpha (\pi _\alpha (\nu x.\psi ))& .\) 

Since \(\phi \)  is closed, these are the only cases. \(\Box \)
