&\qquad\Exists\rsB_1, \rsB_2. m \in\wsat\state{\mask\cup\mask_\f}{\rsB\mtimes\rs_\f}\land m \in\textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land{}&\\
&\qquad\Exists\rsB_1, \rsB_2. m \in\wsat\state{\mask\cup\mask_\f}{\rsB_1 \mtimes\rsB_2\mtimes\rs_\f}\land m \in\textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land{}&\\
&\qquad\qquad (\expr_\f = \bot\lor m \in\textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))