For a forcing notion $Q$, let $\dot{S^Q}$ be the $Q$-name for the class of ordinals $\{\kappa : \kappa = \omega_1^{V}$ $or$ $\kappa$ $is$ $a$ $regular$ $uncountable$ $cardinal \}$ in $V^Q$.
We say that $Q$ is $\dot{S^Q}$-semiproper iff for all $\lambda$ large enough, for all $N$ countable elementary submodel of $(H(\lambda), \in)$ such that $\{Q, \dot{S^Q}\} \in N$, for all $q \in Q \cap N$, there exists $p \in Q$, $p$ extends $q$ and $p$ satisfies the following:
for all regular uncountable cardinal $\kappa$ in $N$, for all $\dot{\beta}$ a $Q$-name for an ordinal in $\kappa$, $p \Vdash_Q $ $``if$ $\kappa \in \dot{S^Q},$ $then$ $\exists A \in N$ $(|A| < \kappa$ $and$ $\dot{\beta} \in A"$.
Now let $\alpha$ be a limit ordinal, $\bar{Q} = \langle P_i, \dot{Q_i} : i < \alpha \rangle$ be a revised countable support (RCS) iteration, and $P_{\alpha} = Rlim(\bar{Q}) =$ RCS limit of $\bar{Q}$.
Assume for all $i < j < \alpha$, $P_i \Vdash$ $``P_j/\dot{G_i}$ $is$ $\dot{S^{P_i/\dot{G_i}}}-semiproper"$. Is it true in general that there exists a $\dot{\xi}$, a $\bar{Q}$-name for an ordinal $< \alpha$ such that:
If $p \in P_{\gamma + 1}$, $p \Vdash_{\bar{Q}} \dot{\xi} = \gamma$, then $p \upharpoonright \gamma \Vdash_{P_{\gamma}} ``cf(\alpha) = \aleph_0$ $or$ $\forall k$ $(\gamma < k < \alpha \rightarrow$ $\Vdash_{P_k/\dot{G_{\gamma}}}$ $``cf(\alpha)^{V^{P_{\gamma}}}$ $is$ $regular$ $uncountable")"$?
