Chapters X, XI and XV (possibly also others) in Shelah's book "Proper and Improper Forcing" deal with the problem of iterating nonproper forcing notions. (By this I mean very non-proper. E.g., not even $S$-proper for any stationary $S$.)

• Chapter X gives a definition of revised countable support iteration (RCS). (It is somewhat difficult to read, but there are other definitions in the literature which could be used instead.
• Chapter XI deals with nonproper iterations not adding reals over models of CH. There is a property of forcing notions $Q$ that I will call $Pr_{X}(Q)$ that satisfies: Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$ and moreover does not add reals. AND: The limit of an RCS iteration (that use lots of collapses) of forcing notions with $Pr_X$ will itself have property $Pr_X$.
• Chapter XV introduces a property that I will call $Pr_{XV}$ and proves a similar statement: Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$ AND: The limit of an RCS iteration (that use lots of collapses) of forcing notions with $Pr_{XV}$ will itself have property $Pr_{XV}$.

A main point is that Namba forcing $Nm$ satisfies both of these properties. (Regardless of whether $Nm$ is semiproper or not. There are several versions of $Nm$: Laver-like or Miller-like, using the club filter or the cobounded filter; I am not sure if all of them have these properties.)

Roughly speaking, $Pr_{XV}(Q)$ is this: whenever you have a sufficiently nice tree $(N_\eta: \eta\in \omega_2^{<\omega})$ of countable elementary submodels of the universe, where niceness in particular implies that the intersections of the models converge to the same ordinal $\delta$, then $Q$ forces that there exists a branch $\nu\in \omega_2^\omega$ such that $N_\nu[G]\cap \omega_1=N_\nu\cap \omega_1=\delta$. As I recall, if $Q=Nm$ then the branch $\nu$ which is generic will satisfy the requirement.

Chapters X, XI and XV (possibly also others) in Shelah's book "Proper and Improper Forcing" deal with the problem of iterating nonproper forcing notions. (By this I mean very non-proper. E.g., not even $S$-proper for any stationary $S$.)

• Chapter X gives a definition of revised countable support iteration (RCS). (It is somewhat difficult to read, but there are other definitions in the literature which could be used instead.
• Chapter XI deals with nonproper iterations not adding reals over models of CH. There is a property of forcing notions $Q$ that I will call $Pr_{X}(Q)$ that satisfies: Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$ and moreover does not add reals. AND: The limit of an RCS iteration (that uses lots of collapses) of forcing notions with $Pr_X$ will itself have property $Pr_X$.
• Chapter XV introduces a property that I will call $Pr_{XV}$ and proves a similar statement: Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$ AND: The limit of an RCS iteration (that uses lots of collapses) of forcing notions with $Pr_{XV}$ will itself have property $Pr_{XV}$.

A main point is that Namba forcing $Nm$ satisfies both of these properties. (Regardless of whether $Nm$ is semiproper or not. There are several versions of $Nm$: Laver-like or Miller-like, using the club filter or the cobounded filter; I am not sure if all of them have these properties.)

Roughly speaking, $Pr_{XV}(Q)$ is this: whenever you have a sufficiently nice tree $(N_\eta: \eta\in \omega_2^{<\omega})$ of countable elementary submodels of the universe, where niceness in particular implies that the intersections of the models with $\omega_1$ converge to the same ordinal $\delta$ along every branch, then $Q$ forces that there exists a branch $\nu\in \omega_2^\omega$ such that $N_\nu[G]\cap \omega_1=N_\nu\cap \omega_1=\delta$. As I recall, if $Q=Nm$ then the generic branch $\nu$ (the union of all stems of conditions in the generic filter) will satisfy the requirement.