Vtgyjfy

Im trying to prove the correctness of the construction proposed in this CS-SE 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 quadtext{ 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.