## Appendix  
### Proof of Theorem 1  
We first give some technical lemmas. **Lemma 1**. : _Let \(TS_{1}=((A_{1},D_{1}),T_{1})\) and \(TS_{2}=((A_{2},D_{2}),T_{2})\) be two trace systems, \(A_{1}\cap A_{2}=\emptyset\) and \(\rho\subseteq A_{1}\cup A_{2}\)._  
1. \(\Pi_{\rho}(TS_{1}.TS_{2})=\Pi_{\rho}(TS_{1}).\Pi_{\rho}(TS_{2})\)__
2. \(\Pi_{\rho}(TS_{1}+TS_{2})=\Pi_{\rho}(TS_{1})+\Pi_{\rho}(TS_{2})\)__  
**Proof. **  
**Item 1. **\(\Pi_{\rho}(TS_{1}.TS_{2})\)__  
\(=\) { _by definition of the concatenation of trace systems_ }  
\(\[PERSON]_{\rho}((A_{1}\cup A_{2},D_{1}D_{2}^{\circ}),\{\tau_{1}.\tau_{2}\mid\tau_{1 }\in T_{1},\;\tau_{2}\in T_{2}\})\)__  
\(=\) { _by Definition 8_ }  
\(((\rho,\[PERSON]_{\rho}(D_{1}D_{2}^{\circ})),\[PERSON]_{\rho}(\{\tau_{1}.\tau_{2}\}\mid \tau_{1}\in T_{1},\;\tau_{2}\in T_{2}\})\)__  
\(=\) { _by the properties of projection over strings and over dependencies_ }  
\(((\rho,\[PERSON]_{\rho}(D_{1})\[PERSON]_{\rho}(D_{2})^{\circ}),\{\[PERSON]_{\rho}(\tau_{1})\mid \tau_{1}\in T_{1}\}.\{\Pi_{\rho}(\tau_{2})\mid\tau_{2}\in T_{2}\}\)__  
\(=\) { _by Definition 8_ }  
\(\Pi_{\rho}(TS_{1}).\Pi_{\rho}(TS_{2})\)__  
**Item 2**.: _This case can be proven in a similar way._  
In the following, given a trace language \(T\), by \(alph(T)\), we denote the set of symbols occurring in all traces belonging to \(T\).  
**Lemma 2**.: _Let \(TS_{1}=((A_{1},D_{1}),T_{1})\) and \(TS_{2}((A_{2},D_{2}),T_{2})\) be two trace systems, \(\rho,\rho^{\prime}\subseteq A_{1}\cup A_{2}\) and \(\rho\subseteq\rho^{\prime}\)._  
1. \(\Pi_{\rho}(TS_{1}\|TS_{2})=\Pi_{\rho}(\Pi_{\rho^{\prime}}(TS_{1})\|\Pi_{\rho^{ \prime}}(TS_{2}))\)__ _where_ \(\rho^{\prime}=\rho\cup(alph(T_{1})\cap alph(T_{2}))\)__
2. \(\Pi_{\rho}(TS_{1}^{i})=(\[PERSON]_{\rho}(TS_{1}))^{i}\)__  
**Proof.**  
**Item 1.**_First, we prove, ad absurdum, that: \(\Pi_{\rho}(T_{1}\|T_{2})\subseteq\Pi_{\rho}(\Pi_{\rho^{\prime}}(T_{1})\|\Pi_{ \rho^{\prime}}(T_{2}))\)__  
_Suppose that \(\tau\
ot\in\Pi_{\rho}(\Pi_{\rho^{\prime}}(T_{1})\|\Pi_{\rho^{\prime}}(T_{2}))\)._  
\(\tau\
ot\in\Pi_{\rho}(\Pi_{\rho^{\prime}}(T_{1})\|\[PERSON]_{\rho^{\prime}}(T_{2}))\)__  
_implies { _by Definition 8.2_ }  
\(\tau\
ot\in\{\Pi_{\rho}(w)\mid w\in(\Pi_{\rho^{\prime}}(T_{1})\|\Pi_{\rho^{ \prime}}(T_{2})\}\)__  
_implies { _by definition of the parallel composition of trace languages_ }  
\(\tau\
ot\in\{\Pi_{\rho}(w)\mid w\in\{w^{\prime}\mid\;\Pi_{A_{1}}(w^{\prime}) \in\Pi_{\rho^{\prime}}(T_{1})\text{ and }\Pi_{A_{2}}(w^{\prime})\in\Pi_{\rho^{\prime}}(T_{2})\}\}\)__  
_implies: \(\tau=\Pi_{\rho}(w)\) and \(\Pi_{A_{1}}(w)\in\Pi_{\rho^{\prime}}(T_{1})\text{ or }\Pi_{A_{2}}(w)\in\Pi_{\rho^{\prime}}(T_{2})\)__  
_implies: { by Definition 8.2_ }  
\(\tau=\Pi_{\rho}(w)\) and \((\Pi_{A_{1}}(w)\
ot\in\{\Pi_{\rho^{\prime}}(k)\mid k\in T_{1}\}\text{ or }\Pi_{A_{2}}(w)\
ot\in\{\Pi_{\rho^{\prime}}(k)\mid k\in T_{1}\})\)__  
_implies: { by Definition 8.2_ }  
\(\tau=\Pi_{\rho}(w)\) and \((\Pi_{A_{1}}(w)\
ot\in\{\Pi_{\rho^{\prime}}(k)\mid k\in T_{1}\}\text{ or }\Pi_{A_{2}}(  
implies:_  
\(\tau=\Pi_{\rho}(w)\) _and \(((\Pi_{A_{1}}(w)=\Pi_{\rho^{\prime}}(k)\) and \(k\
ot\in T_{1})\) or \((\Pi_{A_{2}}(w)=\Pi_{\rho^{\prime}}(k)\) and \(k\
ot\in T_{2}))\)_  
_absurdum_ \(\{\) _since \(\rho^{\prime}=\rho\cup(alph(T_{1})\cap alph(T_{2}))\) \(\}\)__  
_The case \(\Pi_{\rho}(\Pi_{\rho^{\prime}}(T_{1})\|\Pi_{\rho^{\prime}}(T_{2}))\subseteq\Pi _{\rho}(T_{1}\|T_{2})\) can be proven similarly. The thesis holds by properties of projection over dependencies._  
**Item 2.** _This is similar._  
**Lemma 3**.: _Let \(s\) be an expression over \(A\) and \(\rho\subseteq A\)._  
\[\Pi_{\rho}(TS(s))=\Pi_{\rho}(TS(\mathcal{T}_{\rho}(s)))\]  
**Proof. **  
_The proof is made by the induction on the structure of the term._  
**Base step. ** \(s=nil\)_: straightforward._  
**Inductive step. ** _We denote \(TS(a)=(\{a\},\{(a,a)\}),\{[a]\})\)._  
\(s=a.s_{1}\)_:_  
\(\Pi_{\rho}(TS(a.s_{1}))\)__  
\(=\quad\{\) _by Definition 2 and Lemma 1.