(3) \(\forall \vec{i} (\exists \vec{b},\vec{o} (C_{R_1}(\vec{i},\vec{b})\wedge C_{R^{\prime }_2}(\vec{b},\vec{o}))) \leftrightarrow \exists \vec{o}^{\prime } C_R(\vec{i},\vec{o}^{\prime })\) 
, and (4) \(\forall \vec{i},\vec{o} (\exists \vec{b}(C_{R_1}(\vec{i},\vec{b}) \wedge C_{R^{\prime }_2}(\vec{b},\vec{o}))\rightarrow C_R(\vec{i},\vec{o}))\) .
In all these, \(C_{R^{\prime }_2}\)  need not be constructed but can be described by the formula \((\forall \vec{i}) (C_{R_1}(\vec{i},\vec{b})\rightarrow C_R(\vec{i},\vec{o}))\) .By performing quantifier elimination on this formula, \(C_{R^{\prime }_2}\)  can be constructed explicitly, in time that may be exponential. c.f., [1]}..
