Definition. Possible termination predicate for CCS with \textbf {1} [pa-0006]

We define an inductive judgement P \checkmark , where P is a process in CCS augmented with an additional process constant \textbf {1}:

\begin {gather*} \dfrac { }{ \textbf {1} \checkmark } \quad \dfrac {P_k \checkmark }{\sum _{i \in I} P_i \checkmark } \\[2em] \dfrac { P \checkmark \quad Q \checkmark }{P|Q \checkmark } \dfrac { P \checkmark }{ P\setminus \alpha \checkmark } \quad \dfrac { P \checkmark }{ P [ f ] \checkmark } \end {gather*}