1: \begin{definition}

2: Given a refinement function for event structures \refinement, we define an operation $\refinement^\Psi$ that refines an \eventpsi-process to a new one over the names

3: \[

4: T^\Psi = \{(e,e') \mid e\in E, e'\in E_{ref(l(e))}\}. 

5: \]

6: An \eventpsi-process $P$, build according to Theorem~\ref{th_syntactic_restrictions}, with frame $\psiframe{P}=\Psi_P$, is refined into a process 

7: \[

8: \hspace{9ex}\refinement^{\psi}\!(P)=|_{(e,e')\in T^P}P_{(e,e')}, \text{\hspace{8ex} with } T^P = \{(e,e')|e\in \mathit{en}(P), e'\in  E_{ref(l(e))}\}

9: \]

10: and 

11: $P_{(e,e')} = \psiAssertOp{\{(e,e')\}} $, if $e \in \Psi_P $, otherwise

12: $P_{(e,e')} = \psiCase{\varphi_{(e,e')}:\overline{(e,e')}(e,e').\psiAssertOp{\{(e,e')\}}}$, with the conditions being 

13: \[

14: \varphi_{(e,e')} = (\precondset{(e,e')}, \preconfset{(e,e')}),

15: \]

16: where\ \ $\precondset{(e,e')} = \{(d,d') \mid d\in\pi_L(\varphi_e) \vee (d=e \wedge d'\in\condRelEv_{ref(l(d))} e)\}$\ \ and\ \ $\preconfset{(e,e')} = \{(d,d')| d \in \pi_R(\varphi_e)\}$.

17: % 

18: % \hn{In the end we rename any $(d,d')\in T^P$ to an $e\in E$ respecting the order.}

19: \end{definition}

20: