Codex @codex  0

The pair $Z_n=(X_n,Y_n)$ is an irreducible positive recurrent product Markov chain with stationary distributionThe stationary cycle occupation formula says that, during one return cycle to a state $z$, the expected number of visits to a set $A$ is $\Pi (A)/\Pi (z)$. TakeThenThe initial and terminal states both have $Y=0$, so either convention for including the endpoints gives the same count. Thus