# Correctness proof: induction on sequence of steps, need a stronger claim?

Im trying to prove the correctness of the construction proposed in this site answer: a two stack PDA that simulates a Turing Machine. By "correctness" i mean to prove more or less formally that we can translate accepting sequences of steps.

Given a TM $$M=(Q,\Sigma_I,\Sigma_O,\delta,q_0,Q_F)$$ and a 2-PDA $$A=(Q',\Sigma_I,\Sigma_O',\delta',q_0', Q_F)$$ defined as the cited answer suggest.

We need to show that for all $$w \in \Sigma^*$$, if $$w \in L(M)$$ then $$w \in L(A)$$, i.e, if the first accepts then the other accepts.

This is for all $$w \in \Sigma^*$$: $$\exists q \in Q_F: q_0\,w \Rightarrow_{\delta}^* \alpha_1\,q\, \alpha_2 \,\,\implies\,\, \exists q' \in Q_F: (q_0',w,\,\) \Rightarrow_{\delta'}^* (q',\epsilon,\beta_1,\beta_2) \tag{*}\label{*}$$ where:

• $$\Rightarrow_{\delta}$$ is the usual step relation between machine descriptions, asume it is defined appropriately for TM and for 2-PDA based on the transition functions $$\delta$$ and $$\delta'$$ .
• $$\Rightarrow_{\delta}^*$$ is the transitive-reflexive closure of step relation, also for TM and 2-PDA.
• Descriptions for TM are noted $$X_1...X_{i-1} q X_{i}... X_n$$ meaning the actual tape content is $$X_1...X_n$$, actual state is $$q$$ and head is over $$X_i$$
• Descriptions for 2-P2A are quadruplets $$(q,w,\beta_1,\beta_2)$$ meaning the actual state is $$q$$, remaining input is $$w$$, first stack content $$\beta_1$$ and second stack content $$\beta_2$$.

So $$\eqref{*}$$ is saying that for any word $$w$$, if there is in $$M$$ a sequence of steps in from $$q_0$$ to a final state $$q$$ then there is a sequence of steps in $$M'$$ from $$q_0'$$ to a final state $$q'$$.

Induction over the length of $$\Rightarrow_{\delta}^*$$ would be sketched as:

1. Base case $$n=1$$ .....
2. Induction Hypothesis: Asume for any sequence of length $$n > 0$$.
3. Induction Thesis: Prove for a sequence of length $$n+1$$ where $$n > 0$$ .....

But... i have a problem with this approach. In the proof for the inductive step, we have a sequence of $$n+1$$ steps for $$M$$ like: $$q_0\,w \,\Rightarrow_{\delta}\, ... \Rightarrow_{\delta}^n\, \gamma_1\,q_i\,\gamma_1 \,\Rightarrow_{\delta}\, \alpha_1\,q\,\alpha_2 \quad\text{ and } q \in Q_F$$

I cant apply here the Inductive Hypothesis because $$q_i$$ cant be a also a final state transitioning to $$q$$. Final states in TM can't have ongoing transitions ( maybe relaxed variants can be proposed but i prefer to let it be like that).

My question is, do i need to prove something stronger than $$\eqref{*}$$ to avoid these little technical inconveniences?. Im thinking something like: $$\forall q \in Q: q_0\,w \Rightarrow_{\delta}^* \alpha_1\,q\, \alpha_2 \,\,\implies\,\, \forall q' \in Q': (q_0',w,\,\) \Rightarrow_{\delta'}^* (q',\epsilon,\beta_1,\beta_2)$$ But im not sure this logically implies $$\eqref{*}$$. I would like to hear general recommendations when doing this type of proofs.