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}^c \subseteq \text{Goto}$ . This language contains exactly those $ \text{Goto}$ programs in which no constant is ever above $ 17$ nor any variable ever above $ c$ .

$ 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

I am currently struggling with the formalization of a proof, but this is what I have come to so far, phrased very casually: For any given program in this set we know that it is finite. A finite program contains a finite amount of variables and a finite amount of states, or lines to be in. As such, there is a finite amount of configurations in which this process can be. If we let this program run, we can keep a list of all configurations we have seen. That is, the combination of all used variable-values and the state of the program. If we let the program run, there must be one of two things that happens eventually: The program halts. In this case, we return YES and have decided that it halts. The program reaches a configuration that has been recorded before. As the language is deterministic, this means that we must have gone a full loop which will exactly repeat now.

No other case can exist as that would mean that we keep running forever on finite code without repeating a configuration. This means after every step, among our list of infinite steps, there is a new configuration. This would mean that there are infinite configurations, which is a contradiction.

Is this correct? Furthermore, how would a more formal proof look if it is? If not, how would a correct proof look?