The following table summarizes the internal and observable transition relations for tcc.

Let us describe the internal reduction rules:

- The rule
**RTell**says that the process**tell**( c ) adds c to the current store d, via conjunction, and evolves into**skip**. - The rule
**RPar**is the standard interleaving rule for parallel composition. - Let Q =
**local**(x;c) P in Rule**RLoc**. The global store is d and the local store is c. We distinguish between the*external*(corresponding to Q) and the*internal*point of view (corresponding to P). From the internal point of view, the information about the variable x, possibly appearing in the global store d , cannot be observed. Thus, before reducing P we first hide the information about x that Q may have in d by existentially quantifying x in d. Similarly, from the external point of view, the observable information about x that the reduction of internal agent P may produce (i.e., c') cannot be observed. Thus we hide it by existentially quantifying x in c' before adding it to the global store. Additionally, we make c' the new private store of the evolution of the internal process. - Since the process P=
**unless**c**next**Q executes Q in the next time unit only if the final store at the current time unit does not entail c, in the rule**RUnl**P evolves into**skip**if the current store d entails c. - Rule
**RRep**dictates that the process !P produces a copy of P at the current time unit, and then persists in the next time unit. - Rule
**RAsk**describes the behavior of P=**when**c**do**Q. If the current store d entails c, then the process Q is executed. - Let ≡ be the smallest congruence satisfying:
- P ≡ Q if P and Q differ only by a renaming of bound variables (alpha-conversion).
- P ||
**skip**≡ P. - P || Q ≡ Q || P.
- P || (Q || R) ≡ (P || Q) || R.

If P≡Q and c is logically equivalent to d, we say that <P,c>≡<Q,d>. Rule **RStr** says that structurally congruent configurations have the same reductions.

The seemingly missing rules for the processes **next** P and **unless** c **next** P (when c cannot be entailed from the current store) are given by the rule **RObs**. This rule says that an observable transition from P labeled with (c,d) is obtained from a terminating sequence of internal transitions of the form <P,c>→ ^{*}<Q,d>. The process R to be executed in the next time interval is equivalent to F(Q) (the “future” of Q). The process F(Q) is obtained by removing from Q any local information that has been stored in Q, and by
“unfolding” the sub-terms within **next** and **unless** expressions. More precisely:

- F(
**skip**) =**skip** - F(
**next**P) = P - F(
**unless**c**next**P) = P - F(P1 || P2) = F(P1) || F(P2)
- F( (
**local**x;c)P ) = (**local**x;true) P