Definition Chart reparametrization [efr-000K]
Definition Chart reparametrization [efr-000K]
Let A_1,A_2,B_1,B_2 be arenas, and let S_1, f_1: TS_1 \otimes A_1 \leftrightarrows B_1, S_2, f_2: TS_2 \otimes A_2 \leftrightarrows B_2 be controlled processes. A chart reparametrization f_1 \to f_2 consists of charts a: A_1 \rightrightarrows A_2, b: B_1 \rightrightarrows B_2, and a morphism \phi : S_1 \to S_2 so that the square