I am currently looking at a set of problems which all deal with attributes of a certain subset of Goto programs which have certain limitations. They are as follows:

- $ \text{Goto}_{17}$ describes the set of all Goto-programs in which no constant is greater than $ 17$ . Show that every Goto-program can be emulated by a $ \text{Goto}_{17}$ -program.
- $ \text{Goto}_{17}^{c}$ describes the set of all Goto-programs in which variables can be no higher than c and constants no higher than 17. Why is the Halting-problem decideable for this set of programs?

Following are my thoughts so far on these problems:

- It is rather easy to see that any given program can be trivially converted into not using constants higher than 17 by repeating any operation that would do so as often as necessary to evoke the same result. Even comparisons can work by using a dummy variable to store the variables value, then comparing to 17, reducing the variable and so on, until we have compared it against what we want to compare it to. And there will always be a variable easily chosen for this if we just spread out the variables so that in our new $ \text{Goto}_{17}$ -program only every second variable is used for normal calculation. This way we can always work with any variables "dummy-partner" variable for calculations like this without loosing the value. This all feels very unpolished though and I struggle with formulating it in a way that makes it into an actual proof. Am I on the right track and how can this be explained better if yes? How at all, if no?
- In this case I am even less confident in my basic idea. We almost have a situation in which I am confident to say that we can just go through every state of the program that is even theoretically possible and decide whether it can hold in that state. But how do I know of a state whether it is also practically possible, or in other words, does the program actually ever reach this constellation of variable values and position in code? We can’t just simulate the program, as infinite loops are still possible here in contrast to more simple languages like loop-languages. Why can the Halting-Problem be solved in this case? What is the method to achieve this? Can we maybe guarantee that on a set of finite amounts of variables (which is given, as the code must be finite) we must at some point reach a situation where we either halt or where our state exactly matches a prior state, as all these variables have a finite amount of states they can be in?