I cannot prove the following theorem given in Schneider's “On Concurrent Programming” as (3.16e):
$$\Diamond\Box P \to \Box\Diamond P$$
I was given $$\begin{align} \Box P & \to P\\ \Box P & \to \Box\Box P \\ \Box(P\to Q) & \to (\Box P \to \Box Q)\\ P & \vdash \Box P \\ \Diamond P & := \lnot\Box\lnot P \end{align}$$
I deduced that I can prove (3.16e) from $$\Diamond\Box P \to \Box(\Box P \lor \Diamond\Box P)$$ which means “Suppose that $\Box P$ occurs at $t$. If we reached $t$, then $\Box P$, else $\Diamond\Box P$.”. I will appreciate any hint.
It is unprovable in the given theory. There is a Kripke frame $\langle\{0, 1, 2\}, \operatorname{preorder\_cl}(\{\langle 0, 1\rangle, \langle 0, 2\rangle\})\rangle$ (“preorder_cl” is preorder closure aka reflexive transitive closure) that satisfies the given theory and does not satisfy (3.16e). A Kripke frame satisfies (3.16e) iff it is confluent, see Wikipedia/Kripke_semantics#Correspondence_and_completeness. The Kripke frame $\langle\mathbb{N}, \leq\rangle$ used in linear-time temporal logic is confluent.