Theorem. Correctness of the \Upsilon translation [pa-000A]
Our syntactic transformation \Upsilon gives a process whose completed traces are the same as the partial traces of the original process.
\llbracket P \rrbracket _\text {PT} = \llbracket \Upsilon (P) \rrbracket _\text {CT}