Turing-completeness of Goto language with limited constants This is taken from an old exam of my university that I am using to prepare myself for the coming exam:
Given is a language $\text{Goto}_{17} \subseteq \text{Goto}$. This language includes exactly those $\text{Goto}$ programs in which no constant is ever greater than $17$. Show that every $\text{Goto}$ program can be simulated by a $\text{Goto}_{17}$ program.
$Goto$ here describes the set of all programs written in the $Goto$ language made up of the following elements:
With variables $v_i \in \mathbb{N}$ and constants $c \in \mathbb{N}$
Assignment: $x_i := c, x_i := x_i \pm c$ 
Conditional Jump: if(Comparison) goto $L_i$ 
Haltcommand: halt
It seems obvious to me that this would not limit the power of a program, as there are easy ways to just repeat operations to achieve the same thing with limited constants. To add or subtract arbitrary values we can just add or subtract repeatedly. To compare, we can put our value to compare with into a dummy variable and compare, reduce, repeat until we know the value. These dummy variables are guaranteed to be unused and free for this use if we simply map the variables from our Goto program so that any variable $v_i$ from the Goto language maps onto $v_{2i}$ in our new language.
How can the equivalence in power between these to languages be shown? Is a compiler from one to the other the best solution, or are there more elegant ways? Specifically showing how comparisons work seems like it would be rather complicated and this is a question that originally appeared in a written exam with only a few minutes to answer this question if you average it out. If there is no better way, how would an approach to converting the following Goto program into a limited Goto program of this kind look?
v = 99
repeat: v = v + 1
if(v = 100)goto repeat
halt
No, that is not a proof.  &quot;It seems obvious to me&quot; is not a proof.
To obtain a formal proof, describe an algorithm that, given a Goto program $P$, outputs a Goto$_{17}$ program $P'$, and prove that $P'$ simulates $P$.  Basically, you need to construct a compiler that compiles from Goto to Goto$_{17}$, and then prove it correct.