+ \right.} \\
+
+\IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
+& =
+& \mathit{eval\_fold}(x,P_2,\mathcal{E}')
+& \\
+& & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
+\IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\
+
+\mathit{eval\_fold}(x,P,\mathcal{E})
+& =
+& \mathcal{E}(x)
+& \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\
+
+\mathit{eval\_fold}(x,P,\mathcal{E})
+& =
+& \mathit{eval\_fold}(x,P,\mathcal{E}')
+& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
+& & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\
+&
+& \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
+\\
+&
+& \multicolumn{2}{l}{\mathcal{E}''(y) =
+\left\{
+\begin{array}{ll}
+ v_1 & y\in \NAMES(P)\setminus\{x\} \\
+ \mathcal{E}(x) & y=x \\
+ \bot & \mathit{otherwise} \\
+\end{array}
+\right.
+}
+\\
+