Show that the encoding of the operator Even in the mu-calculus captures the property of interest:
β¦Even(π)β§π = {π | β complete computation π = πβ β πβ β πβ β ... βπ s.t. πα΅’ β¨ π}
Discuss an extension of CCS with an operator of sequential composition between processes