Let $\mathbb{X_0,X_1,Y_0,Y_1,A_0,A_1,B_0,B_1}$ be logics.

Let $f_0:\mathbb{X_0}\,|\, \mathbb{A_0}, f_1:\mathbb{X_1}\,|\, \mathbb{A_1} g_0:\mathbb{Y_0}\,|\, \mathbb{B_0} f_0:\mathbb{Y_1}\,|\, \mathbb{B_1}$ be meta processes.

Let $\mathcal{Q_0}(\mathbb{X_0,Y_0}), \mathcal{Q_1}(\mathbb{X_1,Y_1}), \mathcal{R_0}(\mathbb{A_0,B_0}), \mathcal{R_1}(\mathbb{A_1,B_1})$ be meta relations.

Let $i_0(f_0,g_0)$ and $i_1(f_1,g_1)$ be meta inferences.

Let $[\![\mathbb{X}]\!], [\![\mathbb{Y}]\!], [\![\mathbb{A}]\!], [\![\mathbb{B}]\!]$ be flow types.

Let $[\![f]\!], [\![g]\!]$ be flow processes.

Let $[\![\mathcal{Q}]\!], [\![\mathcal{R}]\!]$ be flow relations.

A flow inference, or double transformation,

is a matrix transformation $[\![i]\!]:i_0\Rightarrow i_1$

3.png

which coheres with the joins of the flow relations.

4l.png

4r.png